Path: ...!news.nobody.at!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: The solver does not terminate
Date: Fri, 6 Dec 2024 16:36:28 +0100
Message-ID: <viv5ls$gmgf$1@solani.org>
References: <vihumn$2eqeg$3@dont-email.me> <vijsa2$a7ut$1@solani.org>
 <vik669$3a0q9$1@dont-email.me> <vit5qd$1lts7$1@dont-email.me>
 <viv3d6$2bkfm$1@dont-email.me>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Fri, 6 Dec 2024 15:36:28 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="547343"; 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:fU0gW38W91vAC8DhVf76RlwARPM=
In-Reply-To: <viv3d6$2bkfm$1@dont-email.me>
X-User-ID: eJwFwYEBwCAIA7CXRNoq5+CA/09YQpfpOxAFDicKN2oVmCl7RKvan+1gKcO7a4XNwskrYPq58+zsnd/kjR9XIhXM
Bytes: 2656
Lines: 41


Yes, a binary tree of depth n, can still have 2^n nodes.

Unless you apply some pruning technique.

The typical pruning technique in proof search is

Gentzens inversion lemma.

Julio Di Egidio schrieb:
> 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
>