The reasoning process developed by resolution-based systems inherently involves disjunctions in deriving definite consequences and always requires derived clauses to be reused as side clauses. Hence the number of derived clauses is usually large, and storing all of them appears unacceptably inefficient since both time and space requirements could become prohibitively large. In order to handle such complexity, in addition to the set of inference rules, a set of reduction rules and an adequate control strategy are supplied. The reduction rules aim to simplify the structure of the objects in the search space and to decrease the number of alternatives from which the next deduction step has to be selected, by removing literals and clauses.

This paper presents a series of considerations concerning different reduction rules, most of them already implemented in the Markgraf Karl system developed at the universities of Karlsruhe and Kaiserslautern. Some preliminary definitions, results, and previous work in this area are presented in the first three sections. The fourth section is entirely devoted to the problem of reduction rules and the control of their applicability when the underlying representation is a total clause graph. Rules for the detection and inhibition or removal of tautologies, subsumed clauses, and pure and merging literals are given, and the effects of their application are investigated. A possible control strategy and considerations concerning planning of applications are given in the fifth section. Based on the tests already performed on the Markgraf Karl system, the authors claim that appropriate reduction rules could greatly improve the system’s performance.

The detection of the applicability of different reduction rules and the corresponding system behavior need a well-founded theoretical investigation and therefore could be the topics of further research. Throughout the paper, concepts are clearly expressed, and the reader’s understanding is facilitated by numerous illustrative examples. The paper could be extremely useful to researchers working on resolution-based systems from both theoretical and practical approaches.