Paradox (theorem prover)
Paradox is a finite-domain model finder for pure first-order logic (FOL) with equality developed by Koen Lindström Claessen and Niklas Sörensson at the Chalmers University of Technology. It can a participate as part of an automated theorem proving system. The software is primarily written in the Haskell programming language. It is released under the terms of the GNU General Public License and is free.
Features
The Paradox developers described the software as a Mace-style method after the McCune's tool of that name. The Paradox introduced new techniques which help to reduce the computational complexity of the model search problem:
- term definitions, new variable reduction technique,
- incremental satisfiability checker which works with small domains first, then gradually increases the size of the domain, reusing the information it obtained from previous failed searches,
- static symmetry reduction which adds extra constraints,
- sort inference which works with unsorted problems.
Paradox was developed up to version 4, the final version being effective in model finding for Web Ontology Language OWL2.
Competition
Paradox was a division winner in the annual CADE ATP System Competition, an annual contest for automated theorem proving, in the years 2003 to 2012.