Software:Paradox (theorem prover)
| Developer(s) |
|
|---|---|
| Written in | Haskell |
| Type | Automated theorem proving |
| License | GNU General Public License |
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]
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
- ↑ "Paradox". http://www.cs.chalmers.se/~koen/folkung/.
- ↑ 2.0 2.1 Pudlák, Petr (17 July 2007). "Semantic Selection of Premisses for Automated Theorem Proving". The 21st International Conference on Automated Deduction. 257. Bremen. pp. 27–44. https://pdfs.semanticscholar.org/d997/5c5ff3cb52393224fbe6a3fc78b4e4a54cba.pdf. Retrieved 7 November 2011.
- ↑ "Entrants' System Descriptions". http://tptp.cs.miami.edu/~tptp/CASC/J6/SystemDescriptions.html#Paradox---3.0.
- ↑ "Paradox". http://www.cs.chalmers.se:80/~koen/paradox/.
- ↑ 5.0 5.1 Claessen, Koen; Sörensson, Niklas. "New Techniques that Improve MACE-style Finite Model Finding". https://pdfs.semanticscholar.org/ca65/ae805d0fd210141d13a0f2d7be7a075bdd90.pdf.
- ↑ "Automated Theorem Proving". pp. 73–74. http://users.cecs.anu.edu.au/~baumgart/teaching/logic-summer-school-2009-december/slides-automated-reasoning.pdf.
- ↑ Schneider, Michael; Sutcliffe, Geoff (2011). "Reasoning in the OWL 2 Full Ontology Language using First-Order Automated Theorem Proving". arXiv:1108.0155 [cs.AI].
- ↑ "The CADE ATP System Competition - The World Championship for Automated Theorem Proving". http://tptp.cs.miami.edu/~tptp/CASC/.
 |  |
