Re: The solver does not terminate

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