Theorem-Proving by Computers
This citation is provided as a resource for researchers, but Contrails cannot provide a full-text download
U.S. government employees, Military/Department of Defense employees, and U.S. government contractors and sub-contractors may be eligible to register with the Defense Technical Information Center (DTIC), where this report and others like it may be available
Report Number: AFOSR-65-0338
Author(s): Kallick, B.
Corporate Author(s): IIT Research Inst.
Corporate Report Number: IITRI H6008-5
Date of Publication: 1965-01-31
Pages: 63
Contract: AF 49(638)1349
DoD Task:
Identifier: AD0611815
AD Number: AD 611815
Abstract:
The subject 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 theorem as the negation of a prefix formula of predicate calculus and of finding an inconsistent set of instances of this formula. The following problem is dealt with: in searching for an inconsistent set of instances and having already generated certain instances of a formula, how can the information in the matrix of the formula be utilized to determine the most appropriate way of generating the next instance. In this regard, the idea of expressing the matrix in disjunctive normal form and generating instances so as to construct inconsistent sub-paths is considered to be a useful technique and worthy of continued study. A partial solution to the following problem is also obtained: how can the information that a given disjunctive term of the matrix has figured in an inconsistent sub-path be utilized to avoid the repetition of identical computation the next time that term is encountered. A proof procedure is described which is capable of deciding certain known solvable subcases of the decision problem. It is conjectured that the procedure yield a new solvable subcase.
Author(s): Kallick, B.
Corporate Author(s): IIT Research Inst.
Corporate Report Number: IITRI H6008-5
Date of Publication: 1965-01-31
Pages: 63
Contract: AF 49(638)1349
DoD Task:
Identifier: AD0611815
AD Number: AD 611815
Abstract:
The subject 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 theorem as the negation of a prefix formula of predicate calculus and of finding an inconsistent set of instances of this formula. The following problem is dealt with: in searching for an inconsistent set of instances and having already generated certain instances of a formula, how can the information in the matrix of the formula be utilized to determine the most appropriate way of generating the next instance. In this regard, the idea of expressing the matrix in disjunctive normal form and generating instances so as to construct inconsistent sub-paths is considered to be a useful technique and worthy of continued study. A partial solution to the following problem is also obtained: how can the information that a given disjunctive term of the matrix has figured in an inconsistent sub-path be utilized to avoid the repetition of identical computation the next time that term is encountered. A proof procedure is described which is capable of deciding certain known solvable subcases of the decision problem. It is conjectured that the procedure yield a new solvable subcase.