Presprover reasons about formulas of Presburger arithmetic over natural numbers.

Some example queries and their results:

?- valid(forall(x, exists(y, y > x))).
true.


?- valid(not(exists(x,
               exists(y,
                 exists(z, x > y /\ y > z /\ z > x))))). 
true.


?- valid(x < y ==> 10*x < 20*y).
true.


?- solution(X > 1_000_000_000 /\ Y > 10*X).
X = 1536870912,
Y = 16106127360 ;
X = 1536870912,
Y = 16106128384 ;
X = 1536870912,
Y = 16106127872 .