E (theorem prover)

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, now at Baden-Württemberg Cooperative State University Stuttgart.

## Contents

* 1 System
* 2 Competitions
* 3 Applications
* 4 References
* 5 External links

## System

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] Since version 2.0, E supports many-sorted logic. [5]

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

## Competitions

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.[7] In 2008 it came in second place.[8] 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).[9] It repeated the performance in FOF and CNF in 2010, and won a special award as "overall best" system.[10] In the 2011 CASC-23 E won the CNF division and achieved second places in UEQ and LTB.[11]

## Applications

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

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

## References

1. ↑ Schulz, Stephan (2002). "E - A Brainiac Theorem Prover". Journal of AI Communications 15 (2/3): 111–126.
2. ↑ 2.0 2.1 Schulz, Stephan (2008). "Entrants System Descriptions: E 1.0pre and EP 1.0pre". http://www.cs.miami.edu/~tptp/CASC/J4/SystemDescriptions.html#E
1.0pre. Retrieved 2009-03-24.
3. ↑ Schulz, Stephan (2004). "System Description: E 0.81". Automated Reasoning. Lecture Notes in Computer Science. 3097. pp. 223–228. doi:10.1007/978-3-540-25984-8_15. ISBN 978-3-540-22345-0.
4. ↑ Schulz, Stephan (2001). "Learning Search Control Knowledge for Equational Theorem Proving". KI 2001: Advances in Artificial Intelligence. Lecture Notes in Computer Science. 2174. pp. 320–334. doi:10.1007/3-540-45422-5_23. ISBN 978-3-540-42612-7.
5. ↑ "news on E's website". https://wwwlehre.dhbw-stuttgart.de/~sschulz/E/E.html. Retrieved 2017-07-10.
6. ↑ Schulz, Stephan (2008). "The E Equational Theorem Prover". http://www.eprover.org. Retrieved 2009-03-24.
7. ↑ Sutcliffe, Geoff. "The CADE ATP System Competition". http://www.cs.miami.edu/~tptp/CASC/. Retrieved 2009-03-24.
8. ↑ FOF division of CASC in 2008
9. ↑ Sutcliffe, Geoff (2009). "The 4th IJCAR Automated Theorem Proving System Competition--CASC-J4". AI Communications 22 (1): 59–72. doi:10.3233/AIC-2009-0441. http://iospress.metapress.com/content/f94jp575q0h146v7/. Retrieved 2009-12-16.
10. ↑ Sutcliffe, Geoff (2010). "The CADE ATP System Competition". University of Miami. http://www.cs.miami.edu/~tptp/CASC/J5/. Retrieved 20 July 2010.
11. ↑ Sutcliffe, Geoff (2011). "The CADE ATP System Competition". University of Miami. http://www.cs.miami.edu/~tptp/CASC/23/. Retrieved 14 August 2011.
12. ↑ 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. http://ttvsi.gilith.com/ttvsi.pdf#page=39. Retrieved 2009-12-19.
13. ↑ Meng, Jia; Lawrence C. Paulson (2004). Experiments on Supporting Interactive Proof Using Resolution. Lecture Notes in Computer Science. 3097. Springer. pp. 372–384. doi:10.1007/978-3-540-25984-8_28. ISBN 978-3-540-22345-0.
14. ↑ Sutcliffe, Geoff (2009). The 4th IJCAR ATP System Competition. http://www.cs.miami.edu/~tptp/CASC/J4/Proceedings.pdf. Retrieved 2009-12-18.
15. ↑ 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)". Automated Reasoning. Lecture Notes in Computer Science. 5195. Springer. pp. 162–170. doi:10.1007/978-3-540-71070-7_14. ISBN 978-3-540-71069-1. http://www.ags.uni-sb.de/~chris/papers/C26.pdf. Retrieved 20 December 2009.
16. ↑ Korovin, Konstantin (2008). "iProver—an instantiation-based theorem prover for first-order logic". Automated Reasoning. Lecture Notes in Computer Science. 5195. pp. 292–298. doi:10.1007/978-3-540-71070-7_24. ISBN 978-3-540-71069-1.
17. ↑ Ramachandran, Deepak; Pace Reagan; 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). https://www.aaai.org/Papers/Workshops/2005/WS-05-01/WS05-01-006.pdf.
18. ↑ Ranise, Silvio; David Déharbe (2003). "Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs". Electronic Notes in Theoretical Computer Science (4th International Workshop on First-Order Theorem Proving: Elsevier) 86 (1): 109–119. doi:10.1016/S1571-0661(04)80656-X.
19. ↑ Denney, Ewen; Bernd Fischer; 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. http://eprints.ecs.soton.ac.uk/12355/. Retrieved 19 December 2009.

## External links

* E home page
* E's developer

0.00

(0 votes)

Original source: https://en.wikipedia.org/wiki/E (theorem prover). Read more

|

Retrieved from "https://handwiki.org/wiki/index.php?title=Software:E_(theorem_prover)&oldid=696343"