Re: The solver does not terminate

Hi,
Or start with a deterministic system,
and show that it is immune to how the problem
is stated, immune to all the structural rules.
For example this deterministic classical prover,
for propositional logic. It gives an example
what I mean by Gentzen inversion lemmas:
prove(L) :- select((A->B),L,R), !, prove([-A,B|R]).
prove(L) :- select(-(A->B),L,R), !, prove([A|R]), prove([-B|R]).
prove(L) :- select(-A,L,R), member(A,R), !.
The cut (!)/0 in the first and second claus is justified
by Gentzen inversion lemmas found here, check out page 81:
Basic Proof Theory, Cambridge University Press
A. S. Troelstra &  H. Schwichtenberg - June 2012
https://www.cambridge.org/core/books/basic-proof-theory/928508F797214A017D245A1FB67CCCD9
It can readily prove Peirce Law:
?- prove([(((p->q)->p)->p)]).
true.
But with Coq or Isabelle/HOL you should be
also able to prove these meta theorems about
the Prolog predicate prove/1:
     prove([...,X,Y,...])
    ----------------------- (Exchange)
     prove([...,X,Y,...])
     prove([...,X,X,...])
    ----------------------- (Contraction)
      prove([...,X,...])
      prove([...,X,...])
    ----------------------- (Weakening)
     prove([...,Y,X,...])
https://en.wikipedia.org/wiki/Structural_rule
Bye
Julio Di Egidio schrieb:

On 06/12/2024 17:17, Julio Di Egidio wrote:

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

 

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.

 Indeed, not even a plain `once` works since there may be more than one *different* matching hypothesis, and committing to the first one in order may lead to failure.
 Anyway, as said, I'd rather not cut on the search space (at all), plus I don't see how cutting should matter to termination (given that the reduction rules are not recursive).
 I need to think more about it: what is exactly going wrong.
 -Julio