Re: Still on negative translation for substructural logics

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?

As far as I can tell, i.e. modulo bugs I have not found, it must terminate, though I do not have the full formal proof yet.

?- solve_case(TT, pelletier, G), time(solve_t__sel(TT, G)).
solve_case(neg, pelletier, []=>((p<->(q<->r))<->(p<->q))).
Or just a problem of explosion?

You are using all and only the wrong methods, anyway I happy you...
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).
```
Indeed, haven't you noticed all those appends in `reduction/5`?  It's very slow, especially in SWI-Prolog...  But I won't touch it for now, I need clearer ideas about the next step, plus with appends it's much easier to match it in formalization.
-Julio