nach oben

Erschienen in:

2015 | OriginalPaper | Buchkapitel

There Is No Best \(\beta \)-Normalization Strategy for Higher-Order Reasoners

verfasst von : Alexander Steen, Christoph Benzmüller

Erschienen in: Logic for Programming, Artificial Intelligence, and Reasoning

Verlag: Springer Berlin Heidelberg

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

The choice of data structures for the internal representation of terms in logical frameworks and higher-order theorem provers is a crucial low-level factor for their performance. We propose a representation of terms based on a polymorphically typed nameless spine data structure in conjunction with perfect term sharing and explicit substitutions.

In related systems the choice of a \(\beta \)-normalization method is usually statically fixed and cannot be adjusted to the input problem at runtime. The predominant strategies are hereby implementation specific adaptions of leftmost-outermost normalization. We introduce several different \(\beta \)-normalization strategies and empirically evaluate their performance by reduction step measurement on about 7000 heterogeneous problems from different (TPTP) domains.

Our study shows that there is no generally best \(\beta \)-normalization strategy and that for different problem domains, different best strategies can be identified. The evaluation results suggest a problem-dependent choice of a preferred \(\beta \)-normalization strategy for higher-order reasoning systems.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel On the Expressive Power of Communication Primitives in Parameterised Systems

Nächstes Kapitel Fine Grained SMT Proofs for the Theory of Fixed-Width Bit-Vectors

The LeoPARD framework is freely available under BSD license and can be downloaded at https://github.com/cbenzmueller/LeoPARD.

The archive of semantically embedded S4-formulae from QMLTP can be found at http://page.mi.fu-berlin.de/cbenzmueller/papers/THF-S4-ALL.zip.

The complete evaluation results can be found at http://inf.fu-berlin.de/~lex/files/betaresults.pdf.

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) CrossRef

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)CrossRef

Cervesato, I., Pfenning, F.: A linear spine calculus. J. Logic Comput. 13(5), 639–688 (2003)MATHMathSciNetCrossRef

Church, A.: A set of postulates for the foundation of logic. Ann. Math. 33(2), 346–366 (1932)MathSciNetCrossRef

Church, A.: A set of postulates for the foundation of logic. Second Paper. Ann. Math. 34(4), 839–864 (1933)MATHMathSciNetCrossRef

Church, A.: A formulation of the simple theory of types. J. Symb. Log. 5(2), 56–68 (1940)MathSciNetCrossRef

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) CrossRef

Girard, J.: Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur. Ph.D. thesis, Université Paris VII (1972)

10.

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)MATHMathSciNetCrossRef

11.

Nadathur, G.: A fine-grained notation for lambda terms and its use in intensional operations. J. Funct. Logic Program. 1999(2), 1–62 (1999)

12.

Nadathur, G., Mitchell, D.J.: System description: teyjus - a compiler and abstract machine based implementation of \(\lambda \)prolog. In: Ganzinger, H. (ed.) CADE 1999. LNCS (LNAI), vol. 1632, pp. 287–291. Springer, Heidelberg (1999) CrossRef

13.

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) CrossRef

14.

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) CrossRef

15.

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) CrossRef

16.

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)CrossRef

17.

Reynolds, J.C.: An introduction to polymorphic lambda calculus. In: Logical Foundations of Functional Programming, pp. 77–86. Addison-Wesley (1994)

18.

Steen, A.: Efficient Data Structures for Automated Theorem Proving in Expressive Higher-Order Logics. Master’s thesis, Freie Universität Berlin, Berlin (2014)

19.

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)MATHCrossRef

20.

Sutcliffe, G., Benzmüller, C.: Automated reasoning in higher-order logic using the TPTP THF infrastructure. J. Formalized Reasoning 3(1), 1–27 (2010)MATH

21.

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) CrossRef

Titel: There Is No Best -Normalization Strategy for Higher-Order Reasoners
verfasst von: Alexander Steen
Christoph Benzmüller
Verlag: Springer Berlin Heidelberg
Buch: Logic for Programming, Artificial Intelligence, and Reasoning
Print ISBN: 978-3-662-48898-0

Electronic ISBN: 978-3-662-48899-7

Copyright-Jahr: 2015
DOI: https://doi.org/10.1007/978-3-662-48899-7_23

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner