Extensional Higher-Order Paramodulation in Leo-III

Autor:	Steen, Alexander, Benzmüller, Christoph
Rok vydání:	2019
Předmět:	Computer Science - Artificial Intelligence Computer Science - Logic in Computer Science Computer Science - Symbolic Computation Mathematics - Logic 03B35 03B15 03B45 68T15 68T27 68T30 03Bxx I.2.3 F.4.1 I.2.4
Druh dokumentu:	Working Paper
DOI:	10.1007/s10817-021-09588-x
Popis:	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. Comment: 34 pages, 7 Figures, 1 Table; submitted article
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/1907.11501 Zobrazit plný text záznamu View this record from Arxiv