The solver does not terminate (Was: Still on negative translation for substructural logics)

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...
(Be aware that meanwhile I have changed the code significantly, though the main difference is explicit support for the intuitionistic vs classical proofs.)
-Julio