Skip to main content
SpringerLink
Log in

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

  • Conference paper
  • First Online:
Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2015)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9450))

Included in the following conference series:

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.

This work has been supported by the German National Research Foundation (DFG) under grant BE 2501/11-1 (Leo-III).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

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

  2. 2.

    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.

  3. 3.

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

References

  1. 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)

    Google Scholar 

  2. 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)

    Chapter  Google Scholar 

  3. 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)

    Article  Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  8. 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)

    Chapter  Google Scholar 

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

    Google Scholar 

  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)

    Article  MATH  MathSciNet  Google Scholar 

  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)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  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)

    Article  MATH  Google Scholar 

  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  Google Scholar 

  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)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Computer Science, Freie Universität Berlin, Berlin, Germany

    Alexander Steen & Christoph Benzmüller

Authors
  1. Alexander Steen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Christoph Benzmüller
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Alexander Steen .

Editor information

Editors and Affiliations

  1. New York University, New York, New York, USA

    Martin Davis

  2. University of the South Pacific, Suva, Fiji

    Ansgar Fehnker

  3. Macquarie University, Sydney, New South Wales, Australia

    Annabelle McIver

  4. The University of Manchester, Manchester, United Kingdom

    Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Steen, A., Benzmüller, C. (2015). There Is No Best \(\beta \)-Normalization Strategy for Higher-Order Reasoners. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2015. Lecture Notes in Computer Science(), vol 9450. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-48899-7_23

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-48899-7_23

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-48898-0

  • Online ISBN: 978-3-662-48899-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation