E theorem prover

From Wikipedia, the free encyclopedia
Jump to: navigation, search

E is a high performance theorem prover for full first-order logic with equality.[1] It is based on the equational superposition calculus and uses a purely equational paradigm. It has been integrated into other theorem provers and it has been among the best-placed systems in several theorem proving competitions. E is developed by Stephan Schulz, originally in the Automated Reasoning Group at TU Munich.

System[edit]

The system is based on the equational superposition calculus. In contrast to most other current provers, the implementation actually uses a purely equational paradigm, and simulates non-equational inferences via appropriate equality inferences. Significant innovations include shared term rewriting (where many possible equational simplifications are carried out in a single operation),[2] several efficient term indexing data structures for speeding up inferences, advanced inference literal selection strategies, and various uses of machine learning techniques to improve the search behaviour.[2][3][4]

E is implemented in C and portable to most UNIX dialects and the Cygwin environment. It is available under the GNU GPL.[5]

Competitions[edit]

The prover has consistently performed well in the CADE ATP System Competition, winning the CNF/MIX category in 2000 and finishing among the top systems ever since.[6] In 2008 it came in second place.[7] In 2009 it won second place in the FOF (full first order logic) and UEQ (unit equational logic) categories and third place (after two versions of Vampire) in CNF (clausal logic).[8] It repeated the performance in FOF and CNF in 2010, and won a special award as "overall best" system.[9] In the 2011 CASC-23 E won the CNF division and achieved second places in UEQ and LTB.[10]

Applications[edit]

E has been integrated into several other theorem provers. It is, with Vampire and SPASS, at the core of Isabelle's Sledgehammer strategy.[11][12] E also is the reasoning engine in SInE[13] and LEO-II[14] and used as the clausification system for iProver.[15]

Applications of E include reasoning on large ontologies,[16] software verification,[17] and software certification.[18]

References[edit]

  1. ^ Schulz, Stephan (2002). "E - A Brainiac Theorem Prover". Journal of AI Communications 15 (2/3): 111–126. 
  2. ^ a b Schulz, Stephan (2008). "Entrants System Descriptions: E 1.0pre and EP 1.0pre". Retrieved 2009-03-24. 
  3. ^ Schulz, Stephan (2004). "System Description: E 0.81". Proceedings of the 2nd International Joint Conference on Automated Reasoning (Springer). LNAI 3097: 223–228. doi:10.1007/978-3-540-25984-8_15. 
  4. ^ Schulz, Stephan (2001). "Learning Search Control Knowledge for Equational Theorem Proving". Proceedings of the Joint German/Austrian Conference on Artificial Intelligence (KI-2001) (Springer). LNAI 2174: 320–334. doi:10.1007/3-540-45422-5_23. 
  5. ^ Schulz, Stephan (2008). "The E Equational Theorem Prover". Retrieved 2009-03-24. 
  6. ^ Sutcliffe, Geoff. "The CADE ATP System Competition". Retrieved 2009-03-24. 
  7. ^ FOF division of CASC in 2008
  8. ^ Sutcliffe, Geoff (2009). "The 4th IJCAR Automated Theorem Proving System Competition--CASC-J4". AI Communications 22 (1): 59–72. Retrieved 2009-12-16. 
  9. ^ Sutcliffe, Geoff (2010). "The CADE ATP System Competition". University of Miami. Retrieved 20 July 2010. 
  10. ^ Sutcliffe, Geoff (2011). "The CADE ATP System Competition". University of Miami. Retrieved 14 August 2011. 
  11. ^ Paulson, Lawrence C. (2008). "Automation for Interactive Proof: Techniques, Lessons and Prospects". Tools and Techniques for Verification of System Infrastructure - A Festschrift in Honour of Professor Michael J. C. Gordon FRS: 29–30. Retrieved 2009-12-19. 
  12. ^ Meng, Jia; Lawrence C. Paulson (2004). "Experiments on Supporting Interactive Proof Using Resolution". LNCS (Springer) 3097: 372–384. doi:10.1007/978-3-540-25984-8_28. Retrieved 2009-12-16. 
  13. ^ Sutcliffe, Geoff; et al (2009). The 4th IJCAR ATP System Competition. Retrieved 2009-12-18. 
  14. ^ Benzmüller, Christoph; Lawrence C. Paulson; Frank Theiss; Arnaud Fietzke (2008). "LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)". LNCS (4th International Joint Conference on Automated Reasoning, IJCAR 2008 Sydney, Australia: Springer) 5195: 162–170. doi:10.1007/978-3-540-71070-7_14. 
  15. ^ Korovin, Konstantin (2008). "iProver—an instantiation-based theorem prover for first-order logic (system description)". LNCS (Springer) 5195: 292–298. doi:10.1007/978-3-540-71070-7_24. Retrieved 2009-12-18. 
  16. ^ Ramachandran, Deepak; Pace Reagan and Keith Goolsbery (2005). "First-Orderized ResearchCyc : Expressivity and Efficiency in a Common-Sense Ontology". AAAI Workshop on Contexts and Ontologies: Theory, Practice and Applications (AAAI). 
  17. ^ Ranise, Silvio; David Déharbe (2003). "Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs". ENTCS (4th International Workshop on First-Order Theorem Proving: Elsevier) 86 (1): 109–119. doi:10.1016/S1571-0661(04)80656-X. Retrieved 2009-12-18. 
  18. ^ Denney, Ewen; Bernd Fischer and Johan Schumann (2006). "An Empirical Evaluation of Automated Theorem Provers in Software Certification". International Journal on Artificial Intelligence Tools 15 (1): 81–107. doi:10.1142/s0218213006002576. 

External links[edit]