登入選單
返回Google圖書搜尋
Controlling Recursive Inference
註釋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 the ancestors), provide a proof that it is correct, and discuss the conditions under which the strategy is optimal. We also derive more powerful pruning theorems for cases involving transitivity axioms and cases involving subsumed subgoals. The treatment of repeating inference is followed by consideration of the more difficult problem of recursive inference that does not repeat. Here we show how 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 answers.