Paradox (theorem prover)

Paradox
Original authors	Koen Lindström Claessen Niklas Sörensson
Developer	Chalmers University of Technology
Initial release	2003 (2003)
Final release	4 / 2011 (2011)
Repository	{{URL|example.com|optional display text}}
Written in	Haskell
Engine
Available in	English
Type	Automated theorem proving
License	GNU General Public License

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 written mostly in the programming language Haskell. It is free and open-source software released under the terms of the GNU General Public License.

Features

The Paradox developers described the software as a Models And Counter-Examples (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 method
• incremental satisfiability checker – works with small domains first, then gradually increases the domain size, reusing information gained from prior failed searches
• static symmetry reduction – adds extra constraints
• sort inference – 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.