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 Chalmers University of Technology (, commonly referred to as Chalmers) is a private university, private research university located in Gothenburg, Sweden. Chalmers focuses on engineering and science, but more broadly it also conducts research ...

. It can a participate as part of an

automated theorem proving Automated theorem proving (also known as ATP or automated deduction) is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a majo ...

system. The software is primarily written in the Haskell programming language. It is released under the terms of the

GNU General Public License The GNU General Public Licenses (GNU GPL or simply GPL) are a series of widely used free software licenses, or ''copyleft'' licenses, that guarantee end users the freedom to run, study, share, or modify the software. The GPL was the first ...

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 In computer science, the computational complexity or simply complexity of an algorithm is the amount of resources required to run it. Particular focus is given to computation time (generally measured by the number of needed elementary operations ...

of the

model A model is an informative representation of an object, person, or system. The term originally denoted the plans of a building in late 16th-century English, and derived via French and Italian ultimately from Latin , . Models can be divided in ...

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 The Web Ontology Language (OWL) is a family of Knowledge representation and reasoning, knowledge representation languages for authoring Ontology (information science), ontologies. Ontologies are a formal way to describe Taxonomy, taxonomies and ...

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

{{Haskell programming Free theorem provers Free software programmed in Haskell Software using the GNU General Public License