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 17:17:18 +0100
Organization: A noiseless patient Spider
Lines: 35
Message-ID: <viv82f$2dbt1$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>
 <viv3d6$2bkfm$1@dont-email.me> <viv5ls$gmgf$1@solani.org>
 <viv6ub$gnap$1@solani.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 8bit
Injection-Date: Fri, 06 Dec 2024 17:17:19 +0100 (CET)
Injection-Info: dont-email.me; posting-host="ac1bca722a3413b6aee6206d9f12e286";
	logging-data="2535329"; mail-complaints-to="abuse@eternal-september.org";	posting-account="U2FsdGVkX1/kurD+jMMHGWQV0AmPPqIuTmmWykw9p3A="
User-Agent: Mozilla Thunderbird
Cancel-Lock: sha1:+7+9+Iwsb3bl6WFBWVfKfsd8YiM=
In-Reply-To: <viv6ub$gnap$1@solani.org>
Content-Language: en-GB
Bytes: 2181

On 06/12/2024 16:58, Mild Shock wrote:

> 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.

I had `once` initially, as that certainly makes sense, but it was 
failing even some of the simpler pos cases.  I shall try again.

OTOH, I do not want to cut on the search space, I like the idea that the 
solver backtracks over all possible proofs.  Moreover, I wouldn't think 
that "cutting" matters to termination: 2^n is big, not unbound...

I need to think more about it.

-Julio