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

  • Alexander SteenEmail author
Dissertation and Habilitation Abstracts


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.


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


  1. 1.
    Andrews PB (1972) General models and extensionality. J Symb Log 37(2):395–397. MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Andrews PB (1972) General models, descriptions, and choice in type theory. J Symb Log 37(2):385–394. 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. 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. CrossRefGoogle Scholar
  7. 7.
    Benzmüller C, Brown CE, Kohlhase M (2004) Higher-order semantics and extensionality. J Symb Log 69(4):1027–1088. 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. 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.
  10. 10.
    Church A (1940) A formulation of the simple theory of types. J Symb Log 5(2):56–68. 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.
  13. 13.
    Henkin L (1950) Completeness in the theory of types. J Symb Log 15(2):81–91. MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    Muskens R (2007) Intensional models for the theory of types. J Symb Log 72(1):98–118. 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.
  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.
  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.

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