Re: Still on negative translation for substructural logics

We can recreated the first Wolfram example in Prolog:
Lets permit that we write the input as [1,2,a,4,5,
b,c,8,9,10] and then have rewriting rules [a->3,b->6,
c->7,d->8] applied, by this little Declarative (What) code:
step(L,R) :- nth1(K,L,a,H), nth1(K,R,3,H).
step(L,R) :- nth1(K,L,b,H), nth1(K,R,6,H).
step(L,R) :- nth1(K,L,c,H), nth1(K,R,7,H).
step(L,R) :- nth1(K,L,d,H), nth1(K,R,8,H).
find(L,L) :- \+ step(L,_).
find(L,R) :- step(L,H), find(H,R).
Each derivation is a Procedural (How) execution:
?- find([1,2,a,4,5,b,c,8,9,10],X).
X = [1, 2, 3, 4, 5, 6, 7, 8, 9, 10];
X = [1, 2, 3, 4, 5, 6, 7, 8, 9, 10];
X = [1, 2, 3, 4, 5, 6, 7, 8, 9, 10]
Etc..
Can we count the number of Hows to solve the What?
?- aggregate_all(count, find([1,2,a,4,5,b,c,8,9,10],X), C).
C = 6.
So there are 6 different Procedures that tell
us which steps to exactly use when, to solve the
Declaratively given problem which leaves open
Mild Shock schrieb:

 Looks like uncontrolled confluence, which usually
happens when you write down rules declaratively.
 There are some nice pictures:
 Wolfram, S. A New Kind of Science. Champaign, IL:
Wolfram Media, pp. 507 and 1036-1037, 2002.
https://mathworld.wolfram.com/Confluent.html
 Showing how search explodes, by doing redundant work.
 Mild Shock schrieb:

Could it be that your procedure doesn't
terminate always? Why is this not finished
after more than 1 minute?
>
?- solve_case(TT, pelletier, G), time(solve_t__sel(TT, G)).
Action (h for help) ? abort
% 844,501,974 inferences, 63.891 CPU in 68.236 seconds (94% CPU, 13217933 Lips)
% Execution Aborted
>
The test case was:
>
solve_case(neg, pelletier, []=>((p<->(q<->r))<->(p<->q))).
>
Or just a problem of explosion?