HOME

TheInfoList



OR:

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 ( sv, Chalmers tekniska högskola, often shortened to Chalmers) is a Swedish university located in Gothenburg that conducts research and education in technology and natural sciences at a high international le ...
. 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 ...
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 License (GNU GPL or simply GPL) is a series of widely used free software licenses that guarantee end users the four freedoms to run, study, share, and modify the software. The license was the first copyleft for general ...
and is free.


Features

The Paradox developers described the software as a '' Mace-style'' method after the McCune's tool of that name. 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 languages for authoring ontologies. Ontologies are a formal way to describe taxonomies and classification networks, essentially defining the structure of knowledge for vario ...
OWL2.


Competition

Paradox was a division winner in the annual
CADE ATP System Competition The CADE ATP System Competition (CASC) is a yearly competition of fully automated theorem provers for classical logic CASC is associated with the Conference on Automated Deduction and the International Joint Conference on Automated Reasoning organ ...
, an annual contest for automated theorem proving, in the years 2003 to 2012.


References

Free theorem provers Free software programmed in Haskell {{free-software-stub