Extensional Higher-Order Paramodulation in Leo-III

被引:0
作者
Alexander Steen
Christoph Benzmüller
机构
[1] University of Luxembourg,Department of Mathematics and Computer Science
[2] FSTM,undefined
[3] Freie Universität Berlin,undefined
来源
Journal of Automated Reasoning | 2021年 / 65卷
关键词
Higher-Order logic; Henkin semantics; Extensionality; Leo-III; Equational reasoning; Automated theorem proving; Non-classical logics; Quantified modal logics;
D O I
暂无
中图分类号
学科分类号
摘要
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 many quantified normal 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.
引用
收藏
页码:775 / 807
页数:32
相关论文
共 79 条
  • [11] Miller DA(2019)Universal (meta-)logical reasoning: recent successes Sci. Comput. Prog. 172 48-62
  • [12] Cohen EL(2004)Higher-order semantics and extensionality J. Symb. Log. 69 1027-1088
  • [13] Pfenning F(2010)Multimodal and intuitionistic logics in simple type theory Logic J. IGPL 18 881-892
  • [14] Bachmair L(2013)Quantified multimodal logics in simple type theory Logica Univ. 7 7-20
  • [15] Ganzinger H(2015)The higher-order prover LEO-II J. Autom. Reason. 55 389-404
  • [16] Barcan RC(2017)Computer-assisted analysis of the Anderson-Hájek ontological controversy Logica Univ. 11 139-151
  • [17] Benzmüller C(2017)Experiments in computational metaphysics: Gödel’s proof of God’s existence Savijnanam scientific exploration for a spiritual paradigm J. Bhaktivedanta Inst. 9 43-57
  • [18] Benzmüller C(2013)Extending Sledgehammer with SMT solvers J. Autom. Reason. 51 109-128
  • [19] Benzmüller C(1972)Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the church-rosser theorem INDAG. Math 34 381-392
  • [20] Benzmüller C(2003)A linear spine calculus J. Log. Comput. 13 639-688