“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.

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 [https://github.com/Z3Prover/z3 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. ^{{Cite journal| first=Stephan| last=Schulz| title=E - A Brainiac Theorem Prover| journal=Journal of AI Communications| volume=15| issue=2/3| pages=111–126| year=2002}}
2. ^¹{{Cite web|url=http://www.cs.miami.edu/~tptp/CASC/J4/SystemDescriptions.html#E---1.0pre|title=Entrants System Descriptions: E 1.0pre and EP 1.0pre|last=Schulz|first=Stephan|year=2008|accessdate=2009-03-24}}
3. ^{{Cite journal|last=Schulz|first=Stephan|year=2004|title=System Description: E 0.81|journal=Proceedings of the 2nd International Joint Conference on Automated Reasoning|publisher=Springer|volume=LNAI 3097|pages=223–228|doi=10.1007/978-3-540-25984-8_15|series=Lecture Notes in Computer Science|isbn=978-3-540-22345-0}}
4. ^{{Cite journal|last=Schulz|first=Stephan|year=2001|title=Learning Search Control Knowledge for Equational Theorem Proving|journal=Proceedings of the Joint German/Austrian Conference on Artificial Intelligence (KI-2001)|publisher=Springer|volume=LNAI 2174|pages=320–334|doi=10.1007/3-540-45422-5_23|series=Lecture Notes in Computer Science|isbn=978-3-540-42612-7}}
5. ^{{Cite web|url=https://wwwlehre.dhbw-stuttgart.de/~sschulz/E/E.html|accessdate=2017-07-10|title=news on E's website}}
6. ^{{Cite web|url=http://www.eprover.org|title=The E Equational Theorem Prover|last=Schulz|first=Stephan|year=2008|accessdate=2009-03-24}}
7. ^{{Cite web|url=http://www.cs.miami.edu/~tptp/CASC/|title=The CADE ATP System Competition|last=Sutcliffe|first=Geoff|accessdate=2009-03-24}}
8. ^FOF division of CASC in 2008
9. ^{{Cite journal|last=Sutcliffe|first=Geoff|year=2009|title=The 4th IJCAR Automated Theorem Proving System Competition--CASC-J4|journal=AI Communications|volume=22|issue=1|pages=59–72|url=http://iospress.metapress.com/content/f94jp575q0h146v7/|accessdate=2009-12-16}}
10. ^{{Cite web|last=Sutcliffe|first=Geoff|title=The CADE ATP System Competition|url=http://www.cs.miami.edu/~tptp/CASC/J5/|publisher=University of Miami|accessdate=20 July 2010|year=2010}}
11. ^{{Cite web|last=Sutcliffe|first=Geoff|title=The CADE ATP System Competition|url=http://www.cs.miami.edu/~tptp/CASC/23/|publisher=University of Miami|accessdate=14 August 2011|year=2011}}
12. ^{{Cite journal|last=Paulson |first=Lawrence C. |year=2008|title=Automation for Interactive Proof: Techniques, Lessons and Prospects|journal=Tools and Techniques for Verification of System Infrastructure - A Festschrift in Honour of Professor Michael J. C. Gordon FRS|pages=29–30|url=http://ttvsi.gilith.com/ttvsi.pdf#page=39|accessdate=2009-12-19}}
13. ^{{Cite journal|last=Meng|first=Jia|author2=Lawrence C. Paulson|date=2004|title=Experiments on Supporting Interactive Proof Using Resolution |journal=LNCS|publisher=Springer|volume=3097|pages=372–384|doi=10.1007/978-3-540-25984-8_28|series=Lecture Notes in Computer Science|isbn=978-3-540-22345-0|citeseerx=10.1.1.62.5009}}
14. ^{{Cite book|last=Sutcliffe|first=Geoff|title=The 4th IJCAR ATP System Competition|year=2009|url=http://www.cs.miami.edu/~tptp/CASC/J4/Proceedings.pdf|accessdate=2009-12-18|display-authors=etal}}
15. ^{{Cite journal|last=Benzmüller|first=Christoph|author2=Lawrence C. Paulson |author3=Frank Theiss |author4=Arnaud Fietzke |year=2008|title=LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)|journal=LNCS|publisher=Springer|location=4th International Joint Conference on Automated Reasoning, IJCAR 2008 Sydney, Australia|volume=5195|pages=162–170|url=http://www.ags.uni-sb.de/~chris/papers/C26.pdf|doi=10.1007/978-3-540-71070-7_14|series=Lecture Notes in Computer Science|isbn=978-3-540-71069-1}}
16. ^{{Cite journal|last=Korovin|first=Konstantin|year=2008|title=iProver—an instantiation-based theorem prover for first-order logic (system description)|journal=LNCS|publisher=Springer|volume=5195|pages=292–298|url=http://www.cs.manchester.ac.uk/~korovink/my_pub/iprover_descr_08.pdf|accessdate=2009-12-18|doi=10.1007/978-3-540-71070-7_24|series=Lecture Notes in Computer Science|isbn=978-3-540-71069-1}}
17. ^{{Cite journal|last=Ramachandran|first=Deepak |author2=Pace Reagan |author3=Keith Goolsbery|year=2005|title=First-Orderized ResearchCyc : Expressivity and Efficiency in a Common-Sense Ontology|journal=AAAI Workshop on Contexts and Ontologies: Theory, Practice and Applications|publisher=AAAI|url=https://www.aaai.org/Papers/Workshops/2005/WS-05-01/WS05-01-006.pdf}}
18. ^{{Cite journal|last=Ranise|first=Silvio|author2=David Déharbe|year=2003|title=Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs|journal=ENTCS|publisher=Elsevier|location=4th International Workshop on First-Order Theorem Proving|volume=86|issue=1|pages=109–119|url=http://www.sciencedirect.com/science?_ob=ArticleURL&_udi=B75H1-4DDWKNY-ND&_user=10&_rdoc=1&_fmt=&_orig=search&_sort=d&_docanchor=&view=c&_rerunOrigin=scholar.google&_acct=C000050221&_version=1&_urlVersion=0&_userid=10&md5=7c3d4c7c9b56361f82b30edf963c5443|archive-url=https://archive.today/20120909073320/http://www.sciencedirect.com/science?_ob=ArticleURL&_udi=B75H1-4DDWKNY-ND&_user=10&_rdoc=1&_fmt=&_orig=search&_sort=d&_docanchor=&view=c&_rerunOrigin=scholar.google&_acct=C000050221&_version=1&_urlVersion=0&_userid=10&md5=7c3d4c7c9b56361f82b30edf963c5443|dead-url=yes|archive-date=2012-09-09|accessdate=2009-12-18|doi=10.1016/S1571-0661(04)80656-X}}
19. ^{{Cite journal|last=Denney|first=Ewen |author2=Bernd Fischer |author3=Johan Schumann|year=2006|title=An Empirical Evaluation of Automated Theorem Provers in Software Certification|journal=International Journal on Artificial Intelligence Tools|volume=15|issue=1|pages=81–107|url=http://eprints.ecs.soton.ac.uk/12355/|doi=10.1142/s0218213006002576|citeseerx=10.1.1.163.4861 }}

System

Competitions

Applications

References

External links