Path: ...!eternal-september.org!feeder3.eternal-september.org!news.eternal-september.org!.POSTED!not-for-mail
From: Julio Di Egidio <julio@diegidio.name>
Newsgroups: sci.logic
Subject: Re: The solver does not terminate
Date: Sat, 7 Dec 2024 18:19:46 +0100
Organization: A noiseless patient Spider
Lines: 31
Message-ID: <vj203i$31agv$1@dont-email.me>
References: <vihumn$2eqeg$3@dont-email.me> <vijsa2$a7ut$1@solani.org>
 <vik669$3a0q9$1@dont-email.me> <vit5qd$1lts7$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Sat, 07 Dec 2024 18:19:46 +0100 (CET)
Injection-Info: dont-email.me; posting-host="0c848b736f38b2ea404ae4be7849d99c";
	logging-data="3189279"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX1/OrdRAjLWKXs/+7vRUxzZ/zNDtUZm1xOo="
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:TEaLgh+8ctiWEBw7KMHfOWYWNeE=
In-Reply-To: <vit5qd$1lts7$1@dont-email.me>
Content-Language: en-GB
Bytes: 2105

On 05/12/2024 22:26, Julio Di Egidio wrote:
> On 02/12/2024 12:37, Julio Di Egidio wrote:
>> 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?
>>
>> 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)), X).
>> ```

That 'pelletier' is actually false.  I guess you have miscopied it, this 
one is true (classically):

   `((p <-> (q <-> r)) <-> (p <-> q)) <-> r`.

Meanwhile, I have narrowed the problem of non-termination down to the 
imp-elim rule, and already have a tentative fix in place.

Though I have added that 'pelletier' to my neg cases and the test is now 
failing: and I don't know exactly why (the trace is again overwhelming), 
but I guess either I am trading termination for completeness, or this is 
finally a failure of TNT.

I need a (more) principled approach...

-Julio