E equational theorem prover

From Seo Wiki - Search Engine Optimization and Programming Languages
Jump to navigationJump to search

E is a modern, high performance theorem prover for full first-order logic with equality.[1] It's 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 has been developed by Stephan Schulz, originally in the Automated Reasoning Group at TU Munich.


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.[3][2][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

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]

Applications

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

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

Author

Template:Infobox Scientist

Stephan Schulz is a German computer scientist working in the field of automated reasoning. In 2002, Schulz was recognized by the Florida Artificial Intelligence Research Society with the best paper award for his work A Comparison of Different Techniques for Grounding Near-Propositional CNF Formulae. [17] Together with Geoff Sutcliffe, Schulz founded and has been organizing the ES* Workshop series, a venue for presentation and publishing of practically oriented Automated Reasoning research.[18] He has been significantly involved with the IWIL Workshop series on implementations of logics, and is a member of the Steering Committee of the International Workshop on First-Order Theorem Proving.[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". Proceedings of the 2nd International Joint Conference on Automated Reasoning (Springer) LNAI 3097: 223–228. 
  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. 
  5. ↑ Schulz, Stephan (2008). "The E Equational Theorem Prover". http://www.eprover.org. Retrieved 2009-03-24. 
  6. ↑ Sutcliffe, Geoff. "The CADE ATP System Competition". http://www.cs.miami.edu/~tptp/CASC/. 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. http://iospress.metapress.com/content/f94jp575q0h146v7/. Retrieved 2009-12-16. 
  9. ↑ 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. 
  10. ↑ Meng, Jia; Lawrence C. Paulson (2004). "Experiments on Supporting Interactive Proof Using Resolution". LNCS (Springer) 3097: 372-384}. http://www.springerlink.com/content/btx6b2rrewvmjc9y/. Retrieved 2009-12-16. 
  11. ↑ Sutcliffe, Geoff; et al (2009). The 4th IJCAR ATP System Competition. http://www.cs.miami.edu/~tptp/CASC/J4/Proceedings.pdf. Retrieved 2009-12-18. 
  12. ↑ Benzmüller, Christoph; Lawrence C. Paulson, Frank Theiss , and 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. http://www.ags.uni-sb.de/~chris/papers/C26.pdf. 
  13. ↑ Korovin, Konstantin (2008). "iProver—an instantiation-based theorem prover for first-order logic (system description)". LNCS (Springer) 5195: 292–298. http://www.cs.manchester.ac.uk/~korovink/my_pub/iprover_descr_08.pdf. Retrieved 2009-12-18. 
  14. ↑ 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). https://www.aaai.org/Papers/Workshops/2005/WS-05-01/WS05-01-006.pdf. 
  15. ↑ 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. 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. Retrieved 2009-18-12. 
  16. ↑ 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. http://eprints.ecs.soton.ac.uk/12355/. 
  17. ↑ "Flairs 2002 Conference Report". AI Magazine. 2002-12. http://www.accessmylibrary.com/coms2/summary_0286-27024342_ITM. 
  18. ↑ Schulz, Stephan. "Empirically Successful Topics in Automated Deduction". http://www.eprover.org/EVENTS/es_series.html. Retrieved 19 December 2009. 
  19. ↑ "Home page of FTP workshops/Steering Committee". http://www.csc.liv.ac.uk/FTP-WS/index.html#committee. Retrieved 19 December 2009. 

External links

If you like SEOmastering Site, you can support it by - BTC: bc1qppjcl3c2cyjazy6lepmrv3fh6ke9mxs7zpfky0 , TRC20 and more...

→

Retrieved from "https://mail.seomastering.com:443/w/index.php?title=E_equational_theorem_prover&oldid=15089"