Paradox logo

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.


  • (2003-07-31) Paradox won the SAT/Models class (generated most models) in the CASC 2003 competetion for first-order logic tools!

  • (2003-07-25) The current stable version is Paradox v. 1.0-casc. You can download it below.
  • Usage

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

  • paradox-1.0-casc.tar.gz
  • Here are some pre-compiled binaries for various systems.

  • Linux: paradox-1.0-casc-linux.tar.gz

  • Solaris: paradox-1.0-casc-solaris.tar.gz

  • Windows: paradox-1.0-casc-windows.tar.gz

  • Mac OS X / Panther: paradox-1.0-casc.sit
    (Thanks to Branden Fitelson!)
  • 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.

    Related Systems

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

  • Gandalf, developed by Tanel Tammet.

  • MACE and MACE4 (also called ICGNS), both developed at Argonne National Laboratory.
  • Koen Claessen, Aug 17, 2004.