This Article 
 Bibliographic References 
 Add to: 
A Problem-Oriented Search Procedure for Theorem Proving
August 1976 (vol. 25 no. 8)
pp. 807-815
D.H. Fishman, Bell Laboratories
In, this paper we argue that if search procedures are to use problem-specific information to direct a search, then they must have complete control over the deductive process. This includes the freedom to select any pair of clauses to interact as well as the freedom to select the literals upon which to attempt the interaction. We give examples to indicate the nature of inference rules which are incompatible with such search procedures. We then present a framework for a search procedure to indicate where problem-specific information may be utilized. Finally, we augment the search procedure to prevent the generation of certain redundant inferences. The augmentation makes use of lemmas to avoid replicating deduction sequences in solving multiple instances of the same subproblem at distinct places in the search space.
Index Terms:
Problem solving, resolution, search procedures.
D.H. Fishman, "A Problem-Oriented Search Procedure for Theorem Proving," IEEE Transactions on Computers, vol. 25, no. 8, pp. 807-815, Aug. 1976, doi:10.1109/TC.1976.1674699
Usage of this product signifies your acceptance of the Terms of Use.