Extending E Prover with Similarity Based Clause Selection Strategies

详细信息    查看全文

• 关键词：Automated theorem proving ; Large theory reasoning ; Clause selection
• 刊名：Lecture Notes in Computer Science
• 出版年：2016
• 出版时间：2016
• 年：2016
• 卷：9791
• 期：1
• 页码：151-156
• 全文大小：385 KB
• 参考文献：1.Alama, J., et al.: Premise selection for mathematics by corpus analysis and kernel methods. J. Autom. Reason. 52(2), 191–213 (2014)MathSciNet CrossRef MATH
  2.Kaliszyk, C., Urban, J., Vyskocil, J.: Efficient semantic features for automated reasoning over large theories. In: IJCAI, vol. 15 (2015)
  3.Leskovec, J., Rajaraman, A., Ullman, J.D.: Mining of Massive Datasets, 2nd edn. Cambridge University Press, Cambridge (2014)CrossRef
  4.Levenshtein, V.I.: Binary codes capable of correcting deletions, insertions and reversals. Sov. Phys. Dokl. 10, 707 (1966)MathSciNet MATH
  5.McCune, W.W.: Otter 3.0 Reference Manual and Guide, vol. 9700. Argonne National Laboratory, Argonne (1994)CrossRef
  6.Schulz, S.: E - a brainiac theorem prover. AI Commun. 15(2), 111–126 (2002)MATH
  7.Urban, J.: BliStr: the blind strategymaker. In: Global Conference on Artificial Intelligence, GCAI 2015, vol. 36, pp. 312–319. EasyChair (2015)
  8.Zhang, K., Shasha, D.: Simple fast algorithms for the editing distance between trees and related problems. SIAM J. Comput. 18(6), 1245–1262 (1989)MathSciNet CrossRef MATH
  
• 作者单位：Jan Jakubův (18)
  Josef Urban (18)
  
  18. CIIRC, Czech Technical University, Prague, Czech Republic
  
• 丛书名：Intelligent Computer Mathematics
• ISBN：978-3-319-42547-4
• 刊物类别：Computer Science
• 刊物主题：Artificial Intelligence and Robotics
  Computer Communication Networks
  Software Engineering
  Data Encryption
  Database Management
  Computation by Abstract Devices
  Algorithm Analysis and Problem Complexity
  
• 出版者：Springer Berlin / Heidelberg
• ISSN：1611-3349
• 卷排序：9791

文摘

E prover is a state-of-the-art theorem prover for first-order logic with equality. E prover is built around a saturation loop, where new clauses are derived by inference rules from previously derived clauses. Selection of clauses for the inference provides the main source of non-determinism and an important choice-point of the loop where the right choice can dramatically influence the proof search. In this work we extend E Prover with several new clause selection strategies based on similarity of a clause with the conjecture. In particular, clauses which are more related to the conjecture are preferred. We implement different strategies that define the relationship with a conjecture in different ways. We provide an implementation of the proposed selection strategies and we evaluate their efficiency on an extensive benchmark set.