An Approach for Finding C -Linear Complete Inference Systems
James Robert Slagle · Journal of the ACM · 1972
An inference system is C-linear complete if it is linear (ancestry filter) complete with top clause C, where C is in the original set of clauses and has suitable satisfiability properties.C-linear completeness is important for two reasons: (1) set-of-support refutation completeness is a corollary of C-linear refutation completeness, and previous computer experiments have indicated that the set-of-support strategy is efficient; (2) the search for a C-linear deduction can be naturally represented by a goal tree, and good techniques are known for searching such trees.A theorem is proved which provides a fairly general approach which, when given only a ground complete inference system, often yields a (nonground) C-linear complete system.This approach can be combined with a previously presented approach whose object is to replace some of the axioms of a given theory by a refutation complete system.The object of the combined approach is to replace some of the axioms by a C-linear refutation complete system.The approach of this paper is applied to six combinations of four inference rules.The rules are ordinary resolution, paramodulation, and two rules which respectively replace the transitivity axiom for C and the set membership axiom.C-linear refutation complete systems are found from the six combinations.For the case of resolution alone, the stronger C-linear deduction (consequence-finding) completeness is obtained.