Finite-domain model finder for pure first-order logic with equality
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:
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.
References.
 ;templatestyles src="Reflist/styles.css" / ;