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 条

[1] Andrews P, 1986, An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof
[2] Andrews P. B., 1984, CONT MATH SERIES, V29, P169
[3] RESOLUTION IN TYPE THEORY
ANDREWS, PB
[J]. JOURNAL OF SYMBOLIC LOGIC, 1971, 36 (03) : 414 - &
[4] Bailin S. C., 1988, Journal of Automated Reasoning, V4, P269, DOI 10.1007/BF00244943
[5] RETRACTED: A NORMALIZATION THEOREM FOR SET-THEORY (Retracted article. See vol. 76, pg. 1096, 2011)
BAILIN, SC
[J]. JOURNAL OF SYMBOLIC LOGIC, 1988, 53 (03) : 673 - 695
[6] Church A., 1940, The Journal of Symbolic Logic, V5, P56, DOI [DOI 10.2307/2266170, 10.2307/2266170]
[7] DAVIS M, 1969, P INT FED INF PROC C, P67
[8] HIGHER-ORDER UNIFICATION VIA COMBINATORS
DOUGHERTY, DJ
[J]. THEORETICAL COMPUTER SCIENCE, 1993, 114 (02) : 273 - 298
[9] DOWEK G, 1998, 3556 INRIA
[10] DOWEK G, 1997, LECT NOTES COMPUTER, V1275, P105

← 1 2 3 →