THEOREM PROVING WITH VARIABLE-CONSTRAINED RESOLUTION

被引：7

作者：

CHANG, CL

机构：

来源：

关键词：

D O I：

10.1016/S0020-0255(72)80012-4

中图分类号：

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

学科分类号：

0812 ;

摘要：

引用

页码：217 / &

共 31 条

[1]

ALLEN JR, 1970, MACH INTELL, V5, P321

ANDERSON, R ;

BLEDSOE, WW .

[3] RESOLUTION WITH MERGING [J].

ANDREWS, PB .

[4] UNIT PROOF AND INPUT PROOF IN THEOREM PROVING [J].

CHANG, CL .

[5]

CHANG CL, 1970, ARTIFICIAL INTELLIGE, V1

[6]

CHANG CL, 1971, J ACM, V18

[7] A COMPUTING PROCEDURE FOR QUANTIFICATION THEORY [J].

DAVIS, M ;

PUTNAM, H .

[8]

Davis M., 1963, P S APPL MATH, P15

GILMORE, PC .

[10]

KOWALSKI R, 1969, MACHINE INTELLIGENCE, V0004, P00087