Presprover — Prove formulas of Presburger arithmetic

Presprover lets you reason about formulas of Presburger arithmetic, which is the first-order theory of the natural numbers with addition.

In contrast to Peano arithmetic, Presburger arithmetic omits the multiplication operation. Presburger arithmetic is consistent, complete and decidable.

Source code:

To try it, download Scryer Prolog and run:

      $ scryer-prolog
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

Main page