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: Fri, 6 Dec 2024 15:57:42 +0100
Organization: A noiseless patient Spider
Lines: 30
Message-ID: <viv3d6$2bkfm$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: 8bit
Injection-Date: Fri, 06 Dec 2024 15:57:43 +0100 (CET)
Injection-Info: dont-email.me; posting-host="ac1bca722a3413b6aee6206d9f12e286";
	logging-data="2478582"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX19y2LnvO+71wbVq/KVKUek+9qdFOAvnNyA="
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:D65j3jjB3TbnP/KmxqujflL1uSI=
In-Reply-To: <vit5qd$1lts7$1@dont-email.me>
Content-Language: en-GB
Bytes: 2381

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)), 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).
>> ```
> 
> Yeah, there is definitely a bug, though unrelated to TNT: the reduction 
> rules are applied in the order of definition, and I can confirm that, 
> depending on that order, the solver may not terminate.
> 
> Would you think there is an order that works?  Otherwise it gets 
> complicated...

It's slowly dawning on me what might be going wrong: I have proved that 
reductions decrease the goal size *for each residual goal*, but each 
reduction may produce more than one residual goal, and I have not proved 
that the proof search will not keep branching indefinitely...

-Julio