Re: The solver does not terminate

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