Paradox (theorem prover)
| Developer(s) |
|
|---|---|
| Engine | |
| Type | automated theorem proving |
Search Paradox (theorem prover) on Amazon.
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 participate as part of an automated theorem proving system.[citation needed] 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] 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, the world championship 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 8 November 2018.
- ↑ Pudlák, Petr (17 July 2007). "Semantic Selection of Premisses for Automated Theorem Proving" (PDF). In Urban, J., Sutcliffe, G., Schulz, S. Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories. The 21st International Conference on Automated Deduction. CEUR Workshop Proceedings. 257. Bremen. pp. 27–44. ISSN 1613-0073. Archived (PDF) from the original on 7 November 2011. Retrieved 7 November 2011.CS1 maint: Uses editors parameter (link)
- ↑ "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.
- ↑ Claessen, Koen; Sörensson, Niklas. "New Techniques that Improve MACE-style Finite Model Finding" (PDF). Archived (PDF) from the original 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" (PDF). Archived (PDF) from the original on 18 November 2018. Retrieved 11 November 2018.
- ↑ "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.
 | This computer science article is a stub. You can help EverybodyWiki by expanding it. |
.svg){kind=logo} | This free and open-source software article is a stub. You can help EverybodyWiki by expanding it. |
This article "Paradox (theorem prover)" is from Wikipedia. The list of its authors can be seen in its historical and/or the page Edithistory:Paradox (theorem prover). Articles copied from Draft Namespace on Wikipedia could be seen on the Draft Namespace of Wikipedia and not main one.
|
This page exists already on Wikipedia. |
