Automated theorem proving in first-order logic module: On the difference between type theory and set theory

被引：0
|
作者：
Dowek, G [1 ]
机构：
[1] Inst Natl Rech Informat & Automat, F-78153 Le Chesnay, France
来源：
AUTOMATED DEDUCTION IN CLASSICAL AND NON-CLASSICAL LOGICS | 2000年 / 1761卷
关键词：
D O I：
暂无
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
Resolution modulo is a first-order theorem proving method that can be applied both to first-order presentations of simple type theory (also called higher-order logic) and to set theory. When it is applied to some first-order presentations of type theory, it simulates exactly higher-order resolution. In this note, we compare how it behaves on type theory and on set theory.
引用
收藏
页码：1 / 22
页数：22
相关论文
共 50 条
  • [1] APPROACH TO A SYSTEMATIC THEOREM PROVING PROCEDURE IN FIRST-ORDER LOGIC
    BIBEL, W
    COMPUTING, 1974, 12 (01) : 43 - 55
  • [2] Application of Multi-Clause Synergized Deduction in First-Order Logic Automated Theorem Proving
    Cao F.
    Xu Y.
    Chen S.
    Wu G.
    Chang W.
    Xinan Jiaotong Daxue Xuebao/Journal of Southwest Jiaotong University, 2020, 55 (02): : 401 - 408and427
  • [3] First-order theorem proving: Foreword
    Peltier, Nicolas
    Sofronie-Stokkermans, Viorica
    JOURNAL OF SYMBOLIC COMPUTATION, 2012, 47 (09) : 1009 - 1010
  • [4] A Deep Reinforcement Learning Approach to First-Order Logic Theorem Proving
    Crouse, Maxwell
    Abdelaziz, Ibrahim
    Makni, Bassem
    Whitehead, Spencer
    Cornelio, Cristina
    Kapanipathi, Pavan
    Srinivas, Kavitha
    Thost, Veronika
    Witbrock, Michael
    Fokoue, Achille
    THIRTY-FIFTH AAAI CONFERENCE ON ARTIFICIAL INTELLIGENCE, THIRTY-THIRD CONFERENCE ON INNOVATIVE APPLICATIONS OF ARTIFICIAL INTELLIGENCE AND THE ELEVENTH SYMPOSIUM ON EDUCATIONAL ADVANCES IN ARTIFICIAL INTELLIGENCE, 2021, 35 : 6279 - 6287
  • [5] Optimized encodings of fragments of type theory in first-order logic
    Tammet, T
    Smith, JM
    JOURNAL OF LOGIC AND COMPUTATION, 1998, 8 (06) : 713 - 744
  • [6] Material Dialogues for First-Order Logic in Constructive Type Theory
    Wehr, Dominik
    Kirst, Dominik
    LOGIC, LANGUAGE, INFORMATION, AND COMPUTATION, WOLLIC 2022, 2022, 13468 : 344 - 361
  • [7] On Turner's theorem and first-order theory
    Fine, Benjamin
    Gaglione, Anthony
    Lipschutz, Seymour
    Spellman, Dennis
    COMMUNICATIONS IN ALGEBRA, 2017, 45 (01) : 29 - 46
  • [8] First-Order Logic Theorem Proving and Model Building via Approximation and Instantiation
    Teucke, Andreas
    Weidenbach, Christoph
    FRONTIERS OF COMBINING SYSTEMS, FROCOS 2015, 2015, 9322 : 85 - 100
  • [9] VIRIAL THEOREM AND FIRST-ORDER PERTURBATION THEORY
    KILLINGBECK, J
    JOURNAL OF PHYSICS PART C SOLID STATE PHYSICS, 1970, 3 (01): : 23 - +
  • [10] Clausal connection-based theorem proving in intuitionistic first-order logic
    Otten, J
    AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS, 2005, 3702 : 245 - 261
12345