摘要: We present a higher-order term indexing strategy based on substitution trees. The is in linear patterns where computationally expensive parts are delayed. Insertion of terms into the index computing most specific generalization two patterns. Retrieving matching This structure implemented as part Twelf system to speed-up execution tabled higher-logic programming interpreter. Experimental results show substantial performance improvements, between 100% and over 800%.
springer.com
core.ac.uk
sci-hub.st 参考文章(23)
Brigitte Pientka, Memoization-Based Proof Search in LF: An Experimental Evaluation of a Prototype Electronic Notes in Theoretical Computer Science. ,vol. 70, pp. 110- 123 ,(2002) , 10.1016/S1571-0661(04)80509-7
Brigitte Pientka, Frank Pfenning, Optimizing Higher-Order Pattern Unification conference on automated deduction. pp. 473- 487 ,(2003) , 10.1007/978-3-540-45085-6_40
Peter Graf, Substitution Tree Indexing rewriting techniques and applications. pp. 117- 131 ,(1995) , 10.1007/3-540-59200-8_52
Andrei Voronkov, Alan Robinson, Handbook of automated reasoning Elsevier B.V.. ,(2001) , 10.1016/B978-044450813-3/50006-0
Lucas Dixon, Jacques Fleuriot, IsaPlanner: A Prototype Proof Planner in Isabelle conference on automated deduction. pp. 279- 283 ,(2003) , 10.1007/978-3-540-45085-6_22
Harald Ganzinger, Frank Pfenning, Carsten Schürmann, System Description: Twelf - A Meta-Logical Framework for Deductive Systems conference on automated deduction. pp. 202- 206 ,(1999) , 10.1007/3-540-48660-7_14
Robert Harper, Furio Honsell, Gordon Plotkin, A framework for defining logics Journal of the ACM (JACM). ,vol. 40, pp. 143- 184 ,(1993) , 10.1145/138027.138060
Aleksandar Nanevski, Brigitte Pientka, Frank Pfenning, A modal foundation for meta-variables Proceedings of the 2003 workshop on Mechanized reasoning about languages with variable binding - MERLIN '03. pp. 1- 6 ,(2003) , 10.1145/976571.976582
MICHAEL HANUS, CHRISTIAN PREHOFER, Higher-order narrowing with definitional trees Journal of Functional Programming. ,vol. 9, pp. 33- 75 ,(1999) , 10.1017/S0956796899003330
Lawrence C. Paulson, Natural deduction as higher-order resolution Journal of Logic Programming. ,vol. 3, pp. 237- 258 ,(1986) , 10.1016/0743-1066(86)90015-4