2

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

Bob Jarvis - Слава Україні
  • 48,992
  • 9
  • 77
  • 110
Grzegorz Wierzowiecki
  • 10,545
  • 9
  • 50
  • 88
  • Thanks for pointing out Godel incompleteness theorem. That's , why I need only partial support for arithmetic, which I can handle (implement), if sources will be nice to extend :). – Grzegorz Wierzowiecki Aug 15 '11 at 13:32
  • Hey, @larsmans , [don't forget about that](http://en.wikipedia.org/wiki/G%C3%B6del%27s_completeness_theorem) and might like [to watch that](http://www.youtube.com/watch?v=7XfA5EhH7Bc). – Grzegorz Wierzowiecki Aug 31 '11 at 16:28

3 Answers3

3

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.

Fred Foo
  • 355,277
  • 75
  • 744
  • 836
1

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

  • It's absolutely good for beginning. Covering linear constrains cases is good point to start. What I am looking for is more like [is(equal())](http://maxima.sourceforge.net/docs/manual/en/maxima_11.html#equal) tool from Maxima, or [equals](http://www.wolframalpha.com/input/?i=%28a%2Bb%2Bc%29%2B%28x%2By%29**2+equals+%28x**2%2Bb%2Bc%2Ba%2B2*x*y%2By**2%29) from Wolframalpha. More details, in ["Equations Equality test (in C++ or with Unix tools)"](http://stackoverflow.com/questions/7024746/equations-equality-test-in-c-or-with-unix-tools-algebra-functions-isomorphis/7236855#7236855). – Grzegorz Wierzowiecki Aug 31 '11 at 10:11
  • As you can see in [answer](http://stackoverflow.com/questions/7024746/e/7236855#7236855), Maxima's `is(equal())` is implemented with `ratsimp()`, which simplifies difference of two equations. If difference can be symbolically simplified to 0, it implies, it's equal. Do you have an idea how something like that might be implemented with prolog? Is it suitable? Or maybe another tool for symbolic equations, CAS, [for C++ - here another question](http://stackoverflow.com/questions/7024746/equations-equality-test-in-c-or-with-unix-tools-algebra-functions-isomorphis/7236855) ? – Grzegorz Wierzowiecki Aug 31 '11 at 10:16
  • 1
    This is easy, have a look here: http://www.jekejeke.ch/idatab/doclet/prod/en/docs/05_run/06_bench/09_programs/04_poly/package.html –  Aug 31 '11 at 10:29
  • You can easily define your own is_poly/2, that would evalute a poly. Just defined X is_poly A+B :- Y is_poly A, Z is_poly B, poly_add(Y,Z,X). Etc.. And maybe some pretty printing as well. It is not included in the above code. –  Aug 31 '11 at 12:37
0

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

Grzegorz Wierzowiecki
  • 10,545
  • 9
  • 50
  • 88
  • Actually this looks like a nice book. I like Theorem 2.25 since it is practically my answer. And it also makes use of Prolog, which is nice! But I cannot see the full book on the web. So what section do you think relates to "polynom tautology"? Is it covered in the book? –  Aug 31 '11 at 13:05
  • Unfortunately, it covers only boolean cases, even if it presents a variety of approaches in dealing with boolean logic. – Grzegorz Wierzowiecki Aug 31 '11 at 16:08