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: presprover.pl

To try it, download Scryer Prolog and run:

      $ scryer-prolog presprover.pl

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

More about Prolog

Main page