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 level ...

. 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 maj ...

system. The software is primarily written in the

Haskell programming language Haskell () is a general-purpose, statically-typed, purely functional programming language with type inference and lazy evaluation. Designed for teaching, research and industrial applications, Haskell has pioneered a number of programming lang ...

. 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 (Free software), four freedoms to run, study, share, and modify the software. The license was th ...

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 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 organi ...

, 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