Re: The solver does not terminate

Plus a hand full of more techniques, like
for example what is hard wired into Prolog,
that you choose goals from left to right.
See also:
In both SL and SLD, "S" stands for the fact that the only literal resolved upon in any clause C i is one that is uniquely selected by a selection rule or selection function. In SL resolution, the selected literal is restricted to one which has been most recently introduced into the clause. In the simplest case, such a last-in-first-out selection function can be specified by the order in which literals are written, as in Prolog.
https://en.wikipedia.org/wiki/SLD_resolution#The_origin_of_the_name_%22SLD%22
So basically you would replace something like:
    nth1(N, List, Lit, List2)
    select(Lit, List, List2)
    member(Lit, List)
By this here:
    once(nth1(N, List, Lit, List2))
    once(select(Lit, List, List2))
    once(member(Lit, List))
No need to backtrack over multiple literals.
With Gentzen inversion lemmas you can even go a step farther:
    nth1(N, List, Lit, List2), !
    select(Lit, List, List2), !
    member(Lit, List), !
Cut away certain rules, avoiding even more backtracking.
Mild Shock schrieb:

 Yes, a binary tree of depth n, can still have 2^n nodes.
 Unless you apply some pruning technique.
 The typical pruning technique in proof search is
 Gentzens inversion lemma.
 Julio Di Egidio schrieb:

On 05/12/2024 22:26, Julio Di Egidio wrote:

On 02/12/2024 12:37, Julio Di Egidio wrote:

On 02/12/2024 09:49, Mild Shock wrote:

Could it be that your procedure doesn't
terminate always? Why is this not finished
after more than 1 minute?

>
The solver *is* very slow at the moment, and you are trying to prove a too complicated statement:
>
```
?- unfold(tnt((p<->(q<->r))<->(p<->q)), Qs).
Qs = ((((p->(q->r)/\(r->q))/\((q->r)/\(r->q)->p)->(p->q)/\(q->p))/\((p->q)/\(q->p)->(p->(q->r)/\(r->q))/\((q->r)/\(r->q)->p))->0)->(((p->(q->r)/\(r->q))/\((q->r)/\(r->q)->p)->(p->q)/\(q->p))/\((p->q)/\(q->p)->(p->(q->r)/\(r->q))/\((q->r)/\(r->q)->p))->0)->0). >
```

>
Yeah, there is definitely a bug, though unrelated to TNT: the reduction rules are applied in the order of definition, and I can confirm that, depending on that order, the solver may not terminate.
>
Would you think there is an order that works?  Otherwise it gets complicated...

>
It's slowly dawning on me what might be going wrong: I have proved that reductions decrease the goal size *for each residual goal*, but each reduction may produce more than one residual goal, and I have not proved that the proof search will not keep branching indefinitely...
>
-Julio
>