THEOREM-PROVING ON COMPUTER

被引：34

作者：

ROBINSON, JA

机构：

来源：

JOURNAL OF THE ACM | 1963年 / 10卷 / 02期

关键词：

D O I：

10.1145/321160.321166

中图分类号：

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

学科分类号：

0812 ;

摘要：

引用

页码：163 / &

共 17 条

[1]

Beth E. W., 1962, FORMAL METHODS

[2]

BIRKHOFF G, 1948, AMER MATH SOC COLL P, V25

[3]

BIRKHOFF G., 1953, SURVEY MODERN ALGEBR

[4] ON THE FALSITY OF EULERS CONJECTURE ABOUT THE NON-EXISTENCE OF 2 ORTHOGONAL LATIN SQUARES OF ORDER 4T+2STAR [J].

BOSE, RC ;

SHRIKHANDE, SS .

PROCEEDINGS OF THE NATIONAL ACADEMY OF SCIENCES OF THE UNITED STATES OF AMERICA, 1959, 45 (05) :734-737

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

DAVIS, M ;

PUTNAM, H .

JOURNAL OF THE ACM, 1960, 7 (03) :201-215

[6] A MACHINE PROGRAM FOR THEOREM-PROVING [J].

DAVIS, M ;

LOGEMANN, G ;

LOVELAND, D .

COMMUNICATIONS OF THE ACM, 1962, 5 (07) :394-397

[7]

DAVIS M, 1962, AMS589 M

[8] A PROOF METHOD FOR QUANTIFICATION THEORY - ITS JUSTIFICATION AND REALIZATION [J].

GILMORE, PC .

IBM JOURNAL OF RESEARCH AND DEVELOPMENT, 1960, 4 (01) :28-35

[9] ORTHOGONAL LATIN SQUARES [J].

PARKER, ET .

PROCEEDINGS OF THE NATIONAL ACADEMY OF SCIENCES OF THE UNITED STATES OF AMERICA, 1959, 45 (06) :859-862

[10] A MECHANICAL PROOF PROCEDURE AND ITS REALIZATION IN AN ELECTRONIC COMPUTER [J].

PRAWITZ, D ;

PRAWITZ, H ;

VOGHERA, N .

JOURNAL OF THE ACM, 1960, 7 (02) :102-128

← 1 2 →