Path: ...!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: Still on negative translation for substructural logics
Date: Mon, 2 Dec 2024 09:56:47 +0100
Message-ID: <vijsoe$a84f$1@solani.org>
References: <vihumn$2eqeg$3@dont-email.me> <vijsa2$a7ut$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:56:46 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="336015"; 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:cc6RggaQyToJ5B0n2oBOi9YDilY=
In-Reply-To: <vijsa2$a7ut$1@solani.org>
X-User-ID: eJwFwQkBwDAIA0BLwCBp5fAU/xJ2Fx8UTUfAY2O93gWvulmTI0gUd54JrXFebFqpbsqcYXvWlVTLpy4C4w9PIRVO
Bytes: 4134
Lines: 95

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
>