The Higher-Order Prover Leo-III (Highlight paper)

Steen, Alexander; Benzmüller, Christoph

doi:10.3233/FAIA200462

Available on ORBilu since
01 March 2020

Paper published in a book (Scientific congresses, symposiums and conference proceedings)

The Higher-Order Prover Leo-III (Highlight paper)

Steen, Alexander; Benzmüller, Christoph

2020 • In Proceedings of the 24th European Conference on Artificial Intelligence

Peer reviewed

Permalink
https://hdl.handle.net/10993/42687

DOI
10.3233/FAIA200462

Files Send to Details Statistics Bibliography Similar publications

Files

Full Text

1068_paper.pdf

Author preprint (296.04 kB)

All documents in ORBilu are protected by a user license.

Send to

RIS BibTex APA Chicago Permalink Twitter Linkedin

Details

Keywords :

Leo-III; Higher-Order Logic; Automated Reasoning

Abstract :

[en] Leo-III is an effective automated theorem prover for extensional type theory with Henkin semantics. It is based on an extensional higher-order paramodulation calculus and supports reasoning in monomorphic and rank-1 polymorphic first-order and higher-order logics. Leo-III also automates various non-classical logics, including almost every normal higher-order modal logic.

Disciplines :

Computer science

Author, co-author :

Steen, Alexander ; University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)

Benzmüller, Christoph ; University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)

External co-authors :

yes

Language :

English

Title :

The Higher-Order Prover Leo-III (Highlight paper)

Publication date :

August 2020

Event name :

24th European Conference on Artificial Intelligence (ECAI 2020)

Event place :

Santiago de Compostela, Spain

Event date :

08-06-2020 to 12-06-2020

Audience :

International

Main work title :

Proceedings of the 24th European Conference on Artificial Intelligence

Publisher :

IOS Press

ISBN/EAN :

978-1-64368-100-9

Collection name :

Frontiers in Artificial Intelligence and Applications, Vol. 325

Pages :

2937-2938

Peer reviewed :

Peer reviewed

Additional URL :

http://ebooks.iospress.nl/volume/ecai-2020-24th-european-conference-on-artificial-intelligence

Commentary :

Postprint licensed under CC BY-NC 4.0 (https://creativecommons.org/licenses/by-nc/4.0/deed.en_US)

Statistics

Number of views

79 (2 by Unilu)

Number of downloads

3 (1 by Unilu)

More statistics

Scopus citations^®

Scopus citations^®
without self-citations

Bibliography

Christoph Benzmüller "Higher-order automated theorem provers "in All about Proofs, Proof for All, eds., David Delahaye and Bruno Woltzenlogel Paleo, Mathematical Logic and Foundations, 171-214, College Publications, London, UK, (2015).
Christoph Benzmüller and Peter Andrews "Church's type theory "in The Stanford Encyclopedia of Philosophy, ed., Edward N. Zalta, Metaphysics Research Lab, Stanford University, summer 2019 edn., (2019).
Christoph Benzmüller et al. "The higher-order prover LEO-II "J. Autom. Reasoning, 55 (4), 389-404, (2015).
Christoph Benzmüller and Bruno Woltzenlogel Paleo "Automating Gödel's ontological proof of God's existence with higher-order automated theorem provers "in ECAI, volume 263 of Frontiers in Artificial Intelligence and Applications, pp. 93-98. IOS Press, (2014).
Patrick Blackburn, Johan van Benthem, and Frank Wolter, Handbook of modal logic, volume 3, Elsevier, 2006.
Jasmin C. Blanchette and A. Paskevich "TFF1: The TPTP typed firstorder form with rank-1 polymorphism "in CADE, ed., M. P. Bonacina, volume 7898 of LNCS, pp. 414-420. Springer, (2013).
Chad E. Brown et al. "GRUNGE: A grand unified ATP challenge "in CADE, ed., P. Fontaine, volume 11716 of LNCS, pp. 123-141. Springer, (2019).
Tobias Gleißner, Alexander Steen, and Christoph Benzmüller "Theorem provers for every normal modal logic "in LPAR, eds., Thomas Eiter and David Sands, volume 46 of EPiC Series in Computing, pp. 14-30. EasyChair, (2017).
Cezary Kaliszyk, Geoff Sutcliffe, and Florian Rabe "TH1: The TPTP typed higher-order form with rank-1 polymorphism "in PAAR, eds., P. Fontaine, S. Schulz, and J. Urban, volume 1635 of CEUR Workshop Proceedings, pp. 41-55. CEUR-WS. Org, (2016).
Alexander Steen, Extensional Paramodulation for Higher-Order Logic and its Effective Implementation Leo-III, volume 345 of DISKI, Akademische Verlagsgesellschaft AKA GmbH, Berlin, 2018. Dissertation, Freie Universität Berlin, Germany.
Alexander Steen and Christoph Benzmüller "The higher-order prover Leo-III "in IJCAR, eds., Didier Galmiche, Stephan Schulz, and Roberto Sebastiani, volume 10900 of LNCS, pp. 108-116. Springer, (2018).
Geoff Sutcliffe "The TPTP problem library and associated infrastructure-from CNF to TH0, TPTP v6. 4. 0 "J. Autom. Reasoning, 59 (4), 483-502, (2017).
Geoff Sutcliffe and Christoph Benzmüller "Automated reasoning in higher-order logic using the TPTP THF infrastructure "J. Formalized Reasoning, 3 (1), 1-27, (2010).