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?
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.
(<= a b) [true iff a is less than or equal to b]
(< a b)
(>= a b)
(> a b)
(= a b)
(+ a b c) [true iff a plus b equals c]
(+ a b c d)
tzimtsum accepts the following logical connectives, which take in
booleans and return a boolean.
(and x y)
(or x y)
(if x y) [equivalent to (or (not x) y)]
For help with writing propositions using quantifiers, see the "Translating
English to FOL" section of these UWisconsin lecture
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!