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
相关论文
共 30 条
  • [11] DOWEK G, 1998, 3542 INRIA
  • [12] DOWEK G, 1995, LECT NOTES COMPUTER, V902, P154
  • [13] DOWEK G, 1998, 3400 INRIA
  • [14] EKMAN J, 1994, THESIS CHALMERS U TE
  • [15] FAY M, 1979, 4TH P WORKSH AUT DED, P161
  • [16] HALLNAS L, 1983, THESIS U STOCKHOLM
  • [17] HUET G, 1972, THESIS CASE W RESERV
  • [18] HUET G, 1976, THESIS U PARIS 7
  • [19] HUET G, 1973, INT J C ART INT, P139
  • [20] Huet G. P., 1975, Theoretical Computer Science, V1, P27, DOI 10.1016/0304-3975(75)90011-0
123