Higher Order Logic; Automated Reasoning; LEO Prover; Lambda-Calculus
Disciplines :
Sciences informatiques
Auteur, co-auteur :
STEEN, Alexander ; University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)
BENZMÜLLER, Christoph ; University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)
Co-auteurs externes :
no
Langue du document :
Anglais
Titre :
There Is No Best Beta-Normalization Strategy for Higher-Order Reasoners
Date de publication/diffusion :
novembre 2015
Nom de la manifestation :
20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR)
Lieu de la manifestation :
Suva, Fidji
Date de la manifestation :
November 24-28, 2015
Manifestation à portée :
International
Titre de l'ouvrage principal :
Logic for Programming, Artificial Intelligence, and Reasoning (LPAR)
Abadi, M., Cardelli, L., Curien, P.L., Levy, J.J.: Explicit substitutions. In: Proceedings of the 17th Symposium on Principles of Programming Languages, POPL 1990, pp. 31–46. ACM, New York, NY, USA (1990)
Benzmüller, C., Raths, T.: HOL based first-order modal logic provers. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19 2013. LNCS, vol. 8312, pp. 127–136. Springer, Heidelberg (2013)
Bruijn, N.G.D.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem. INDAG. MATH 34, 381–392 (1972)
Cervesato, I., Pfenning, F.: A linear spine calculus. J. Logic Comput. 13(5), 639–688 (2003)
Church, A.: A set of postulates for the foundation of logic. Ann. Math. 33(2), 346–366 (1932)
Church, A.: A set of postulates for the foundation of logic. Second Paper. Ann. Math. 34(4), 839–864 (1933)
Church, A.: A formulation of the simple theory of types. J. Symb. Log. 5(2), 56–68 (1940)
Gacek, A.: The abella interactive theorem prover (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 154–161. Springer, Heidelberg (2008)
Girard, J.: Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur. Ph.D. thesis, Université Paris VII (1972)
Liang, C., Nadathur, G., Qi, X.: Choices in representation and reduction strategies for lambda terms in intensional contexts. J. Autom. Reasoning 33(2), 89–132 (2004)
Nadathur, G.: A fine-grained notation for lambda terms and its use in intensional operations. J. Funct. Logic Program. 1999(2), 1–62 (1999)
Nadathur, G., Mitchell, D.J.: System description: teyjus - a compiler and abstract machine based implementation of λprolog. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 287–291. Springer, Heidelberg (1999)
Pfenning, F., Schürmann, C.: System description: Twelf - a meta-logical framework for deductive systems. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 202–206. Springer, Heidelberg (1999)
Pientka, B., Dunfield, J.: Beluga: a framework for programming and reasoning with deductive systems (system description). In: Giesl, J., Hähnle, R. (eds.) IJCAR 2010. LNCS, vol. 6173, pp. 15–21. Springer, Heidelberg (2010)
Raths, T., Otten, J.: The QMLTP problem library for first-order modal logics. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 454–461. Springer, Heidelberg (2012)
Reynolds, J.C.: Towards a theory of type structure. In: Robinet, B. (ed.) Symposium on Programming. LNCS, vol. 19, pp. 408–423. Springer, Heidelberg (1974)
Reynolds, J.C.: An introduction to polymorphic lambda calculus. In: Logical Foundations of Functional Programming, pp. 77–86. Addison-Wesley (1994)
Steen, A.: Efficient Data Structures for Automated Theorem Proving in Expressive Higher-Order Logics. Master’s thesis, Freie Universität Berlin, Berlin (2014)
Sutcliffe, G.: The TPTP problem library and associated infrastructure: The FOF and CNF parts, v3.5.0. J. Autom. Reasoning 43(4), 337–362 (2009)
Sutcliffe, G., Benzmüller, C.: Automated reasoning in higher-order logic using the TPTP THF infrastructure. J. Formalized Reasoning 3(1), 1–27 (2010)
Wisniewski, M., Steen, A., Benzmüller, C.: LeoPARD — A generic platform for the implementation of higher-order reasoners. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS, vol. 9150, pp. 325–330. Springer, Heidelberg (2015)
