Path: eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: Julio Di Egidio <julio@diegidio.name>
Newsgroups: sci.logic
Subject: Re: Still on negative translation for substructural logics
Date: Mon, 2 Dec 2024 12:37:44 +0100
Organization: A noiseless patient Spider
Lines: 31
Message-ID: <vik669$3a0q9$1@dont-email.me>
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: 7bit
Injection-Date: Mon, 02 Dec 2024 12:37:46 +0100 (CET)
Injection-Info: dont-email.me; posting-host="8b87f2f7e098ae75aa40ba304ec8e6fd";
	logging-data="3474249"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX185stcHaNxyv1vivywvkF5Xg2oSKxzXPD0="
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:8xNCDX3LuvNKGzOzpeMuyK5XXp8=
Content-Language: en-GB
In-Reply-To: <vijsa2$a7ut$1@solani.org>

On 02/12/2024 09:49, Mild Shock wrote:

> Could it be that your procedure doesn't
> terminate always? Why is this not finished
> after more than 1 minute?

As far as I can tell, i.e. modulo bugs I have not found, it must 
terminate, though I do not have the full formal proof yet.

> ?- solve_case(TT, pelletier, G), time(solve_t__sel(TT, G)).
> solve_case(neg, pelletier, []=>((p<->(q<->r))<->(p<->q))).
> Or just a problem of explosion?

You are using all and only the wrong methods, anyway I happy you...

The solver *is* very slow at the moment, and you are trying to prove a 
too complicated statement:

```
?- unfold(tnt((p<->(q<->r))<->(p<->q)), Qs).
Qs = 
((((p->(q->r)/\(r->q))/\((q->r)/\(r->q)->p)->(p->q)/\(q->p))/\((p->q)/\(q->p)->(p->(q->r)/\(r->q))/\((q->r)/\(r->q)->p))->0)->(((p->(q->r)/\(r->q))/\((q->r)/\(r->q)->p)->(p->q)/\(q->p))/\((p->q)/\(q->p)->(p->(q->r)/\(r->q))/\((q->r)/\(r->q)->p))->0)->0).
```

Indeed, haven't you noticed all those appends in `reduction/5`?  It's 
very slow, especially in SWI-Prolog...  But I won't touch it for now, I 
need clearer ideas about the next step, plus with appends it's much 
easier to match it in formalization.

-Julio