Paradox (theorem prover)

Finite-domain model finder for pure first-order logic with equality From Wikipedia, the free encyclopedia

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.[1][2] It can a participate as part of an automated theorem proving system.[2] The software is primarily written in the Haskell programming language.[3] It is released under the terms of the GNU General Public License and is free.[4]

Quick Facts Developer(s), Written in ...
Paradox
Developer(s)
  • Koen Lindström Claessen
  • Niklas Sörensson
Written inHaskell
TypeAutomated theorem proving
LicenseGNU General Public License
Close

Features

The Paradox developers described the software as a Mace-style method after the McCune's tool of that name.[5][6] The Paradox introduced new techniques which help to reduce the computational complexity of the model search problem:[5]

  • 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.[7]

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.[8]

References

Loading related searches...

Wikiwand - on

Seamless Wikipedia browsing. On steroids.