THEOREM PROVING WITH VARIABLE-CONSTRAINED RESOLUTION

被引：7

作者：

CHANG, CL

机构：

来源：

INFORMATION SCIENCES | 1972年 / 4卷 / 03期

关键词：

D O I：

10.1016/S0020-0255(72)80012-4

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

引用

收藏

页码：217 / &

相关论文

共 31 条

[1] ALLEN JR, 1970, MACH INTELL, V5, P321
[2] A LINEAR FORMAT FOR RESOLUTION WITH MERGING AND A NEW TECHNIQUE FOR ESTABLISHING COMPLETENESS
ANDERSON, R
BLEDSOE, WW
[J]. JOURNAL OF THE ACM, 1970, 17 (03) : 525 - &
[3] RESOLUTION WITH MERGING
ANDREWS, PB
[J]. JOURNAL OF THE ACM, 1968, 15 (03) : 367 - &
[4] UNIT PROOF AND INPUT PROOF IN THEOREM PROVING
CHANG, CL
[J]. JOURNAL OF THE ACM, 1970, 17 (04) : 698 - &
[5] CHANG CL, 1970, ARTIFICIAL INTELLIGE, V1
[6] CHANG CL, 1971, J ACM, V18
[7] A COMPUTING PROCEDURE FOR QUANTIFICATION THEORY
DAVIS, M
PUTNAM, H
[J]. JOURNAL OF THE ACM, 1960, 7 (03) : 201 - 215
[8] Davis M., 1963, P S APPL MATH, P15
[9] A PROOF METHOD FOR QUANTIFICATION THEORY - ITS JUSTIFICATION AND REALIZATION
GILMORE, PC
[J]. IBM JOURNAL OF RESEARCH AND DEVELOPMENT, 1960, 4 (01) : 28 - 35
[10] KOWALSKI R, 1969, MACHINE INTELLIGENCE, V0004, P00087

← 1 2 3 4 →