Question

Closed. This question is seeking recommendations for books, tools, software libraries, and more. It does not meet Stack Overflow guidelines. It is not currently accepting answers.

We don’t allow questions seeking recommendations for books, tools, software libraries, and more. You can edit the question so it can be answered with facts and citations.

Closed 8 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

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

Answer 3

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

友情链接