How to Use Cycles for Logical Compilation

. Forward chaining is an algorithm that is particularly simple, and therefore used in many inference systems. It computes the facts that are the consequence of a set of facts and rules. Unfortunately, this algorithm is not complete with respect to negation. To solve this problem, it is possible, in the context of propositional calculus, to automatically add the rules needed to make computations with forward chaining complete. This transformation is a logical compilation of knowledge bases. This article presents a new method, based on a cycle search in a graph associated to the set of rules to compile, which identifies precisely the rules that must be added. 1 Introduction Among the various inference algorithms, forward chaining appears to be particularly simple and efficient. Based on modus ponens, it is commonly used in expert systems. Beyond its simplicity and its speed, it has the advantage to produce the set of facts that are consequence of knowledge, which isn't the case of theor..