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 条
  • [1] Abadi M(1991)Explicit substitutions J. Funct. Program. 1 375-416
  • [2] Cardelli L(1971)Resolution in type theory J. Symb. Log. 36 414-432
  • [3] Curien P(1972)General models and extensionality J. Symb. Log. 37 395-397
  • [4] Lévy J(1972)General models, descriptions, and choice in type theory J. Symb. Log. 37 385-394
  • [5] Andrews PB(2006)TPS: a hybrid automatic-interactive system for developing proofs J. Appl. Logic 4 367-395
  • [6] Andrews PB(1984)Automating higher-order logic Contemp. Math. 29 169-192
  • [7] Andrews PB(1994)Rewrite-based equational theorem proving with selection and simplification J. Log. Comput. 4 217-247
  • [8] Andrews PB(1946)A functional calculus of first order based on strict implication J. Symb. Log. 11 1-16
  • [9] Brown CE(2011)Combining and automating classical and non-classical logics in classical higher-order logics Ann. Math. Artif. Intell. 62 103-128
  • [10] Andrews PB(2017)Cut-elimination for quantified conditional logic J. Philos. Logic 46 333-353
12345678