Skip to main content
SpringerLink
Log in

The Higher-Order Prover Leo-III (Extended Abstract)

  • Conference paper
  • First Online:
KI 2019: Advances in Artificial Intelligence (KI 2019)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 11793))

  • 1069 Accesses

Abstract

Leo-III is an automated theorem prover for extensional type theory with Henkin semantics. It also automates various non-classical logics, e.g., almost every normal higher-order modal logic is supported. In this extended abstract, the features of Leo-III are surveyed.

This is an abstract of the homonymous paper accepted at the 9th International Joint Conference on Automated Reasoning (IJCAR 2018), see doi: 10.1007/978-3-319-94205-6_8.

The work was 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 59.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 74.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.

    See the Leo-III project at GitHub: http://github.com/leoprover/Leo-III.

  2. 2.

    Cf. http://www.cs.miami.edu/~tptp/TPTP/Proposals/LogicSpecification.html.

  3. 3.

    Cf. [14, §2.2]; we refer to the literature [9] for more details on HOML.

References

  1. Andrews, P.B., Brown, C.E.: TPS: a hybrid automatic-interactive system for developing proofs. J. Appl. Log. 4(4), 367–395 (2006). https://doi.org/10.1016/j.jal.2005.10.002

    Article  MathSciNet  MATH  Google Scholar 

  2. Benzmüller, C., Andrews, P.: Church’s type theory. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, Stanford (2019). https://plato.stanford.edu/entries/type-theory-church/

    Google Scholar 

  3. Benzmüller, C., Kohlhase, M.: System description: LEO – a higher-order theorem prover. In: Kirchner, C., Kirchner, H. (eds.) CADE 1998. LNCS, vol. 1421, pp. 139–143. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0054256

    Chapter  Google Scholar 

  4. Benzmüller, C., Miller, D.: Automation of higher-order logic. In: Siekmann, J.H. (ed.) Computational Logic, Handbook of the History of Logic, vol. 9, pp. 215–254. Elsevier, Amsterdam (2014). https://doi.org/10.1016/B978-0-444-51624-4.50005-8

    Chapter  MATH  Google Scholar 

  5. Benzmüller, C., Otten, J., Raths, T.: Implementing and evaluating provers for first-order modal logics. In: Raedt, L.D., et al. (eds.) ECAI 2012. Frontiers in AI and Applications, vol. 242, pp. 163–168. IOS Press, Montpellier (2012). https://doi.org/10.3233/978-1-61499-098-7-163

    Chapter  Google Scholar 

  6. Benzmüller, C., Paulson, L.C.: Multimodal and intuitionistic logics in simple type theory. Log. J. IGPL 18(6), 881–892 (2010). https://doi.org/10.1093/jigpal/jzp080

    Article  MathSciNet  MATH  Google Scholar 

  7. Benzmüller, C., Sultana, N., Paulson, L.C., Theiss, F.: The higher-order prover LEO-II. J. Autom. Reason. 55(4), 389–404 (2015). https://doi.org/10.1007/s10817-015-9348-y

    Article  MathSciNet  MATH  Google Scholar 

  8. Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development - Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science an EATCS Series. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-662-07964-5

    Book  MATH  Google Scholar 

  9. Blackburn, P., van Benthem, J.F., Wolter, F.: Handbook of Modal Logic, vol. 3. Elsevier, Amsterdam (2006)

    MATH  Google Scholar 

  10. Blanchette, J.C., Paskevich, A.: TFF1: the TPTP typed first-order form with rank-1 polymorphism. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 414–420. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38574-2_29

    Chapter  Google Scholar 

  11. Blanchette, J.C., Nipkow, T.: Nitpick: a counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 131–146. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14052-5_11

    Chapter  Google Scholar 

  12. Brown, C., Gauthier, T., Kaliszyk, C., Sutcliffe, G., Urban, J.: GRUNGE: a grand unified ATP challenge. In: Fontaine, P. (ed.) Proceedings of the 27th International Conference on Automated Reasoning (2019, to appear). Preprint: arXiv:1903.02539 [cs.LO]

  13. Brown, C.E.: Satallax: an automatic higher-order prover. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 111–117. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31365-3_11

    Chapter  Google Scholar 

  14. Gleißner, T., Steen, A., Benzmüller, C.: Theorem provers for every normal modal logic. In: Eiter, T., Sands, D. (eds.) LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning. EPiC Series in Computing, Maun, Botswana, 7–12 May 2017, vol. 46, pp. 14–30. EasyChair (2017). https://doi.org/10.29007/jsb9

  15. Hustadt, U., Schmidt, R.A.: MSPASS: modal reasoning by translation and first-order resolution. In: Dyckhoff, R. (ed.) TABLEAUX 2000. LNCS (LNAI), vol. 1847, pp. 67–71. Springer, Heidelberg (2000). https://doi.org/10.1007/10722086_7

    Chapter  MATH  Google Scholar 

  16. Kaliszyk, C., Sutcliffe, G., Rabe, F.: TH1: the TPTP typed higher-order form with rank-1 polymorphism. In: Fontaine, P., Schulz, S., Urban, J. (eds.) Proceedings of the 5th Workshop on Practical Aspects of Automated Reasoning. CEUR Workshop Proceedings, vol. 1635, pp. 41–55 (2016). CEUR-WS.org

  17. Lindblad, F.: A focused sequent calculus for higher-order logic. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 61–75. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08587-6_5

    Chapter  Google Scholar 

  18. Steen, A.: Extensional paramodulation for higher-order logic and its effective implementation Leo-III, DISKI, vol. 345. Akademische Verlagsgesellschaft AKA GmbH, Berlin, September 2018. Dissertation, Freie Universität Berlin, Germany

    Google Scholar 

  19. Steen, A., Benzmüller, C.: The higher-order prover Leo-III. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS (LNAI), vol. 10900, pp. 108–116. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-94205-6_8

    Chapter  Google Scholar 

  20. Sutcliffe, G.: The TPTP problem library and associated infrastructure - from CNF to TH0, TPTP v6.4.0. J. Autom. Reason. 59(4), 483–502 (2017)

    Article  MathSciNet  Google Scholar 

  21. Sutcliffe, G., Benzmüller, C.: Automated reasoning in higher-order logic using the TPTP THF infrastructure. J. Formaliz. Reason. 3(1), 1–27 (2010). https://doi.org/10.6092/issn.1972-5787/1710

    Article  MathSciNet  MATH  Google Scholar 

  22. Tishkovsky, D., Schmidt, R.A., Khodadadi, M.: The tableau prover generator MetTeL2. In: del Cerro, L.F., Herzig, A., Mengin, J. (eds.) JELIA 2012. LNCS (LNAI), vol. 7519, pp. 492–495. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-33353-8_41

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. FSTC, University of Luxembourg, Esch-sur-Alzette, Luxembourg

    Alexander Steen

  2. Department of Maths and Computer Science, Freie Universität Berlin, Berlin, Germany

    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. Freie Universität Berlin, Berlin, Germany

    Christoph Benzmüller

  2. Universität Mannheim, Mannheim, Germany

    Heiner Stuckenschmidt

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Steen, A., Benzmüller, C. (2019). The Higher-Order Prover Leo-III (Extended Abstract). In: Benzmüller, C., Stuckenschmidt, H. (eds) KI 2019: Advances in Artificial Intelligence. KI 2019. Lecture Notes in Computer Science(), vol 11793. Springer, Cham. https://doi.org/10.1007/978-3-030-30179-8_30

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-30179-8_30

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-30178-1

  • Online ISBN: 978-3-030-30179-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation