Re: The solver does not terminate

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