Tautology Checker for GNU Prolog [closed]

Question

Closed. This question does not meet Stack Overflow guidelines. It is not currently accepting answers.

---

Want to improve this question? Update the question so it's on-topic for Stack Overflow.

Closed 5 years ago.

Improve this question

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

Answer 1

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.

Answer 2

I've found some tautology checkers, in Mathematical Logic for Computer Science by Ben-Ari, Mordechai, unfortunately they cover boolean logic. What advantage, his implementations are in Prolog, and present a variety of approaches related with automated proving, or solving such equations (or, automatically verifying proofs).

Answer 3

You could use constraint logic programming for your problem. Equality gives you directly a result (example GNU Prolog):

?- X*X #= 4.
X = 2

For inequality you will typically need to ask the system to generate instanciations after the constraints have been set up. This is typically done via a labeling directive (example GNU Prolog):

?- 27 * (X + 2) #\= (9 * X) + 18.
X = _#22(0..14913080)
?- 27 * (X + 2) #\= (9 * X) + 18, fd_labeling(X).
X = 0 ? ;
X = 1 ? ;
X = 2 ? ;
Etc..

A list that shows which prologs do have which kind of CLP can be found here. Just check the CLP multi column.

Overview of Prolog Systems, Ulrich Neumerkel

Bye