Path: ...!feeds.phibee-telecom.net!weretis.net!feeder8.news.weretis.net!reader5.news.weretis.net!news.solani.org!.POSTED!not-for-mail
From: Mild Shock <janburse@fastmail.fm>
Newsgroups: sci.logic
Subject: Re: intuitionistic vs. classical implication in Prolog code
Date: Mon, 2 Dec 2024 09:31:33 +0100
Message-ID: <vijr94$a72h$2@solani.org>
References: <vihumn$2eqeg$3@dont-email.me> <vihvl9$9568$1@solani.org>
 <vii0l0$m02t$1@solani.org> <vii1jv$2eqeg$4@dont-email.me>
 <vii2qb$97ao$1@solani.org> <vii9vv$2eqeg$5@dont-email.me>
 <vijpj3$a69e$2@solani.org> <vijr25$a72h$1@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Mon, 2 Dec 2024 08:31:32 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="334929"; mail-complaints-to="abuse@news.solani.org"
User-Agent: Mozilla/5.0 (Windows NT 10.0; Win64; x64; rv:91.0) Gecko/20100101
 Firefox/91.0 SeaMonkey/2.53.19
Cancel-Lock: sha1:f56S4ibo3RJxW4hkl6VQBWoTsvU=
X-User-ID: eJwVytEVwEAEBMCWsixOOUfov4S8zPeYOryDbk5bW081xjQaN/mmRMOPQldgtdUZEnOw/0uOM67UXMkqzsMPNGsU4g==
In-Reply-To: <vijr25$a72h$1@solani.org>
Bytes: 2157
Lines: 49


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?