Re: intuitionistic vs. classical implication in Prolog code

Can you use your gentzen.v to show
that your TNT always works?
Basically giving a Coq verification.
How does one usually demonstrate
Glivenkos theorem?
Mild Shock schrieb:

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?