Advertisement

Extensional Paramodulation for Higher-Order Logic and Its Effective Implementation Leo-III

  • Alexander SteenEmail author
Dissertation and Habilitation Abstracts

Abstract

Automation of classical higher-order logic faces various theoretical and practical challenges. On a theoretical level, powerful calculi for effective equality reasoning from first-order theorem proving cannot be lifted to the higher-order domain in a simple manner. Practically, implementations of higher-order reasoning systems have to incorporate procedures that often have high time complexity or are not decidable in general. In my dissertation, both the theoretical and the practical challenges of designing an effective higher-order reasoning system are studied. The resulting system, the automated theorem prover Leo-III, is one of the most effective and versatile systems, in terms of supported logical formalisms, to date.

Keywords

Higher-order logic Automated theorem proving Henkin semantics Quantified modal logics 

References

  1. 1.
    Andrews PB (1972) General models and extensionality. J Symb Log 37(2):395–397.  https://doi.org/10.2307/2272982 MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Andrews PB (1972) General models, descriptions, and choice in type theory. J Symb Log 37(2):385–394.  https://doi.org/10.2307/2272981 MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Bachmair L, Ganzinger H (1994) Rewrite-based equational theorem proving with selection and simplification. J Log Comput 4(3):217–247.  https://doi.org/10.1093/logcom/4.3.217 MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Benzmüller C (1999) Extensional higher-order paramodulation and RUE-resolution. In: CADE-16, LNCS, 1632:399–413. SpringerGoogle Scholar
  5. 5.
    Benzmüller C (2015) Higher-order automated theorem provers. In: Delahaye D, Woltzenlogel Paleo B (eds) All about proofs, proof for all, mathematical logic and foundations. College Publications, London, pp 171–214Google Scholar
  6. 6.
    Benzmüller C (2019) Universal (meta-)logical reasoning: recent successes. Sci Comput Progr 172:48–62.  https://doi.org/10.1016/j.scico.2018.10.008 CrossRefGoogle Scholar
  7. 7.
    Benzmüller C, Brown CE, Kohlhase M (2004) Higher-order semantics and extensionality. J Symb Log 69(4):1027–1088.  https://doi.org/10.2178/jsl/1102022211 MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Benzmüller C, Miller D (2014) Automation of higher-order logic. In: Siekmann JH (ed) Computational logic, handbook of the history of logic, vol 9. Elsevier, Amsterdam, pp 215–254.  https://doi.org/10.1016/B978-0-444-51624-4.50005-8 CrossRefzbMATHGoogle Scholar
  9. 9.
    Brown C, et al. (2019) GRUNGE: A Grand Unified ATP Challenge. In: P. Fontaine (ed.) Automated deduction – CADE-27, LNCS, vol. 11716, pp. 123–141. Springer.  https://doi.org/10.1007/978-3-030-29436-6_8
  10. 10.
    Church A (1940) A formulation of the simple theory of types. J Symb Log 5(2):56–68.  https://doi.org/10.2307/2266170 MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Frege G (1879) Begriffsschrift, eine der arithmetischen nachgebildete Formelsprache des reinen Denkens. Verlag von Louis Nebert, HalleGoogle Scholar
  12. 12.
    Gleißner T, Steen A, Benzmüller C (2017) Theorem provers for every normal modal logic. In: T. Eiter, D. Sands (eds.) LPAR-21, EPiC Series in Computing, vol. 46, pp. 14–30. EasyChair.  https://doi.org/10.29007/jsb9
  13. 13.
    Henkin L (1950) Completeness in the theory of types. J Symb Log 15(2):81–91.  https://doi.org/10.2307/2266967 MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    Muskens R (2007) Intensional models for the theory of types. J Symb Log 72(1):98–118.  https://doi.org/10.2178/jsl/1174668386 MathSciNetCrossRefzbMATHGoogle Scholar
  15. 15.
    Robinson G, Wos L (1969) Paramodulation and theorem-proving in first-order theories with equality. Mach Intell 4:135–150MathSciNetzbMATHGoogle Scholar
  16. 16.
    Steen A (2018) Extensional Paramodulation for Higher-Order Logic and its Effective Implementation Leo-III, DISKI - Dissertations in Artificial Intelligence, vol. 345. Akademische Verlagsgesellschaft AKA GmbH, Berlin, Dissertation. Freie Universität Berlin, GermanyGoogle Scholar
  17. 17.
    Steen A, Benzmüller C (2018) The higher-order prover Leo-III. In: D. Galmiche, et al. (eds.) IJCAR 2018, LNCS, vol. 10900, pp. 108–116. Springer.  https://doi.org/10.1007/978-3-319-94205-6_8
  18. 18.
    Steen A et al (2017) Going polymorphic—TH1 reasoning for Leo-III. In: Eiter T et al (eds) IWIL@LPAR 2017, Kalpa Publications in Computing, vol. 1. EasyChair.  https://doi.org/10.29007/jgkw
  19. 19.
    Sutcliffe G (2017) The TPTP problem library and associated infrastructure—from CNF to th0, TPTP v6.4.0. J Autom Reason 59(4):483–502MathSciNetCrossRefGoogle Scholar
  20. 20.
    Wisniewski M, Steen A, Benzmüller C (2016) TPTP and beyond: Representation of quantified non-classical logics. In: C. Benzmüller, J. Otten (eds.) ARQNL 2016, CEUR Workshop Proceedings, vol. 1770, pp. 51–65. CEUR-WS.orgGoogle Scholar
  21. 21.
    Wisniewski M, Steen A, Kern K, Benzmüller C (2016) Effective normalization techniques for HOL. In: Olivetti N, Tiwari A (eds) IJCAR 2016, LNCS, vol. 9706, pp. 362–370. Springer.  https://doi.org/10.1007/978-3-319-40229-1_25

Copyright information

© Gesellschaft für Informatik e.V. and Springer-Verlag GmbH Germany, part of Springer Nature 2019

Authors and Affiliations

  1. 1.Faculty of Science, Technology and CommunicationUniversity of LuxembourgEsch-sur-AlzetteLuxembourg

Personalised recommendations