Re: Still on negative translation for substructural logics

Similar problem here:
?- solve_case(TT, pelletier2, G), time(solve_t__sel(TT, G)).
Action (h for help) ? abort
% 1,368,141,792 inferences, 103.188 CPU in 109.107 seconds (95% CPU, 13258794 Lips)
% Execution Aborted
Mostlikely the reduction has way too much backtracking,
the implementation of some Gentzen inversion lemmas
is lacking. Gentzen inversion lemma allow to place
cuts in the proof search. I don't know how you formulate
this in Coq. I even don't know whether your Coq formalization
models the Prolog non-determinism.
The test case was:
solve_case(pos, pelletier2, []=>((p<->(q<->(r<->s)))<->(p<->(q<->r)))).
Mild Shock schrieb:

Could it be that your procedure doesn't
terminate always? Why is this not finished
after more than 1 minute?
 ?- solve_case(TT, pelletier, G), time(solve_t__sel(TT, G)).
Action (h for help) ? abort
% 844,501,974 inferences, 63.891 CPU in 68.236 seconds (94% CPU, 13217933 Lips)
% Execution Aborted
 The test case was:
 solve_case(neg, pelletier, []=>((p<->(q<->r))<->(p<->q))).
 Or just a problem of explosion?
 Julio Di Egidio schrieb:

On 01/12/2024 15:32, Mild Shock wrote:
>
 > So although it was very temping to download
 > you software, and then replace these line:
 > <https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11>
 > By these line:
 > notation(gliv(X), (~(~X)))
 > solve_t__sel(neg, C=>X) :-
 >     solve(C=>gliv(X)).
>
Or just change the definition of `dnt`, or create another one.  The code is functional and pretty flexible actually, `notation/5` is `multifile`.
>
 > I am afraid I have no time for that. You
 > could do it by yourself. Or what
>
I have already done it, and I have already told you the results!  You have no time for anything apparently, except for posting random shit and fucking with thread titles: I have messages all over the place, and it's just me, you, and Ross once a month...
>
---
>
Here is an interesting new case, which I had thought should be *unsolvable*:
>
```
?- solve_w([]=>dnt((~(~p)->p)<->p\/(~p))), !.  % DNE<->LEM
```
>
Unsolvable not just because my logic is *affine*, but because the actual statement, provable intuitionistically, is intrinsically higher-order:
>
```
Theorem DNE_is_LEM : (forall p, ~ ~ p -> p) <-> (forall p, p \/ ~ p).
```
>
while the statement I am proving above is this one, and it is not intuitionistically provable (AFAICT):
>
```
Theorem DNE_is_LEM_not_quite : forall p, (~ ~ p -> p) <-> (p \/ ~ p)
```
>
Yet with my `dnt`, my solver proves even that one (but I still have to inspect the proof tree, what I actually get).  Indeed, I am rather worried that it just solves everything I throw at it, though not the falsities... which is why I am also developing a meta-theory for it, in Coq:
>
<https://gist.github.com/jp-diegidio/b6a7a071f9f81a469c493c4afcc5cb11#file-gentzen-v> >
>
-Julio