Efficiency and Completeness of the Set of Support Strategy in Theorem Proving

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 irrelevant 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.