Libal, Tomer ; University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)
Steen, Alexander ; University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)
External co-authors :
yes
Language :
English
Title :
Towards a Substitution Tree Based Index for Higher-order Resolution Theorem Provers
Publication date :
July 2016
Event name :
5th Workshop on Practical Aspects of Automated Reasoning
Hendrik Pieter Barendregt. The Lambda Calculus - Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, 1984.
Alexander Baumgartner, Temur Kutsia, Jordi Levy, and Mateu Villaret. A variant of higher-order antiunification. In Leibniz International Proceedings in Informatics (LIPPICS): 24th International Conference on Rewriting Techniques and Applications (RTA 2013): RTA 2013: June 24-26 2013: Eindhoven, The Netherlands, vol. 21, p. 113-127. Dagstuhl Publishing, 2013.
Christoph Benzmüller, Lawrence C. Paulson, Nik Sultana, and Frank Theiß. The Higher-Order Prover LEO-II. Journal of Automated Reasoning, 55(4):389-404, 2015.
Alonzo Church. A formulation of the simple theory of types. J. Symb. Log., 5(2):56-68, 1940.
François Fages. Associative-commutative unification. Journal of Symbolic Computation, 3(3):257-275, 1987.
Peter Graf. Substitution tree indexing. In Rewriting Techniques and Applications, pages 117-131. Springer, 1995.
Peter Graf and Christoph Meyer. Advanced indexing operations on substitution trees. In CADE, volume 1104 of Lecture Notes in Computer Science, pages 553-567. Springer, 1996.
Gérard P. Huet. A unification algorithm for typed lambda-calculus. Theor. Comput. Sci., 1(1):27-57, 1975.
A. Leitsch. The Resolution Calculus. EATCS Monographson Theoretical Computer Science. Springer, 1997.
Alberto Martelli and Ugo Montanari. An efficient unification algorithm. ACM Trans. Program. Lang. Syst., 4(2):258-282, April 1982.
Dale Miller. Unification of simply typed lambda-terms as logic programming. In 8th International Logic Programming Conference, pages 255-269. MIT Press, 1991.
Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. Contextual modal type theory. Under consideration for publication in the ACM Transactions on Computation Logic, 2005.
Frank Pfenning and Carsten Schürmann. System description: Twelfa meta-logical framework for deductive systems. In Automated DeductionCADE-16, pages 202-206. Springer, 1999.
Brigitte Pientka. Higher-order term indexing using substitution trees. ACM Transactions on Computational Logic (TOCL), 11(1):6, 2009.
Brigitte Pientka and Frank Pfenning. Optimizing higher-order pattern unification. In Automated Deduction-CADE-19, pages 473-487. Springer, 2003.
I. V. Ramakrishnan, R. C. Sekar, and Andrei Voronkov. Term indexing. In John Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning (in 2 volumes), pages 1853-1964. Elsevier and MIT Press, 2001.
John Alan Robinson. A machine-oriented logic based on the resolution principle. J. ACM, 12(1):23-41, 1965.
Stephan Schulz. Simple and efficient clause subsumption with feature vector indexing. In Automated Reasoning and Mathematics, volume 7788 of Lecture Notes in Computer Science, pages 45-67. Springer, 2013.
Wayne Snyder and Jean H. Gallier. Higher-order unification revisited: Complete sets of transformations. J. Symb. Comput., 8(1/2):101-140, 1989.
Alexander Steen, Max Wisniewski, and Christoph Benzmüller. Agent-Based HOL Reasoning. In The 5th International Congress on Mathematical Software (ICMS 2016), volume 9725 of LNCS, Berlin, Germany, 2016. Springer. To appear in 2016.
Colin Stirling. Decidability of higher-order matching. Logical Methods in Computer Science, 5(3), 2009.
Frank Theiss and Christoph Benzmüller. Term indexing for the LEO-II prover. In IWIL-6 workshop at LPAR 2006: The 6th International Workshop on the Implementation of Logics, Pnom Penh, Cambodia, 2006.
Andrei Voronkov. Implementing bottom-up procedures with code trees: a case study of forward subsumption. Technical report, 1995.
Max Wisnieski, Alexander Steen, and Christoph Benzmüller. The Leo-III project. In Alexander Bolotov and Manfred Kerber, editors, Joint Automated Reasoning Workshop and Deduktionstreffen, page 38, 2014.