Presprover — Prove formulas of Presburger
Presprover lets you reason about formulas of
arithmetic, which is the first-order theory of the
natural numbers with addition.
In contrast to Peano arithmetic, Presburger arithmetic omits
the multiplication operation.
Source code: presprover.pl
To try it,
download SWI-Prolog >=
6.0 and execute:
$ swipl presprover.pl
A few example queries and their results:
?- valid(exists(x, x > 0)).
?- valid(forall(x, exists(y, 3*x + y > 2))).
?- valid(2*y + 3*x = 30 /\ x = 0 ==> y = 15).
Please see the source file for more information.
More about Prolog