E (theorem prover)

Last updated

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

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]

Related Research Articles

Automated theorem proving is a subfield of automated reasoning and mathematical logic dealing with proving mathematical theorems by computer programs. Automated reasoning over mathematical proof was a major impetus for the development of computer science.

In computer science, formal methods are mathematically rigorous techniques for the specification, development, analysis, and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.

Logic for Computable Functions (LCF) is an interactive automated theorem prover developed at Stanford and Edinburgh by Robin Milner and collaborators in early 1970s, based on the theoretical foundation of logic of computable functions previously proposed by Dana Scott. Work on the LCF system introduced the general-purpose programming language ML to allow users to write theorem-proving tactics, supporting algebraic data types, parametric polymorphism, abstract data types, and exceptions.

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. It can a participate as part of an automated theorem proving system. The software is primarily written in the Haskell programming language. It is released under the terms of the GNU General Public License and is free.

Vampire is an automatic theorem prover for first-order classical logic developed in the Department of Computer Science at the University of Manchester. Up to Version 3, it was developed by Andrei Voronkov together with Kryštof Hoder and previously with Alexandre Riazanov. Since Version 4, the development has involved a wider international team including Laura Kovacs, Giles Reger, and Martin Suda. Since 1999 it has won at least 53 trophies in the CADE ATP System Competition, the "world cup for theorem provers", including the most prestigious FOF division and the theory-reasoning TFA division.

<span class="mw-page-title-main">Proof assistant</span> Software tool to assist with the development of formal proofs by human-machine collaboration

In computer science and mathematical logic, a proof assistant or interactive theorem prover is a software tool to assist with the development of formal proofs by human-machine collaboration. This involves some sort of interactive proof editor, or other interface, with which a human can guide the search for proofs, the details of which are stored in, and some steps provided by, a computer.

Carew Arthur Meredith, usually cited as C. A. Meredith, was an influential Irish logician, who worked in Trinity College, Dublin from 1943 to 1964. His work on condensed detachment is influential in modern research.

In computer science, in particular in knowledge representation and reasoning and metalogic, the area of automated reasoning is dedicated to understanding different aspects of reasoning. The study of automated reasoning helps produce computer programs that allow computers to reason completely, or nearly completely, automatically. Although automated reasoning is considered a sub-field of artificial intelligence, it also has connections with theoretical computer science and philosophy.

The International Joint Conference on Automated Reasoning (IJCAR) is a series of conferences on the topics of automated reasoning, automated deduction, and related fields. It is organized semi-regularly as a merger of other meetings. IJCAR replaces those independent conferences in the years it takes place. The conference is organized by the organizers of the Conference on Automated Deduction (CADE), and CADE has always been one of the conferences partaking in IJCAR.

In computer science and mathematical logic, satisfiability modulo theories (SMT) is the problem of determining whether a mathematical formula is satisfiable. It generalizes the Boolean satisfiability problem (SAT) to more complex formulas involving real numbers, integers, and/or various data structures such as lists, arrays, bit vectors, and strings. The name is derived from the fact that these expressions are interpreted within ("modulo") a certain formal theory in first-order logic with equality. SMT solvers are tools that aim to solve the SMT problem for a practical subset of inputs. SMT solvers such as Z3 and cvc5 have been used as a building block for a wide range of applications across computer science, including in automated theorem proving, program analysis, program verification, and software testing.

<span class="mw-page-title-main">John Alan Robinson</span> American computer scientist

John Alan Robinson was a philosopher, mathematician, and computer scientist. He was a professor emeritus at Syracuse University.

In the computer science fields of knowledge engineering and ontology, the Sigma knowledge engineering environment (SigmaKEE) is an open source computer program for the development of formal ontologies. It is designed for use with the Suggested Upper Merged Ontology. It originally included only the Vampire theorem prover as its core deductive inference engine, but now allows use of many other provers that have participated in the CASC/CADE competitions.

SPASS is an automated theorem prover for first-order logic with equality developed at the Max Planck Institute for Computer Science and using the superposition calculus. The name originally stood for Synergetic Prover Augmenting Superposition with Sorts. The theorem-proving system is released under the FreeBSD license.

<span class="mw-page-title-main">Geoff Sutcliffe</span>

Geoff Sutcliffe is a US-based computer scientist working in the field of automated reasoning. He was born in the former British colony of Northern Rhodesia , grew up in South Africa, and earned his PhD in Australia. Sutcliffe currently works at the University of Miami, and is of both British and Australian nationality.

The CADE ATP System Competition (CASC) is a yearly competition of fully automated theorem provers for classical logic CASC is associated with the Conference on Automated Deduction and the International Joint Conference on Automated Reasoning organized by the Association for Automated Reasoning. It has inspired similar competition in related fields, in particular the successful SMT-COMP competition for satisfiability modulo theories, the SAT Competition for propositional reasoners, and the modal logic reasoning competition.

<span class="mw-page-title-main">Andrei Voronkov</span>

Andrei Anatolievič Voronkov is a Professor of Formal methods in the Department of Computer Science at the University of Manchester.

TPTP is a freely available collection of problems for automated theorem proving. It is used to evaluate the efficacy of automated reasoning algorithms. Problems are expressed in a simple text-based format for first order logic or higher-order logic. TPTP is used as the source of some problems in CASC.

Deepak Kapur is a Distinguished Professor in the Department of Computer Science at the University of New Mexico.

Modal clausal form, also known as separated normal form by modal levels (SNFml) and Mints normal form, is a normal form for modal logic formulae.

References

  1. ↑ Schulz, Stephan (2002). "E – A Brainiac Theorem Prover". Journal of AI Communications. 15 (2/3): 111–126.
  2. 1 2 Schulz, Stephan (2008). "Entrants System Descriptions: E 1.0pre and EP 1.0pre". Archived from the original on 15 June 2009. Retrieved 24 March 2009.
  3. ↑ Schulz, Stephan (2004). "System Description: E 0.81". Automated Reasoning. Lecture Notes in Computer Science. Vol. 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. Vol. 2174. pp. 320–334. doi:10.1007/3-540-45422-5_23. ISBN   978-3-540-42612-7.
  5. ↑ "news on E's website" . Retrieved 10 July 2017.
  6. ↑ Schulz, Stephan (2008). "The E Equational Theorem Prover" . Retrieved 24 March 2009.
  7. ↑ Sutcliffe, Geoff. "The CADE ATP System Competition". Archived from the original on 2 March 2009. Retrieved 24 March 2009.
  8. ↑ "FOF division of CASC in 2008". Archived from the original on 15 June 2009. Retrieved 19 December 2009.
  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 . Retrieved 16 December 2009.
  10. ↑ Sutcliffe, Geoff (2010). "The CADE ATP System Competition". University of Miami. Archived from the original on 29 June 2010. Retrieved 20 July 2010.
  11. ↑ Sutcliffe, Geoff (2011). "The CADE ATP System Competition". University of Miami. Archived from the original on 12 August 2011. Retrieved 14 August 2011.
  12. ↑ Paulson, Lawrence C. (2008). "Automation for Interactive Proof: Techniques, Lessons and Prospects" (PDF). Tools and Techniques for Verification of System Infrastructure – A Festschrift in Honour of Professor Michael J. C. Gordon FRS: 29–30. Retrieved 19 December 2009.
  13. ↑ Meng, Jia; Lawrence C. Paulson (2004). Experiments on Supporting Interactive Proof Using Resolution. Lecture Notes in Computer Science. Vol. 3097. Springer. pp. 372–384. CiteSeerX   10.1.1.62.5009 . doi:10.1007/978-3-540-25984-8_28. ISBN   978-3-540-22345-0.
  14. ↑ Sutcliffe, Geoff; et al. (2009). The 4th IJCAR ATP System Competition (PDF). Archived from the original (PDF) on 17 June 2009. Retrieved 18 December 2009.
  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 (PDF). Lecture Notes in Computer Science. Vol. 5195. Springer. pp. 162–170. doi:10.1007/978-3-540-71070-7_14. ISBN   978-3-540-71069-1. Archived from the original (PDF) on 15 June 2011. 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. Vol. 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" (PDF). AAAI Workshop on Contexts and Ontologies: Theory, Practice and Applications. AAAI.
  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 .{{cite journal}}: CS1 maint: location (link)
  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. CiteSeerX   10.1.1.163.4861 . doi:10.1142/s0218213006002576. Archived from the original on 24 February 2012. Retrieved 19 December 2009.
This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.