Accession Number:

AD0628319

Title:

THEOREM-PROVING BY COMPUTER.

Descriptive Note:

Final rept. for 1 Jan-31 Dec 65,

Corporate Author:

IIT RESEARCH INST CHICAGO ILL

Personal Author(s):

Report Date:

1966-01-05

Pagination or Media Count:

36.0

Abstract:

The subject of this study is the development of efficient theorem-proving algorithms, amenable to computer implementation, through the application of the theory of mathematical logic. The approach taken is via the Herbrand theorem and consists in expressing the denial of the theorem as a prefix formula of predicate calculus and generating an inconsistent set of instances of this formula. Several such refutation procedures are described and shown to be capable of deciding the satisfiability of various classes of formulas. Author

Subject Categories:

  • Theoretical Mathematics
  • Computer Hardware

Distribution Statement:

APPROVED FOR PUBLIC RELEASE