Comparing Approaches To Resolution Based Higher-Order Theorem Proving

被引：0
|
作者：
Christoph Benzmüller
机构：
[1] Universität des Saarlandes,Fachbereich Informatik
来源：
Synthese | 2002年 / 133卷
关键词：
Theorem Prove; Full Extensionality; Extensionality Treatment; Additional Extensionality; Extensionality Axiom;
D O I：
暂无
中图分类号：
学科分类号：
摘要：
We investigate several approaches to resolution based automated theoremproving in classical higher-order logic (based on Church's simply typedλ-calculus) and discuss their requirements with respect to Henkincompleteness and full extensionality. In particular we focus on Andrews' higher-order resolution (Andrews 1971), Huet's constrained resolution (Huet1972), higher-order E-resolution, and extensional higher-order resolution(Benzmüller and Kohlhase 1997). With the help of examples we illustratethe parallels and differences of the extensionality treatment of these approachesand demonstrate that extensional higher-order resolution is the sole approach thatcan completely avoid additional extensionality axioms.
引用
收藏
页码：203 / 335
页数：132
相关论文
共 50 条
  • [1] Comparing approaches to resolution based higher-order theorem proving
    Benzmüller, C
    SYNTHESE, 2002, 133 (1-2) : 203 - 235
  • [2] Higher-order theorem proving and its applications
    Steen, Alexander
    IT-INFORMATION TECHNOLOGY, 2019, 61 (04): : 187 - 191
  • [3] Higher-order unification as a theorem proving procedure
    Hagiya, Masami
    Proceedings of the International Conference on Logic Programming, 1991,
  • [4] Graph Representations for Higher-Order Logic and Theorem Proving
    Paliwal, Aditya
    Loos, Sarah M.
    Rabe, Markus N.
    Bansal, Kshitij
    Szegedy, Christian
    THIRTY-FOURTH AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE, THE THIRTY-SECOND INNOVATIVE APPLICATIONS OF ARTIFICIAL INTELLIGENCE CONFERENCE AND THE TENTH AAAI SYMPOSIUM ON EDUCATIONAL ADVANCES IN ARTIFICIAL INTELLIGENCE, 2020, 34 : 2967 - 2974
  • [5] THEOREM-PROVING FOR A HIGHER-ORDER FUNCTIONAL LANGUAGE
    KAUFMANN, M
    JOURNAL OF SYMBOLIC LOGIC, 1986, 51 (03) : 847 - 847
  • [6] Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems
    Chad E. Brown
    Journal of Automated Reasoning, 2013, 51 : 57 - 77
  • [7] HOList: An Environment for Machine Learning of Higher-Order Theorem Proving
    Bansal, Kshitij
    Loos, Sarah
    Rabe, Markus
    Szegedy, Christian
    Wilcox, Stewart
    INTERNATIONAL CONFERENCE ON MACHINE LEARNING, VOL 97, 2019, 97
  • [8] Theorem Proving in Dependently-Typed Higher-Order Logic
    Rothgang, Colin
    Rabe, Florian
    Benzmueller, Christoph
    AUTOMATED DEDUCTION, CADE 29, 2023, 14132 : 438 - 455
  • [9] Progress in the Development of Automated Theorem Proving for Higher-Order Logic
    Sutcliffe, Geoff
    Benzmueller, Christoph
    Brown, Chad E.
    Theiss, Frank
    AUTOMATED DEDUCTION - CADE-22, 2009, 5663 : 116 - +
  • [10] Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems
    Brown, Chad E.
    AUTOMATED DEDUCTION - CADA-23, 2011, 6803 : 147 - 161
12345