Extensional Higher-Order Paramodulation in Leo-III

Steen, Alexander; Benzmüller, Christoph

doi:10.1007/s10817-021-09588-x

Reference : Extensional Higher-Order Paramodulation in Leo-III


	Document type :	Scientific journals : Article
	Discipline(s) :	Engineering, computing & technology : Computer science
	To cite this reference:	http://hdl.handle.net/10993/46727

Title :	Extensional Higher-Order Paramodulation in Leo-III
Language :	English
Author, co-author :	Steen, Alexander [University of Luxembourg > Faculty of Science, Technology and Medicine (FSTM) > Department of Computer Science (DCS) >]
	Benzmüller, Christoph [University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC) >]
Publication date :	27-Mar-2021
Journal title :	Journal of Automated Reasoning
Publisher :	Kluwer Academic Publishers
Volume :	65
Pages :	775-807
Peer reviewed :	Yes (verified by ORBi^lu)
Audience :	International
ISSN :	0168-7433
e-ISSN :	1573-0670
Country :	Netherlands
Keywords :	[en] Automated Theorem Proving ; Higher-Order Logic ; Automated Reasoning
Abstract :	[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.
Funders :	Deutsche Forschungsgemeinschaft ; Volkswagenstiftung
Name of the research project :	Leo-III (BE 2501/11-1)
Target :	Researchers
Permalink :	http://hdl.handle.net/10993/46727
DOI :	10.1007/s10817-021-09588-x
Other URL :	https://rdcu.be/chCsq
Commentary :	Preprint available at https://arxiv.org/abs/1907.11501

File(s) associated to this reference

Fulltext file(s):

	File	Commentary	Version	Size	Access
Open access	main.pdf		Author preprint	957.5 kB	View/Open

All documents in ORBi^lu are protected by a user license.

University of Luxembourg Library | Feedback | Legal notices