E(이론프로버)

E (theorem prover)

E는 [1]등식을 갖는 완전 1차 논리에 대한 고성능 정리 프로버입니다.그것은 등식 중첩 미적분에 기초하고 순수하게 등식 패러다임을 사용한다.그것은 다른 정리 프로버들과 통합되었고, 몇몇 정리 증명 대회에서 가장 좋은 위치에 있는 시스템들 중의 하나이다.E는 Stephan Schulz에 의해 개발되었습니다.Stephan Schulz는 원래 TU Munich의 자동 추리 그룹(현재는 Baden-Wurttemberg Cooperative State University Stuttg)에 있습니다.

시스템.

그 시스템은 등가 중첩 미적분에 기초하고 있다.대부분의 다른 현재의 프로버와 달리, 구현은 실제로 순수하게 동등한 패러다임을 사용하며 적절한 평등 추론을 통해 비균등 추론을 시뮬레이션한다.중대한 혁신 공유 용어 추론을 과속( 많은 가능한 방정식의 단순화 단일 작전에서 시행되고 있)[2]여러 효율적인 용어 색인 데이터 구조를 다시 쓰고, 진보된 추론 리터럴 선택 전략과 기계의 다양한 사용 기술 검색 행동을 개선하는 것을 배우는 것을 포함한다.[2][3][4]버전 2.0 이후 E는 다중 정렬 로직을 지원합니다.[5]

E는 C에 구현되어 대부분의 UNIX 변종 및 Cygwin 환경에 이식할 수 있습니다.GNU [6]GPL에서 사용할 수 있습니다.

경합

프로버는 2000년 CNF/MIX 부문에서 우승하고 그 [7]후 줄곧 상위 시스템 중 하나로 마감하는 등 CADE ATP 시스템 대회에서 좋은 성적을 거두고 있습니다.2008년에는 2위를 차지했다.[8]2009년에는 FOF(완전 1차 논리) 및 UEQ(단위 등가 논리) 범주에서 2위를 차지했으며 CNF(결합 논리)[9]에서는 3위(Vampire의 두 가지 버전에 이어)를 차지했다.2010년에는 FOF와 CNF에서 공연을 반복해, 「전체 베스트」[10]시스템으로서 특별상을 수상했다.2011년, CASC-23 E는 CNF 사업부에서 우승하여 UEQ와 LTB에서 [11]2위를 달성하였습니다.

적용들

E는 몇몇 다른 정리프로버에 통합되었다.그것은 뱀파이어, SPASS, CVC4, Z3와 함께 이자벨의 슬레지해머 [12][13]전략의 핵심이다.또한 E는 SInE와[14] LEO-II의[15] 추론 엔진으로 iProver의 [16]클로즈화 시스템으로 사용됩니다.

E의 어플리케이션에는 대규모 온톨로지,[17] 소프트웨어 검증 [18]및 소프트웨어 [19]인증에 대한 논리가 포함됩니다.

레퍼런스

  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 24 March 2009.
  3. ^ Schulz, Stephan (2004). "System Description: E 0.81". Proceedings of the 2nd International Joint Conference on Automated Reasoning. Lecture Notes in Computer Science. Springer. LNAI 3097: 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". Proceedings of the Joint German/Austrian Conference on Artificial Intelligence (KI-2001). Lecture Notes in Computer Science. Springer. LNAI 2174: 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. ^ 2008년 CASC FOF 부문
  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. Retrieved 20 July 2010.
  11. ^ Sutcliffe, Geoff (2011). "The CADE ATP System Competition". University of Miami. 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). 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) (PDF). Lecture Notes in Computer Science. Vol. 5195. 4th International Joint Conference on Automated Reasoning, IJCAR 2008 Sydney, Australia: 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.{{cite book}}: CS1 유지보수: 위치(링크)
  16. ^ Korovin, Konstantin (2008). "iProver—an instantiation-based theorem prover for first-order logic (system description)". Automated Reasoning (PDF). Lecture Notes in Computer Science. Vol. 5195. Springer. pp. 292–298. doi:10.1007/978-3-540-71070-7_24. ISBN 978-3-540-71069-1. Retrieved 18 December 2009.[영구 데드링크]
  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 유지보수: 위치(링크)
  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.

외부 링크