Paradox (theorem prover)
Template:Short description {{#invoke:Infobox|infobox}}Template:Template other {{#invoke:Check for unknown parameters|check|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 class | logo size | logo title | logo upright | logo_alt | logo_caption | logo_class | logo_size | logo_title | logo_upright | middleware | module | name | operating system | operating_system | other_names | platform | programming language | programming_language | qid | released | replaced_by | replaces | repo | screenshot | screenshot alt | screenshot class | screenshot size | screenshot title | screenshot upright | screenshot_alt | screenshot_class | screenshot_size | screenshot_upright | service_name | size | standard | title | ver layout | website }}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 written mostly in the programming language Haskell.<ref name="CASC-6-Entrants"/> It is free and open-source software released under the terms of the GNU General Public License.<ref name="Paradox-home-alone"/>
Features
The Paradox developers described the software as a Models And Counter-Examples (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 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.<ref name="Hoot-too"/>
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.<ref name="CADE-comp-2018"/>