THEOREM-PROVING BY COMPUTER.
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)
Document Details
- Document Type
- Technical Report
- Publication Date
- Jan 05, 1966
- Accession Number
- AD0628319
Entities
People
- B. Kallick
Organizations
- IIT Research Institute