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:58:03 +0100
Message-ID: <viv6ub$gnap$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> <viv5ls$gmgf$1@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Fri, 6 Dec 2024 15:58:03 -0000 (UTC)
Injection-Info: solani.org;
	logging-data="548185"; 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:fESUcSGGOfmPPBSEuL+sWLz8IUM=
X-User-ID: eJwNwYEBwCAIA7CXQAq4c7DI/yfMxC00mAgP+Lx7aVQfJJ9vemNfU58yWY17dViaMl7N8BJwnaYaKQbnD29uFmM=
In-Reply-To: <viv5ls$gmgf$1@solani.org>
Bytes: 3953
Lines: 82

Plus a hand full of more techniques, like

for example what is hard wired into Prolog,

that you choose goals from left to right.

See also:

In both SL and SLD, "S" stands for the fact that the only literal 
resolved upon in any clause C i is one that is uniquely selected by a 
selection rule or selection function. In SL resolution, the selected 
literal is restricted to one which has been most recently introduced 
into the clause. In the simplest case, such a last-in-first-out 
selection function can be specified by the order in which literals are 
written, as in Prolog.
https://en.wikipedia.org/wiki/SLD_resolution#The_origin_of_the_name_%22SLD%22

So basically you would replace something like:

    nth1(N, List, Lit, List2)
    select(Lit, List, List2)
    member(Lit, List)

By this here:

    once(nth1(N, List, Lit, List2))
    once(select(Lit, List, List2))
    once(member(Lit, List))

No need to backtrack over multiple literals.

With Gentzen inversion lemmas you can even go a step farther:

    nth1(N, List, Lit, List2), !
    select(Lit, List, List2), !
    member(Lit, List), !

Cut away certain rules, avoiding even more backtracking.

Mild Shock schrieb:
> 
> 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
>>
>