UNIFYING VIEW OF SOME LINEAR HERBRAND PROCEDURES

被引：15

作者：

LOVELAND, DW

机构：

来源：

关键词：

D O I：

10.1145/321694.321706

中图分类号：

TP3 [计算技术、计算机技术];

学科分类号：

0812 ;

摘要：

引用

页码：366 / &

共 21 条

ANDERSON, R ;

BLEDSOE, WW .

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

CHANG, CL .

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

DAVIS, M ;

PUTNAM, H .

[4]

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

[5]

HAYES P, 1969, MACHINE INTELLIGENCE, V4, P87

[6]

KOWALSKI R, 1970, 34 ED U MET UN MEM

LOVELAND, DW .

[8] MECHANICAL THEOREM-PROVING BY MODEL ELIMINATION [J].

LOVELAND, DW .

[9]

LOVELAND DW, 1971, COMPUTER SCIENCE RES, P7

[10]

LOVELAND DW, 1970, SOME LINEAR HERBRAND