Re: Still on negative translation for substructural logics

About Gentzens Inversion Lemma that allow
to place cuts and tremdously speed up proofs.
You find this in Gentzens original paper:
Untersuchungen über das logische Schließen. I. In: Mathematische Zeitschrift. Band 39 (2), 1935, S. 176–210
https://gdz.sub.uni-goettingen.de/id/PPN266833020_0039?tify={%22view%22:%22info%22,%22pages%22:[180]}
But you can also draw on Jens Otten.
In Jens Otten intuitionistic logic prover,
he has a column in his tabular representation
of inference rules that indicates whether a rule
is invertible. "nin" stands for not invertible.
"inv" stands for invertible.
fml((A=>B), 1,nin,[(A=>B)],         [C],[D],[], _, _,[!],A:B,C:D).
fml((A=>B), 0,inv,[A],              [B],[], [], _, _,[], [], [] ).
https://www.leancop.de/ileansep/
Invertible inference rules are somtimes denoted
by a double bar ===, whereas the non invertible
inference rules only use a single bar ---.
The two implication inference rules are:
        G, A |- B
      =============== (R->)
        G |- A -> B
        G, A -> B |- A    G, B |- C
      ------------------------------ (L->)
          G, A -> B |- C
(R->) is invertible, (L->) is not invertible.
Invertible rules such as (R->) can be greedily
applied with the need for backtracking.
Roughly expressed when you see an invertible rule,
you can commit yourself in applying it in
backward chaining.
Julio Di Egidio schrieb:

On 02/12/2024 12:37, Julio Di Egidio wrote:
 

?- unfold(tnt((p<->(q<->r))<->(p<->q)), Qs).

 (That should have been an `X`, not a `Qs`, that is a formula, not a proof tree: anyway, you get the point.)
 -Julio