Coq is a formal proof management system: a proof done with Coq is mechanically checked by the machine. In particular, Coq allows:
* to define functions or predicates,
* to state mathematical theorems and software specifications,
* to develop interactively formal proofs of these theorems,
... [More] check these proofs by a relatively small certification "kernel". [Less]
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
... [More] the SAT/Models division of the CASC World Championship on First-Order
Automated Theorem Proving in 2003, 2004, 2005 and 2006. [Less]