Search code examples
open-sourceprologgnu-prologtheorem-proving

Tautology Checker for GNU Prolog

I am looking for open-source implementations of tautology checkers written in GNU Prolog (implementation for SWI-Prolog is acceptable as well, but GNU Prolog is preferred).

I'd like to feed program input with queries like:

A and (B or C) iff (A or B) and (A or C).

or

3^2 * (X + 2) == (9 * X) + 18.

of course, notation can be different, like this:

(3 power 2) mul (X plus 2) equals (9 mul X) plus 18.

What I expect as result, is boolean answer , like "Yes/No", "Equals/Different", "Prove found/Failed to find prove" or similar.

I've found tautology checker for GNU-Prolog on ftp://ftp.cs.yorku.ca/pub/peter/SVT/GNU/ , but licence is not attached and no clue how to apply Gnu Prolog Arithmetic constraints and Arithmetic capabilities in order to extend just logical model with arithmetic.

  • Any other simmilar solvers?
  • Some examples how arithmetic capabilities might be used in order to extend model.

Thanks, Greg.

P.S. According arithmetic, I am looking for partial support - I want to handle only some basic cases, which I can code by hand with simple heuristics (gnu-prolog integer functions examples welcome as well) if proposed solution will handle classical logic properly and open-source code will be nice to extend :).

P.P.S As @larsmans noted, according to Gödel's incompleteness theorems there is no way to prove "all" formulas. That's why I am looking for something that proves, what can be proven from given set of axioms and rules, as I am looking for Gnu Prolog program, I am looking for examples of such sets of axioms and rules ;). Of course checker may fail - I am expecting it will work in "some" cases :). - On the other hand, there is Gödel's completeness theorem ;).

Solution

  • If you want an extensible theorem prover in Prolog, check out the family of lean theorem provers, of which leanCOP is the main representative; it handles classical first-order logic in 555 bytes of Prolog.

    Version 1.0 is the following program:

    prove(M,I) :- append(Q,[C|R],M), \+member(-_,C),
 append(Q,R,S), prove([!],[[-!|C]|S],[],I).
prove([],_,_,_).
prove([L|C],M,P,I) :- (-N=L; -L=N) -> (member(N,P);
 append(Q,[D|R],M), copy_term(D,E), append(A,[N|B],E),
 append(A,B,F), (D==E -> append(R,Q,S); length(P,K), K<I,
 append(R,[D|Q],S)), prove(F,S,[L|P],I)), prove(C,M,P,I).

    The leanCOP website has more readable versions, with more features. You'll have to implement equality and arithmetic yourself.