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.

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