tzimtsum, a Presburger arithmetic proposition decider Haskell library

Instructions. Write a formula in the textbox, click Decide, and tzimtsum will tell you if that formula is true or false.
Click the example links in the Introduction to try them out! Syntax and semantics are described below.

This form will send your formula to the server.
To use tzimtsum locally, you can download the x86-64 Linux binary or compile the source code.


Have you ever wanted to know if there's a largest natural number?

Ex.Ay.(>= x y)

There exists an x such that for all y, x is greater than or equal to y.

Or if a natural plus a positive natural could ever equal itself?

Ex.Ey.La=0.(and (> y a) (+ x y x))

Let a = 0. There exist x, y for which y is greater than a and x plus y equals x.

Or if there are infinite even numbers?

Ax.Ey.Ez.(and (> y x) (+ z z y))

For all x, there exists y that is larger than x and is two times some z.

Or if there exist x, y, z with n greater than 2 for which xn + yn = zn is satisfiable?

Well, tzimtsum can't help you with that last one. But it will let you decide the truth of any proposition involving quantifiers, addition, and comparisons (but not variable multiplication).

That's because Presburger arithmetic is a decidable theory, although the runtime is lower bounded by a double exponential in the number of nested quantifiers!

tzimtsum uses the automata-based solution given in Michael Sipser's Introduction to the Theory of Computation (6.2).

tzimtsum Syntax and Semantics

The tzimtsum syntax is strict.
First, a series of quantifiers, either existential (E) or universal (A) and the variables they bind, separated by periods.
Then a series of literals (L), the variable it binds, an equals sign, and the natural number it binds to, separated by periods.
Then a formula using those variables and literals.

Be careful! Too many universals or too large of a formula will quickly grow too expensive to compute.

If a variable is not quantified over or bound to a literal, it defaults to zero.

tzimtsum accepts the following relations, which take in variables or literals and return a boolean. tzimtsum accepts the following logical connectives, which take in booleans and return a boolean. For help with writing propositions using quantifiers, see the "Translating English to FOL" section of these UWisconsin lecture notes.
tzimtsum is written in Haskell, and uses Parsec for parsing input. Interested readers can check out the source code, contributors welcome!

Comments and suggestions can be mailed to surya at [this domain name].

> In the magical art of Steganography, there is nothing frivolous, nor contrary to the Gospels and the Catholic faith; nor have we taught superstitious beliefs. Everything is based on natural, lawful and honest principles; the mystery which veils the precepts of this art and the names of the spirits, requires a cultivated reader; to hide the secrets of this art, which could be harmful if made known to wicked men, we avail ourselves of the services of the spirits.

tzimtsum is dedicated to my Friend, my Maybe Monad of Indiscriminate Embrace. Uniform Whiskey!