Welcome to the homepage of Paradox! Paradox is a tool that processes first-order logic problems and tries to find finite-domain models for them. Paradox is written by Koen Claessen and Niklas Sörensson.

News

Paradox reads problems in TPTP and Otter syntax. It understands TPTP-style clauses and formulas, and it also supports the TPTP include command. Further, Paradox can read Otter-style clause sets, though only if you switch on prolog_style_variables.

Paradox produces one of the following three results: CONTRADICTORY, when it has shown that there is no model, SATISFIABLE, when it has found a model, or INCONCLUSIVE, when it has given up. On request, a list of function and predicate tables over a finite domain can be produced when a model is found.

Here is a list of options (which you get when typing paradox --help).

Paradox is mainly implemented in Haskell, but a part of it is an incremental SAT-solver implemented in C++. They are linked together using Haskell's Foreign Function Interface. The techniques we use in Paradox are described in a paper accepted at Model Computation 2003. There is also a Paradox CASC system description.

Here is the source distribution of Paradox v. 1.0-casc. We have successfully used ghc 5.04.3 and g++ 2.95.3 in order to build Paradox. Use other compiler versions at your own risk! The source code is licensed under the GPL. (Please let us know if you have problems with that license.)

Please let us know if you are using Paradox! We are always interested in hearing about both success stories and cases where Paradox could be improved.

Here are some links to other systems for finding finite-domain models: