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 条
  • [31] A First Class Boolean Sort in First-Order Theorem Proving and TPTP
    Kotelnikov, Evgenii
    Kovacs, Laura
    Voronkov, Andrei
    INTELLIGENT COMPUTER MATHEMATICS, CICM 2015, 2015, 9150 : 71 - 86
  • [32] SEPARATION PRINCIPLES IN HIERARCHY THEORY OF PURE FIRST-ORDER LOGIC
    CLARKE, DA
    JOURNAL OF SYMBOLIC LOGIC, 1966, 31 (03) : 503 - &
  • [33] UNIFORM COMPACTNESS THEOREM IN FIRST-ORDER LOGIC
    WEAVER, GE
    NOTICES OF THE AMERICAN MATHEMATICAL SOCIETY, 1973, 20 (06): : A588 - A588
  • [34] A Lindstrom theorem for intuitionistic first-order logic
    Olkhovikov, Grigory
    Badia, Guillermo
    Zoghifard, Reihane
    ANNALS OF PURE AND APPLIED LOGIC, 2023, 174 (10)
  • [35] Heterogeneous Heuristic Optimisation and Scheduling for First-Order Theorem Proving
    Holden, Edvard K.
    Korovin, Konstantin
    INTELLIGENT COMPUTER MATHEMATICS (CICM 2021), 2021, 12833 : 107 - 123
  • [36] AUTOMATED THEOREM-PROVING APPLIED TO THE THEORY OF SEMIGROUPS
    MCFADDEN, RB
    LECTURE NOTES IN MATHEMATICS, 1988, 1320 : 235 - 243
  • [37] THEORY LINKS - APPLICATIONS TO AUTOMATED THEOREM-PROVING
    MURRAY, NV
    ROSENTHAL, E
    JOURNAL OF SYMBOLIC COMPUTATION, 1987, 4 (02) : 173 - 190
  • [38] Proving isomorphism of first-order logic proof systems in HOL
    Mikhajlova, A
    von Wright, J
    THEOREM PROVING IN HIGHER ORDER LOGICS, 1998, 1479 : 295 - 314
  • [39] Automated theorem proving for many-sorted free description theory based on logic translation
    Nakamatsu, K
    Suzuki, A
    ADVANCES IN LOGIC, ARTIFICIAL INTELLIGENCE AND ROBOTICS, 2002, 85 : 17 - 28
  • [40] 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 - +
12345