Re: intuitionistic vs. classical implication in Prolog code

Ok my fault I tested Glivenko and not your TNT,
with TNT I get indeed this here:
?- solve_case(TT, pierce, G), solve_t__sel(TT, G).
TT = neg,
G = ([((p->q)->p)]=>p).
Oki Doki
But I am not familiar with this proof display:
[
   impI((p->0))
   impI((p->0))
   [
     impE1(1:(p->q))
     impI(p)
     [
       impE1(1:p)
       unif(2:p)
     ]
     [
       impE2(1:0)
       botE(3:0)
     ]
   ]
   [
     impE2(1:p)
     [
       impE1(1:p)
       unif(2:p)
     ]
     [
       impE2(1:0)
       unif(3:0)
     ]
   ]
]
How is one supposed to read the above?
Mild Shock schrieb:

It didn't work, I was running:
 ?- solve_case(TT, pierce, G), solve_t__sel(TT, G).
 And it showed me in SWI-Prolog false:
 false.
 But the result shoud be true.
 Julio Di Egidio schrieb:

On 01/12/2024 17:27, Mild Shock wrote:
>

Well then Pierce Law is not povable under
the usual Glivenko translation in affine logic.
So what? Whats your point?

>
That my TNT (I am now dubbing it "triple-negation translation") instead works, and where is some piece of theory to attach to it?
>

I found only one book that discusses Glivenk
style translations for substructural logics:
Chatpter 8: Glivenko Theorems
Residuated Lattices: an algebraic glimpse at substructural logics
https://www.researchgate.net/publication/235626321

>
Indeed there is a lot of not much around.  But Girard talks about not having and not wanting a separate semantics, it's all purely syntactic. But I still have only a vague intuition about what that means.
<https://girard.perso.math.cnrs.fr/0.pdf>
>
Anyway, pretty much along that line, I am thinking: could I prove in Prolog the meta-properties I have proved in Coq (so far)? Meta-programming and program-analysis features of Prolog are certainly not lacking...
>
-Julio
>