Abstract: This paper describes a theorem prover, running on a PDP-10-TENEX system, that can prove some theorems whose statements Involve a relatively large number of definitions. Such theorems require special methods because (1) their statements contain a large number of clauses and (2) their proofs are quite long although straight-forward.
A theorem is proven by first subdividing it into simple subgoals and then using a standard resolution theorem prover to prove the subgoals. The first part of this process Involves the substitution of definitions for defined quantities and the use of logical simplification. This process which is more similar to a natural deduction system than a resolution system, is shown to be complete when restricted to first-order logic. However, the theorem prover can deal with some interesting higher-order theorems as is shown by an example.
Publication Year: 1973
Publication Date: 1973-08-20
Language: en
Type: article
Access and Citation
Cited By Count: 4
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot