Paper Info
Title
Efficiency and Completeness of the Set of Support Strategy in Theorem Proving
Abstract
One of the major problems in mechanical theorem proving is the generation of a plethora of redundant and irrelevant information. To use computers effectively for obtaining proofs, it is necessary to find strategies which will materially impede the generation of irre- levant inferences. One strategy wilich achieves this end is the set of support strategy. With any such strategy two questions of primary interest are that of its efficiency and that of its logical completeness. Evidence of the efficiency of this strategy is presented, and a theorem giving sufficient conditions for its logical completeness is proved. In a previous paper on theorem proving (1) a strategy based on the concept of set of support was briefly discussed. This concept, its logical significance, and the theorem establishing the logical completeness of the corresponding strategy are the focus of attention in the first part of the present, paper. The remainder of the paper is concerned witil the efficiency and sensitivity of the strategy. Evidence is supplied of its effect on time and memolT requirements and of its effect on the importance of the choice of parameter values. Evidence is also given of the value of the strategy in obtaining proofs of theorems whose mathe- matical depth is measurably greater than that of those previously provable by mechanical means. The evidence was obtained with the theorem-proving program PG1 implemented for the Control Data 3600. The language employed by PG1 is first-order predicate calculus, and the chief rule of inference employed therein is resolution (1, 2, 3).
Year
DOI
Venue
1965
10.1145/321296.321302
J. ACM
Keywords
DocType
Volume
Theorem Proving,Support Strategy
Journal
12
Issue
ISSN
Citations 
4
0004-5411
157
PageRank 
References 
Authors
154.12
1
3
Search Limit
100157
Name
Order
Citations
PageRank
Lawrence Wos1301212.69
George A. Robinson2251204.49
Daniel F. Carson3251204.49