To install click the Add extension button. That's it.

The source code for the WIKI 2 extension is being checked by specialists of the Mozilla Foundation, Google, and Apple. You could also do it yourself at any point in time.

4,5
Kelly Slayton
Congratulations on this excellent venture… what a great idea!
Alexander Grigorievskiy
I use WIKI 2 every day and almost forgot how the original Wikipedia looks like.
Live Statistics
English Articles
Improved in 24 Hours
Added in 24 Hours
What we do. Every page goes through several hundred of perfecting techniques; in live mode. Quite the same Wikipedia. Just better.
.
Leo
Newton
Brights
Milds

Paradox (theorem prover)

From Wikipedia, the free encyclopedia

Paradox
Developer(s)
  • Koen Lindström Claessen
  • Niklas Sörensson
Written inHaskell
TypeAutomated theorem proving
LicenseGNU 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

  1. ^ "Paradox". Chalmers University of Technology. Archived from the original on 8 January 2007. Retrieved 26 May 2007.
  2. ^ 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.
  3. ^ "Entrants' System Descriptions". University of Miami. Paradox 3.0. Archived from the original on 7 November 2018. Retrieved 7 November 2018.
  4. ^ "Paradox". Chalmers University of Technology. Archived from the original on 15 January 2007. Retrieved 30 April 2020.
  5. ^ 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.
  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.
  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].
  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.
This page was last edited on 2 May 2024, at 21:45
Basis of this page is in Wikipedia. Text is available under the CC BY-SA 3.0 Unported License. Non-text media are available under their specified licenses. Wikipedia® is a registered trademark of the Wikimedia Foundation, Inc. WIKI 2 is an independent company and has no affiliation with Wikimedia Foundation.