[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 :
Sciences informatiques
Auteur, co-auteur :
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)
Co-auteurs externes :
yes
Langue du document :
Anglais
Titre :
The Higher-Order Prover Leo-III (Highlight paper)
Date de publication/diffusion :
août 2020
Nom de la manifestation :
24th European Conference on Artificial Intelligence (ECAI 2020)
Lieu de la manifestation :
Santiago de Compostela, Espagne
Date de la manifestation :
08-06-2020 to 12-06-2020
Manifestation à portée :
International
Titre de l'ouvrage principal :
Proceedings of the 24th European Conference on Artificial Intelligence
Maison d'édition :
IOS Press
ISBN/EAN :
978-1-64368-100-9
Collection et n° de collection :
Frontiers in Artificial Intelligence and Applications, Vol. 325
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).
