In contrast to Peano arithmetic, Presburger arithmetic

Source code:

To try it, download SWI-Prolog >= 6.0 and execute:

$ swipl presprover.plA few example queries and their results:

?- valid(exists(x, x > 0)). true. ?- valid(forall(x, exists(y, 3*x + y > 2))). true. ?- valid(2*y + 3*x = 30 /\ x = 0 ==> y = 15). true.Please see the source file for more information.