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.
These details are provided for information only. No information here is legal advice and should not be used as such.
At one point, Open Hub analyzed source code for this project based on code location(s) available at that time. Since then, the code locations have been removed.