Paradox (theorem prover)
Paradox is a finite-domain model finder for pure first-order logic 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 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 methodincremental satisfiability checker – works with small domains first, then gradually increases the domain size, reusing information gained from prior failed searchesstatic symmetry reduction – adds extra constraintssort inference – works with unsorted problemsParadox was developed up to version 4, the final version being effective in model finding for Web Ontology Language OWL2.