Paradox

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. 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