HUMAN ORIENTED LOGIC FOR AUTOMATIC THEOREM-PROVING

被引：17

作者：

NEVINS, AJ ^{[1
]}

机构：

[1] GEORGE WASHINGTON UNIV,WASHINGTON,DC

来源：

JOURNAL OF THE ACM | 1974年 / 21卷 / 04期

关键词：

D O I：

10.1145/321850.321858

中图分类号：

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

学科分类号：

0812 ;

摘要：

引用

页码：606 / 621

页数：16

共 19 条

[1]

ALLEN J, 1970, MACHINE INTELLIGENCE, P321

[2] SPLITTING AND REDUCTION HEURISTICS IN AUTOMATIC THEOREM PROVING [J].

BLEDSOE, WW .

ARTIFICIAL INTELLIGENCE, 1971, 2 (01) :55-77

[3] COMPUTER PROOFS OF LIMIT THEOREMS [J].

BLEDSOE, WW ;

BOYER, RS ;

HENNEMAN, WH ;

BOYER, RS ;

HENNEMAN, WH .

ARTIFICIAL INTELLIGENCE, 1972, 3 (02) :27-60

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

CHANG, CL .

JOURNAL OF THE ACM, 1970, 17 (04) :698-&

[5] THEOREM PROVING WITH VARIABLE-CONSTRAINED RESOLUTION [J].

CHANG, CL .

INFORMATION SCIENCES, 1972, 4 (03) :217-&

[6]

CHINTHAYAMMA, 1969, NOTICES AM MATH SOC, V16, pT69

[7] UTILITY OF INDEPENDENT SUBGOALS IN THEOREM PROVING [J].

ERNST, GW .

INFORMATION AND CONTROL, 1971, 18 (03) :237-&

[8]

KLEENE SC, 1952, INTRO METAMATHEMATIC

[9] LINEAR RESOLUTION WITH SELECTION FUNCTION [J].

KOWALSKI, R ;

KUEHNER, D .

ARTIFICIAL INTELLIGENCE, 1971, 2 (3-4) :227-260

[10] UNIFYING VIEW OF SOME LINEAR HERBRAND PROCEDURES [J].

LOVELAND, DW .

JOURNAL OF THE ACM, 1972, 19 (02) :366-&

← 1 2 →