On the Evaluation of Indexing Techniques for Theorem Proving
作者： Robert Nieuwenhuis , Thomas Hillenbrand , Alexandre Riazanov , Andrei Voronkov , None
关键词:
摘要: The problem of term indexing can be formulated abstractly as follows (see [19]). Given a set L indexed terms, binary relation R over terms (called the retrieval condition) and t query term), identify subset M that consists l such R(l; t) holds. Terms in will called candidate terms. Typical conditions used first-order theorem proving are matching, generalization, unifiability, syntactic equality. Such is interleaved with insertion to L, deletion them from L.
springer.com
manchester.ac.uk参考文章(22)
Bart Selman, David Mitchell, Hector Levesque, Hard and easy distributions of SAT problems national conference on artificial intelligence. pp. 459- 465 ,(1992)
Daniel Rolf, Algorithms for the Satisfiability Problem ,(2018)
Hans Jürgen Ohlbach, Abstraction tree indexing for terms european conference on artificial intelligence. pp. 479- 484 ,(1990)
W.W. McCune, OTTER 3.0 Reference Manual and Guide Argonne National Laboratory. ,(1994) , 10.2172/10129052
Peter Graf, Extended Path-Indexing conference on automated deduction. pp. 514- 528 ,(1994) , 10.1007/3-540-58156-1_37
Mark E. Stickel, The Path-Indexing Method for Indexing Terms Defense Technical Information Center. ,(1989) , 10.21236/ADA460990
Paul Walton Purdom, Cynthia A. Brown, Fast many-to-one matching algorithms Rewriting Techniques and Applications. pp. 407- 416 ,(1985) , 10.1007/3-540-15976-2_21
Thomas Hillenbrand, Arnim Buch, Roland Vogt, Bernd Löchner, WALDMEISTER - High-Performance Equational Deduction Journal of Automated Reasoning. ,vol. 18, pp. 265- 270 ,(1997) , 10.1023/A:1005872405899
Peter Graf, Substitution Tree Indexing rewriting techniques and applications. pp. 117- 131 ,(1995) , 10.1007/3-540-59200-8_52