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 条
  • [41] CSE_E 1.0: An Integrated Automated Theorem Prover for First-Order Logic
    Cao, Feng
    Xu, Yang
    Liu, Jun
    Chen, Shuwei
    Ning, Xinran
    SYMMETRY-BASEL, 2019, 11 (09):
  • [42] FIRST-ORDER SMOOTHING THEORY
    ROBERTS, PH
    SOWARD, AM
    JOURNAL OF MATHEMATICAL PHYSICS, 1975, 16 (03) : 609 - 615
  • [43] FIRST-ORDER PLANETARY THEORY
    HAMID, S
    ASTRONOMICAL JOURNAL, 1968, 73 (10P2): : S181 - &
  • [44] Type inference for first-order logic
    Schubert, A
    FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, 2000, 1784 : 297 - 313
  • [45] On the Proof-Theory of two Formalisations of Modal First-Order Logic
    Yehuda Schwartz
    George Tourlakis
    Studia Logica, 2010, 96 : 349 - 373
  • [46] On the Proof-Theory of two Formalisations of Modal First-Order Logic
    Schwartz, Yehuda
    Tourlakis, George
    STUDIA LOGICA, 2010, 96 (03) : 349 - 373
  • [47] DISCUSSIONS ABOUT THE REPORT “COMBINATORY LOGIC AS THE FIRST-ORDER MATHEMATICAL THEORY”
    柯通
    ChineseScienceBulletin, 1990, (23) : 2012 - 2013
  • [48] First-Order Logic Formalisation of Arrow's Theorem
    Grandi, Umberto
    Endriss, Ulle
    LOGIC, RATIONALITY, AND INTERACTION, PROCEEDINGS, 2009, 5834 : 133 - 146
  • [49] On first-order theorem proving using generalized odd-superpositions Ⅱ
    吴尽昭
    刘卓军
    Science in China(Series E:Technological Sciences), 1996, (06) : 608 - 619
  • [50] Well-Behaved Inference Rules for First-Order Theorem Proving
    Jinzhao Wu
    Zhuojun Liu
    Journal of Automated Reasoning, 1998, 21 : 381 - 400
12345