Paradox (theorem prover)
Template:Short description {{#invoke:Infobox|infobox}}Template:Template other{{#invoke:Check for unknown parameters | check | showblankpositional=1 | unknown = Template:Main other | preview = Page using Template:Infobox software with unknown parameter "_VALUE_"|ignoreblank=y | AsOf | author | background | bodystyle | caption | collapsetext | collapsible | developer | discontinued | engine | engines | genre | included with | language | language count | language footnote | latest preview date | latest preview version | latest release date | latest release version | latest_preview_date | latest_preview_version | latest_release_date | latest_release_version | licence | license | logo | logo alt | logo caption | logo upright | logo size | logo title | logo_alt | logo_caption | logo_upright | logo_size | logo_title | middleware | module | name | operating system | operating_system | other_names | platform | programming language | programming_language | released | replaced_by | replaces | repo | screenshot | screenshot alt | screenshot upright | screenshot size | screenshot title | screenshot_alt | screenshot_upright | screenshot_size | screenshot_title | service_name | size | standard | title | ver layout | website | qid }}Template:Main other
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.<ref name="Equinox-Paradox"/><ref name="Petr-P"/> It can a participate as part of an automated theorem proving system.<ref name="Petr-P"/> The software is primarily written in the Haskell programming language.<ref name="CASC-6-Entrants"/> It is released under the terms of the GNU General Public License and is free.<ref name="Paradox-home-alone"/>
FeaturesEdit
The Paradox developers described the software as a Mace-style method after the McCune's tool of that name.<ref name="Author-paper"/><ref name="Baumgartner-slides"/> The Paradox introduced new techniques which help to reduce the computational complexity of the model search problem:<ref name="Author-paper"/>
- 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 OWL2.<ref name="Hoot-too"/>
CompetitionEdit
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.<ref name="CADE-comp-2018"/>