Paradox (theorem prover)

Paradox
Paradox
Original author(s)	Koen Lindström Claessen; Niklas Sörensson;
Developer(s)	Chalmers University of Technology
Initial release	2003; 22 years ago
Final release	4 / 2011; 14 years ago
Written in	Haskell
Available in	English
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 written mostly in the programming language Haskell.^[3] It is free and open-source software released under the terms of the GNU General Public License.^[4]

Features

The Paradox developers described the software as a Models And Counter-Examples (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 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.^[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". Chalmers University of Technology. Archived from the original on 8 January 2007. Retrieved 26 May 2007.
^ ^a ^b Pudlák, Petr (17 July 2007). "Semantic Selection of Premisses for Automated Theorem Proving" (PDF). In Urban, J.; Sutcliffe, G.; Schulz, S. (eds.). Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories. The 21st International Conference on Automated Deduction. CEUR Workshop Proceedings. Vol. 257. Bremen. pp. 27–44. ISSN 1613-0073. S2CID 16318678. Archived from the original (PDF) on 7 November 2018. Retrieved 7 November 2011.
^ "Entrants' System Descriptions". University of Miami. Paradox 3.0. Archived from the original on 7 November 2018. Retrieved 7 November 2018.
^ "Paradox". Chalmers University of Technology. Archived from the original on 15 January 2007. Retrieved 30 April 2020.
^ ^a ^b Claessen, Koen; Sörensson, Niklas. "New Techniques that Improve MACE-style Finite Model Finding" (PDF). S2CID 15694927. Archived from the original (PDF) on 11 November 2018. Retrieved 11 November 2018.
^ "Automated Theorem Proving" (PDF). Australian National University College of Engineering & Computer Science. pp. 73–74. Archived (PDF) from the original on 11 November 2018. Retrieved 11 November 2018.
^ 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". Previous CASCs' Division Winners. Archived from the original on 1 September 2018. Retrieved 7 November 2018.

[Equinox-Paradox-1] "Paradox". Chalmers University of Technology. Archived from the original on 8 January 2007. Retrieved 26 May 2007.

[Petr-P-2] Pudlák, Petr (17 July 2007). "Semantic Selection of Premisses for Automated Theorem Proving" (PDF). In Urban, J.; Sutcliffe, G.; Schulz, S. (eds.). Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories. The 21st International Conference on Automated Deduction. CEUR Workshop Proceedings. Vol. 257. Bremen. pp. 27–44. ISSN 1613-0073. S2CID 16318678. Archived from the original (PDF) on 7 November 2018. Retrieved 7 November 2011.

[CASC-6-Entrants-3] "Entrants' System Descriptions". University of Miami. Paradox 3.0. Archived from the original on 7 November 2018. Retrieved 7 November 2018.

[Paradox-home-alone-4] "Paradox". Chalmers University of Technology. Archived from the original on 15 January 2007. Retrieved 30 April 2020.

[Author-paper-5] Claessen, Koen; Sörensson, Niklas. "New Techniques that Improve MACE-style Finite Model Finding" (PDF). S2CID 15694927. Archived from the original (PDF) on 11 November 2018. Retrieved 11 November 2018.

[Baumgartner-slides-6] "Automated Theorem Proving" (PDF). Australian National University College of Engineering & Computer Science. pp. 73–74. Archived (PDF) from the original on 11 November 2018. Retrieved 11 November 2018.

[Hoot-too-7] Schneider, Michael; Sutcliffe, Geoff (2011). "Reasoning in the OWL 2 Full Ontology Language using First-Order Automated Theorem Proving". arXiv:1108.0155 [cs.AI].

[CADE-comp-2018-8] "The CADE ATP System Competition - The World Championship for Automated Theorem Proving". Previous CASCs' Division Winners. Archived from the original on 1 September 2018. Retrieved 7 November 2018.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

Paradox (theorem prover)

Features

Competition

References

Portal di Ensiklopedia Dunia