Reference : Extensional Higher-Order Paramodulation in Leo-III
Scientific journals : Article
Engineering, computing & technology : Computer science
Extensional Higher-Order Paramodulation in Leo-III
Steen, Alexander mailto [University of Luxembourg > Faculty of Science, Technology and Medicine (FSTM) > Department of Computer Science (DCS) >]
Benzmüller, Christoph mailto [University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC) >]
Journal of Automated Reasoning
Kluwer Academic Publishers
[en] Automated Theorem Proving ; Higher-Order Logic ; Automated Reasoning
[en] Leo-III is an automated theorem prover for extensional type theory with Henkin semantics and choice. Reasoning with primitive equality is enabled by adapting paramodulation-based proof search to higher-order logic. The prover may cooperate with multiple external specialist reasoning systems such as first-order provers and SMT solvers. Leo-III is compatible with the TPTP/TSTP framework for input formats, reporting results and proofs, and standardized communication between reasoning systems, enabling e.g. proof reconstruction from within proof assistants such as Isabelle/HOL. Leo-III supports reasoning in polymorphic first-order and higher-order logic, in all normal quantified modal logics, as well as in different deontic logics. Its development had initiated the ongoing extension of the TPTP infrastructure to reasoning within non-classical logics.
Deutsche Forschungsgemeinschaft ; Volkswagenstiftung
Leo-III (BE 2501/11-1)
Preprint available at

File(s) associated to this reference

Fulltext file(s):

Open access
main.pdfAuthor preprint957.5 kBView/Open

Bookmark and Share SFX Query

All documents in ORBilu are protected by a user license.