Equinox is an automated theorem prover for pure first-order logic with equality.

Equinox actually implements a hierarchy of logics, realized as a stack of theorem provers that use abstraction refinement to talk with each other. In the bottom sits an efficient SAT solver (MiniSat).

The main aims of Equinox are (1) to be a theorem prover that performs well at large, automatically generated problems, coming up in for example formal verification areas, and (2) to be able to provide understandable feedback about failed proof attempts.

Equinox is written in the functional programming language Haskell, and developed by Koen Lindström Claessen.

Equinox is funded (2007-2009) by the Swedish Research Council, project 2006-4364.

Paradox is a finite-domain model finder for pure first-order logic with equality.

Paradox is a MACE-style model finder, which means that it translates a first-order problem into a sequence of SAT problems, which are solved by a SAT solver (in our case MiniSat).

Paradox is the proud winner of the SAT/Models division of the CASC World Championship on First-Order Automated Theorem Proving in 2003, 2004, 2005 and 2006.

Paradox is written in the functional programming language Haskell, and is developed by Koen Lindström Claessen and Niklas Sörensson.

Paradox is/was funded (2003-2006) by the Swedish Research Council, project 2003-2983.

The latest version of Equinox. This is still an experimental prototype.

Slides about Equinox:

The latest version of Paradox. This version only reads the new TPTP input syntax.

Paper about Paradox: