Automated hypothesis generation using extended inductive resolution
Charles O. Morgan · International Joint Conference on Artificial Intelligence · 1975
We report on a method of automated hypothesis generation, called f-resolution, which is derived from deductive resolution techniques. The method is inductive in character, in the sense that given input statement E, it generates hypotheses H, such that E is a deductive consequence of E. The method is extended by a generalized unification algorithm which introduces appropriate identity assumptions needed to unify a pair of literals. The f-resolution technique is shown to embody a version of Ockham's raror as a pruning heuristic. Some promising experimental results are also presented.