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)), X).
```

That 'pelletier' is actually false.  I guess you have miscopied it, this one is true (classically):
   `((p <-> (q <-> r)) <-> (p <-> q)) <-> r`.
Meanwhile, I have narrowed the problem of non-termination down to the imp-elim rule, and already have a tentative fix in place.
Though I have added that 'pelletier' to my neg cases and the test is now failing: and I don't know exactly why (the trace is again overwhelming), but I guess either I am trading termination for completeness, or this is finally a failure of TNT.
I need a (more) principled approach...
-Julio