Selecting the Selection

详细信息    查看全文

• 刊名：Lecture Notes in Computer Science
• 出版年：2016
• 出版时间：2016
• 年：2016
• 卷：9706
• 期：1
• 页码：313-329
• 全文大小：327 KB
• 参考文献：1.Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. Revised version in the J. Log. Comput. 4(3), 217–247 (1994). Research Report MPI-I-91-208, Max-Planck-Institut für Informatik, 1991
  2.Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Handbook of Automated Reasoning, vol. I, chapter 2, pp. 19–99. Elsevier Science (2001)
  3.Bachmair, L., Ganzinger, H., Waldmann, U.: Superposition with simplification as a desision. In: Mundici, D., Gottlob, G., Leitsch, A. (eds.) KGC 1993. LNCS, vol. 713, pp. 83–96. Springer, Heidelberg (1993)CrossRef
  4.Dershowitz, N., Plaisted, D.A.: Rewriting. In: Handbook of Automated Reasoning, vol. I, chapter 9, pp. 535–610. Elsevier Science (2001)
  5.Ganzinger, H., de Nivelle, H.: A superposition decision procedure for the guarded fragment with equality. In: 14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, 2–5 July, pp. 295–303. IEEE Computer Society (1999)
  6.Knuth, D., Bendix, P.: Simple word problems in universal algebra. In: Computational Problems in Abstract Algebra, pp. 263–297. Pergamon Press (1970)
  7.Kovács, L., Voronkov, A.: First-order theorem proving and Vampire . In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 1–35. Springer, Heidelberg (2013)CrossRef
  8.Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Handbook of Automated Reasoning, vol. I, chapter 7, pp. 371–443. Elsevier Science (2001)
  9.Reger, G., Suda, M., Voronkov, A.: Playing with AVATAR. In: Reger, G., Suda, M., Voronkov, A. (eds.) CADE-25. LNCS, vol. 9195, pp. 399–415. Springer, Switzerland (2015)CrossRef
  10.Reger, G., Voronkov, A.: The Vampire manual. Technical report (2016, in preperation)
  11.Schulz, S.: E – a brainiac theorem prover. AI Commun. 15(2–3), 111–126 (2002)MATH
  12.Schulz, S.: E 1.8 User Manual (2015). http://​wwwlehre.​dhbw-stuttgart.​de/​sschulz/​WORK/​E_​DOWNLOAD/​V_​1.​9/​eprover.​pdf . Accessed 22 Jan 2016
  13.Sekar, R., Ramakrishnan, I., Voronkov, A.: Term indexing. In: Handbook of Automated Reasoning, vol. II, chapter 26, pp. 1853–1964. Elsevier Science (2001)
  14.Stump, A., Sutcliffe, G., Tinelli, C.: StarExec, a cross community logic solving service (2012). https://​www.​starexec.​org
  15.Sutcliffe, G.: The TPTP problem library and associated infrastructure. J. Autom. Reason. 43(4), 337–362 (2009)CrossRef MATH
  16.Sutcliffe, G., Suttner, C.: The state of CASC. AI Commun. 19(1), 35–48 (2006)MathSciNet MATH
  17.Voronkov, A.: AVATAR: the architecture for first-order theorem provers. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 696–710. Springer, Heidelberg (2014)
  18.Weidenbach, C.: Combining superposition, sorts and splitting. In: Handbook of Automated Reasoning, vol. II, chapter 27, pp. 1965–2013. Elsevier Science (2001)
  
• 作者单位：Kryštof Hoder (15) (16) (17)
  Giles Reger (15)
  Martin Suda (15)
  Andrei Voronkov (15) (16) (17)
  
  15. University of Manchester, Manchester, UK
  16. Chalmers University of Technology, Gothenburg, Sweden
  17. EasyChair, Manchester, UK
  
• 丛书名：Automated Reasoning
• ISBN：978-3-319-40229-1
• 刊物类别：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
• 卷排序：9706

文摘

Modern saturation-based Automated Theorem Provers typically implement the superposition calculus for reasoning about first-order logic with or without equality. Practical implementations of this calculus use a variety of literal selections and term orderings to tame the growth of the search space and help steer proof search. This paper introduces the notion of lookahead selection that estimates (looks ahead) the effect of selecting a particular literal on the number of immediate children of the given clause and selects to minimize this value. There is also a case made for the use of incomplete selection strategies that attempt to restrict the search space instead of satisfying some completeness criteria. Experimental evaluation in the Vampire theorem prover shows that both lookahead selection and incomplete selection significantly contribute to solving hard problems unsolvable by other methods.