Report 84 06 Controlling Recursive Inference . S Stanford David E. Smith Michael R. Matthew L. Ginsberg a

Loosely speaking, recursive inference is when an inference procedure generates an infinite sequence of similar subgoals. In general, the control of recursive inference involves demonstrating that recursive portions of a search space will not contribute any new answers to the problem beyond a certain level. We first review a well known syntactic method for controlling repeating inference (inference where the conjuncts processed are instances of their ruicestors), provide a proof that it is correct, and discuss the con- (Mims under which the strategy is optimal. We also derive more powerful pruning theorems for rases involving transitivity axioms arid cases involving subsumed subgoals. The treatment of repeating inference is followed by consideration of the More difficult prr)liIon of recursive inference Crat does not repeat. Here we show bow knowledge of the properties of the relations involved and knowledge about the contents of the system's database can be used to prove that portions of a search space will not contribute any new .az