A Note on Backward Dual Resolution and Its Application to Proving Completeness of Rule-Based Systems

1 Introduction

Resolution theorem proving has gained a great popular­ ity after it was first described by Robinson (1965]. The method combines in a single rule the power of other rules, and , due to its uniformity, can be easily implemented for automated theorem proving with computers.

In this paper, an idea of a theorem proving method dual to classical resolution is investigated in brief. The method can be related to the inverse method of Maslov [Maslov, 1964] (see also [Maslov, 1968] for the most com­ plete presentation) , and according to [Kuehner, 1971] it can be derived from the inverse method; in fact, it falls into the class of localized inverse methods [Kuehner, 1971 ; Maslov, 1971]. However, it seems most straightfor­ ward to introduce the investigated method as one dual to classical resolution.

The presented method is called backward dual resolu­ tion or bd-resolution, for short . The proposed method is analogous to resolution method. Instead of checking unsatisfiability of a set of clauses we rather try to prove validity of a given formula in disjunctive normal form. Thus, the initial form is in fact dual to the one in reso­ lution method. Further, the proposed method works in fact backwards. This means that during the process of derivation one generates new formulae from parent for­ mulae starting from the initial formula to be proved - but with regard to logical inference, the alternative of parent formulae is a logical consequence of the derived formula! Thus, at any step of reasoning the derivation process is reversed with regard to finding logical consequences. The process of derivation is successful if it eventually ends up with an empty tautology formula which (here) is always true- in this case, the initial formula, as a logical consequence of it, is proved. Since the method is dual to resolution, all but necessary technical details and proofs are omitted here; one can find them in [Lig~za, 1992b).l The motivation for bd-resolution follows from logical investigation of rule-based control systems. Throughout this paper, by a rule-based control system (knowledge­ based control system) we shall understand a system de­ signed to control some object and consisting of a set of rules defining the possible control actions. A rule-based control system is assumed to operate according to the following scheme: the current state of the controlled sys­ tem is observed, then a rule with satisfied preconditions is selected, and the specified by this rule control action is executed; the basic cycle is repeated in an "endless loop" until it is stopped (either by some of the rules or as a result of some external interrupt) . Such systems were discussed in [Tzafestas and Lig~za, 1989] and more thoroughly in [Lig~za, 1992b].

·This research was supported by State Committee on Sci­ entific Research within the Project Computer Systems of Control and Decision Making - Elements of Theory, For­ mal Tools and Computer Aided Design, Grant No. 8-85289102; a first version of this paper appeared as a Techni­ cal Report of Laboratoire d'Automatique et d'Analyse des Systemes (LAAS du CNRS) No. 92214, Toulouse, France, 1992.

BD-resolution was initially introduced as a basic rea­ soning paradigm for knowledge-based control systems (Lig~za, 1992a; Lig~za, 1992b]. There are at least three standard issues concerning logical investigation of such systems; these are: (I) checking if logical description of the current situation satisfies the formula defining pre­ conditions of a rule (i.e. checking if a rule can be fired) , (II) checking if some two formulae defining preconditions of two rules may be simultaneously satisfied (i.e. checking if some two rules can succeed for the same state - in such a case the system is indeterministic and there is a need for conflict resolution), and {III) checking if the alternative of precondition formulae of all the rules constitutes a tautology {i.e. checking if the control sys­ tem can react in any state an so it is complete) . The above tasks can be approached with use of different in­ ference mechanisms (including the classical resolution), but it seems that bd-resolution fits best the purpose. The advantage of bd-resolution consist in the possibil­ ity of direct reasoning with formulae describing situa­ tions and preconditions in a most natural way. Further, in case of incomplete systems formulae defining specific completeness are directly generated. Here we investi­ gate only the possible application of bd-resolution con­ cerning completeness verification of rule-based systems (problem (III)). The other problems and related issues are presented in some details in [Ligt:za, 1992b] .

1 A copy of this report should be available from Documen­ tation Service, L.A.A.S. du C.N.R.S. , 7, Av. du Colonel­ Roche, 31-077 Toulouse Cedex, France.

The problem of logical checking of completeness, con­ sistency, and related issues seems to be of both theoreti­ cal interest and practical importance, but simultaneously largely ignored in the literature. A comprehensive recent review providing a recapitulation of the problems and summarizing current results is given in [Andert, 1992]; almost complete list of problem literature can be found there as well .

With regard to completeness of rule-based systems two basic approaches can be noticed. The most pop­ ular one consists in, roughly speaking, an exhaustive enumeration of possible input data and systematic in­ spection of a given set of rules versus a table con­ taining all possible parameters and conditions combi­ nations. This kind of approach can be called an ex­ haustive completeness check [Andert, 1992]. Some exam­ ples of this approach are presented in [Suwa et al, 1984; Cragun and Steudel, 1987]. A basic approach ([Suwa et al, 1984]) consists in finding all parameters used in con­ ditions of rules, generating a table displaying all possible combinations of parameter values, and checking the set of rules against the table so as to verify completeness and detect missing rules. This kind of approach can be also referred to as static verification of the set of rules.

The other approach consists in a run-time validation and verification of the expert system with use of selected set of test cases [Tepandi, 1990]. The selected example problems should also provide an exhaustive list of pos­ sible cases. Some other approaches of this kind are also discussed in [Andert , 1992]. Methods of this sort can be referred to as dynamic verification of rule-based system.

In this paper another logic-based approach is pro­ posed. The approach neither requires the generation and use of tables containing possible condition/parameter combinations, nor it is based on exhaustive test of pos­ sible cases. Note that, in case of use of full first-order logic for building preconditions of the system rules an exhaustive check would seldom be feasible, since even for a language containing only one function symbol the Herbrand universe ([Chang and Lee, 1973]) is- infinite.

The proposed approach can be applied directly to sys­ tems in which niles are constructed with use of predicate logic notation such that conjunction is the basic connector between facts {conditions); more complex formulae are built with use alternative. The negation is to be ex­ pressed explicitly, i.e. facts of the form p and ·p should be used. The method can be used for rules constituting a "single-layer" of reasoning, i.e. during reasoning one of the rules from a considered set is to be selected and fired; thus, the proposed approach is especially convenient for knowledge-based control systems [Ligt:za, 1992b; Tzafestas and Lig~za, 1989].

2 BD-Resolution

Let us briefly recapitulate the main idea of resolution theorem proving {the resolution method is presented in e.g. [Chang and Lee, 1973; Genesereth and Nilsson, 1987]) . Throughout the paper we shall made use of some commonly used logical symbols, including I= (I= 1 ) for denoting logical satisfaction (satisfaction under interpre­ tation I) and 1- for provability ([Genesereth and Nilsson, 1987]). An empty tautology formula (always true!) will be denoted with T.

Without going into details, resolution theorem proving proceeds as follows. Let ~ denote a set of given axioms (from logical point of view, a conjunction), and let 4> be a formula to be proved. Thus, one is to prove that

is a valid formula. In classical resolution method, in­ stead of proving (1), one takes the negation of it , i.e.

and tries to show that (2) is unsatisfiable. In practice (2) is transformed into so-called clausal form, i.e. to a set (conjunction) of clauses (disjunctions of literals). Now, in order to show that a set of clauses is unsatisfiable, one attempts to derive from it an empty clause (here: always unsatisfiable). The derivation is carried out with use of resolution rule, which preserves logical consequence. Thus, any newly derived clause is a logical consequence of its parent clauses. If an empty clause is eventually derived, the unsatisfiability of the initial set of clauses is proved.

A great advantage of the classical resolution method consists in leaving the set of axioms~ almost unchanged. In most of practical cases there is a set (conjunction) of separate axioms, and each of them can be converted into clausal form independently from the others. This ap­ proach saves computational effort and fits most of classi­ cal problems in a naturally efficient way. However, from theoretical point of view, one can also try to prove va­ lidity of (1) directly. Below, we present the basic idea in some details.

First, instead of converting a formula to its clausal form one can transform the initial formula to a dual form, consisting of an alternative of conjunctions of literals. Now we shall need the two following definitions.

Definition 1 Let q1, q2 , .· . , qk be literals. A formula ¢J· = q11\ q2 I\ .. . I\ qk is called a simple formula. Further, let ¢Jb ifJ2, .. . , l/Jn be some simple formulae . Any formula 4> = ifJ1 V ifJ2 V ... V l/Jn will be called a normal formula.

Thus, a simple formula is a finite conjunction of lit­ erals- simple formulae will be frequently denoted with the l~tters ¢; and 1/J. A normal formula is also called in literature a formula in disjunctive normal form {DNF); normal formulae will be most frequently denoted with the letters ~ and 'if.

For further considerations we assume that the formula to be proved is a normal formula. Note that all the vari­ ables in the formula are (implicitly) existentially quan­ tified (dually to classical resolution method). Thus, the formula can be written as

Let ,P 1 and ,P 2 be two simple formulae of 'If . Bd­ resolution is defined as follows .

Definition 2 (Backward dual resolvent) Let 1/J 1 = ,p<l> /1. ql and ,p2 = ,p<2> /1. -,q2 and let there exist a most general unifier {mgu) u for q 1 and q2. Then, a formula 1/J

will be called a backward dual resolvent (bd-resolvent) of ,P 1 and ,P2.

Now, we shall prove that in fact for any bd-resolvent ( 4) , the alternative of the parent formulae ,P 1 and ,P 2 is its logical consequence.

Theorem 1 (Soundness of bd-resolution) Let 1/J be the bd-resolvent defined as above {4). Then 1/J 1 V 1/J 2 is the logical consequence of 1/J .

Proof Let us assume that 1/J is satisfied under some in­ terpretation I , i.e. FI 1/J. Thus both FI ,p<l> u and f= 1 ,p< 2 > u . Obviously, for any pair of complementary literals q 1 u and -,q2u, there is either FI ,p<l>u /1. q 1 u or f=1 ,p< 2 >u /1. -,q2u . Thus the alternative of the two above is satisfied. Since changing the terms substituted by u into existentially quantified variables does not vio­ late satisfiability (existential quantifier introduction), the alternative ,P 1 V ,P 2 is satisfied under I, Q.E.D.

In order to pass to theorem proving with bd-resolution let us define an idea of derivation with use of bd­ resolution. Below, by a factor of a formula we shall un­ derstand the result of applying some substitution to the formula in order to replace certain variables with terms. Any formula is logical consequence of any of its factors.

Definition 3 (BD-derivation) A bd-derivation {or derivation, for short) of a simple formula 1/J from a nor­ mal formula 'If given by {3) is any sequence of simple formula e ,P 1 , ,P2, ... , ,pk , satisfying the following condi­ tions:

• for any i E {1 , 2, ... , k} , 1/J' is a bd-resolvent or a factor of simple formulae either belonging to 'if or generated earlier bd-resolvents,
• 1/J = ,pk,

Formula t/J is said to be derived from 'if.

For convenience, if k = 1 ( 1/J E 'If) we shall also say that t/J is derived from 'if.

Now, we can state the following theorem.

Theorem 2 (Soundness of bd-derivation) Let 'if be a normal formula defined by {9) . If an empty tautology formula (always true, denoted with T) can be derived from 'if, then 'If is valid {is a tautology) .

Proof For any simple formula 1/J derived from 'if there is 1/J f= 'If. If the empty tautology formula is derived from 'if, then we have T f= 'If . Thus 'if is valid, Q.E.D.

We are not investigating here the problem of com­ pleteness of bd-resolution; however, one can expect that due to duality to resolution method the bd-resolution method is potentially comf.lete, as well . The proof can be found in [LigE:za, 1992b .

3 Completeness and generalized resolution

For intuition, a knowledge-based system of rules is com­ plete if it "covers" all the possible cases to which the rules are aimed to be applied. Obviously, a set of rules should be complete in order to assure the possibility of dealing with any occurring case. We shall refer to any such case as a state. A set of states will be referred to as situation. 2 To any state there is assigned a unique formula describing this state, to be called state formula . Any situation can have more than one describing for­ mula, to be called situation formulae . Of course, if a state s having state formula ¢; belongs to a situation S having situation formula~, there is¢; f= ~ -

A definition of completeness requires some more pre­ cise statement with regard to logical notions introduced. Generally speaking, from logical point of view, a com­ plete system of rules is one having the potential power of dealing with any occurring state formula. This, in fact, means that the alternative of the rule precondition formulae should constitute an empty tautology formula (always true) . In such a case, for any potentially possible formula describing some state s described with state for­ mula¢;, some of the precondition formulae must "cover" ¢;; logically, the condition can be written as ¢; F= 'if; , where 'If; is a normal formula defining preconditions of some i-th rule. Note however, that the strictly logical completeness will in most cases be too strong for prac­ tical applications. This is so, because most of the sys­ tems are incomplete with regard to possible state rep­ resentation [LigE:za, 1992b], and thus, there is no need to "cover" all the "potential" states but only the really existing ones.

With regard to the above considerations the following definition of completeness is stated.

Definition 4 (Completeness) Let us consider a knowledge-based system consisting of a set T of k produc­ tion rules, each of them having its precondition formula 'if; , i= 1,2, . .. ,k. The system is:

• logically complete, if and only if the alternative of the preconditions formulae satisfies the following condition:

2 Formal definitions and a detailed presentation of prob­ lem concerning states and situations can be found in [LigE:za, 1992b].

{in other words, 1li1 V 1li2 V . .. VIIi~: is a tautology),

• physically complete, if and only if for any existing state s descnbed wzth formula <P there exists at least one rule in T applicable to s, i.e. there is

Definition 5 (Specific completeness) Consider a knowledge-based system as above. The system is:

• specifically logically complete with regard to formula III, if and only if the following condition holds

• specifically physically complete with regard to situa­ tion S described with formula 1li, if and only if for any state s described with formula <P and such that s E S (<P f= 1li) there exists at least one rule in T applicable to s, i.e. the following condition holds for some z

With regard to the above definitions, a set of rules can be complete in a strictly logical sense (logical complete­ ness) or complete in reference to the particular universe of discourse. Of course, the logical completeness consti­ tutes a stronger requirement ; it always implies physical completeness, while the reverse statement is not true.

Both logical and physical completeness can refer to a general case (the former definition) or to a specific case (the latter one) . The latter definition provides in fact a weak requirement for completeness. Intuitively speaking, specific completeness means that the scope of possible situations in which the systems is intended to operate is a priori restricted to the one described with formula 1li. Of course logical (physical) completeness always implies specific logical (physical) completeness. Moreover , spe­ cific logical completeness with regard to formula 1li im­ plies the appropriate specific physical completeness with regard to the situation described with 1li .

The above definitions of completeness (either logical or physical) are, to certain degree similar; they become the same for S being the situation of all the existing states (for example, for the appropriate situation formula being ¢1 V ¢2 V ... V <Pn, where ¢1, ¢2, ... , <Pn are the state formulae of all the states, or respectively 1li being the empty tautology formula (always true) .

The aim of building complete systems is that it should be possible for the control system to react in and further transform any physical state. This means that the set of rules (the preconditions of them) should cover the whole state-space of the system. Since in practical applications not all the possible to describe states are feasible, it is useful to define a weak completeness, i.e. completeness with regard to some specified formula 1li (situation S) . Of course, situation S should contain all the physically possible states, i.e. 1li should be chosen in such a way that ¢1 V ¢2 V . .. V <Pn f= 1li. Simultaneously, the "more detailed" 1li is, the easier the design of a complete system should be. If all the state formulae are given explicitly, it would be enough to take them as preconditions of the transformation rules directly (at least potentially; in re­ alistic case the formulae, would be probably very long and there would be quite a large number of them) .

Note that the presented above definition of logical completeness does not refer to any specific interpreta­ tion. Thus one may regard it as too abstract; in fact , it will be usually too strong - and therefore rarely (or never) satisfied - for realistic systems. In the context of practical applications the definition of physical com­ pleteness is much more in place. However, this definition refers implicitly to the intended interpretation, the one under which the formulae describing states refer to the universe of interest (can be read) in a reasonable way.

Let us notice that in the case of verifying physi­ cal completeness purely logical methods are likely to be insufficient. These methods are based on syntactic structure of formulae and do not refer to interpreta­ tion. Thus, a formula like switch(on)Vswitch(oft) will never be regarded as tautology, while with refer­ ence to the obvious intended interpretation it is always true - the switch must be either in on or off posi­ tion. Further, the approaches to completeness verifi­ cation given in literature [Cragun and Steudel, 1987; Suwa et al, 1984] based on inspection of possible cases (states) do, in principle, make use of the physical com­ pleteness. Thus, it may be in order to modify the defini­ tion of bd-resolution towards covering this case, as well. Below, a formal definition of generalized bd-resolution is proposed. ,

Definition 6 (Generalized bd-resolution)

Let t/J1, t/J2, .. . , t/J" be some simple formulae , such that t/J1 = t~J<1> /1. q1 , t/J2 = t~J<2> /1. q2 , ... , t/Jk = t~J<k> /1. qk and let there exist a most general unifier (mgu) u for q 1 , q 2 , . . . , q" . Let I denote the intended interpretation. If FI q 1 u V q 2 u V . .. V qku then, a formula t/J

will be called a generalized backward dual resolvent (generalized bd-resolventJ of t/J1, t/J2, ... , t/Jk.

We shall prove that with regard to the intended in­ terpretation I the alternative of the parent formulae t/J1, t/J2, ... , t!J" is a logical consequence of the generalized bd-resolvent defined by (5) .

Theorem 3 (Correctness of generalized bd-reso­ lution) Let t/J be a generalized bd-resolvent defined as above {5). Then, if FI t/J then FI t/J1 V t/J2 V ... V t/Jk.

Proof Let us assume that t/J is satisfied under interpre­ tation I , which is the intended one, i.e. FI t/J . Thus FI t~J< 1 >u, FI t!J<2>u, ... , FI t~J<k>u . From assumption, FI q 1 u V q 2 u V ... V qku, and thus for at least one i E {1, 2, .. . , k} there is FI qiu. Hence, obviously FI t~J<i> u /1. q;u for at least one i E {1 , 2, .. . , k }, as well. Since turning constants (terms) into existentially quan­ tified variables only "improves" satisfiability (existential quantifier introduction), there is also FI t/Ji for at least one i E { 1, 2, ... , k} and obviously FI t/J1 V t/J2 V ... V t/Jk, i.e. the alternative of initial formulae is satisfied, Q.E.D.

With regard to the presented logical approach, the fol­ lowing algorithm can be suggested for checking specific completeness with regard to a given formula 'If. Note that for checking logical completeness it is enough to replace 'If with T .

Algorithm for checking completeness

1. Build a formula describing the sum of all the appro­ priate precondition formulae (the normal formula of the form 'li'1 V 'li'2 V ... V 'li'~;).
2. Perform any possible derivation ofbd-resolvent, e.g. by applying the level-saturation method [Chang and Lee, 1973], or any other complete strategy so as to prove that 'If I= 'li'1 V 'li'2 V ... V 'If~;.
3. If the above logical satisfaction is eventually proved, then the system is complete with regard to 'If.
4. In other case (due to the completeness of the bd­ resolution) the system is incomplete. The derived formulae describe the situations which are "served" (i.e. the system is complete with regard to at least the obtained formulae) .

Note, that the generation of bd-resolvents is not guar­ anteed to stop. However, for finite physical systems the number of possible states is finite, and thus the num­ ber of situations is finite as well. Since our goal is to "cover" the state space, the situation formulae less than or equally general to some previously generated ones can be eliminated from further derivation. Taking into ac­ count that any bd-resolvent is less than or equally gen­ eral to the alternative of the two "mother" formulae one can expect to eventually 'cut ' all the branches of the tree of potential derivations.

4 Examples

Let us analyze an example given in [Cragun and Steudel, 1987], p.635. in TABLE 1. There are given seven rules with the following Boolean preconditions R~-R7.

R1= chatter 1\ edge..de:formation, R2= chatter 1\ -,edge..deformation 1\ tool..brealtage, R3= chatter 1\ -,edge..deformation/\ -,tool ..breakage, R4= -,chatter 1\ edge..deformation 1\ tool..brealtage, R5= -,chatter 1\ edge..deformation/\ ....,tool ..breakage, R6= ....,chatter 1\ -,edge..deformation/\ tool ..breakage, R7=

....,chatter 1\ -,edge..deformation 1\ ....,tool..brealtage. Let us apply the above algorithm to check whether the set of rules of the above preconditions is complete. The following example inferences can be performed (in parentheses parent formulae are given):

Since an empty tautology formula was deduced with use of bd-resolution, the set of rules is complete.

Now, let us consider a more complex example. Let there be given a rule-based system for automatic con­ trol of some object. The rules define the actions which are to be performed while certain input signals occur . There are three input signals, namely inputl, input2, and input3. Each input signal can be of low, medium, or high intensity. To denote the level of certain signal we shall use the predicate level(<signal>,<intensity>). There are four control rules which define admissible ac­ tions to be performed. The preconditions of the rules are given by the following formulae:

P1 level(inputl, low) 1\ -,level(input2,high) 1\ ....,level( input3, high), P2 level( inputl, high) 1\ -,level( input2, low) 1\ ....,level(input3, low), P3 level(inputl,medium) P4 level(X, low) 1\ level(Y, high).

We attempt to check if the specified rules are complete, i.e. if in any state, there is at least one rule which can be applied. The bd-derivation can proceed as follows:

1. level(inputl, low) 1\ ....,level(input2, high); (Pl ,

P4)

the unifying substitution is {Y /input3}. Fac­

torization is performed by applying substitution

{X/inputl},

1. level(inputl, low); (1, P4) the unifying substitution is {Y f input2} . Again, factorization is performed by applying substitution {X/inputl},
2. level( ~nputl, high) 1\ -,level( input2, low); (P2, P4) the unifying substitution is {X/input3}. Fac­ torization is performed by applying substitution {Y/inputl}.
3. level(inputl,high) (3, P4) the unifying substitution is {X/input2}. Again, factorization is performed by applying substitution {Y/inputl}.

At this stage, one can notice that any physical state will be served by the system, since formulae P3, 2, and 4 cover all the possible states (the whole state-space) . In fact, the alternative of these formu­ lae is level(inputl,low) V level(inputl,medium) V level(inputl, high), and there are no other possibilities in our system. However, in order to prove this formally, one is to replace P3 with the following formula:

P3' ....,level(inputl, low) 1\ ....,level(inputl,high),

which, according to the interpretation of the consid­ ered system is logically equivalent to P3. Now, the de­ duction can be completed:

5 . ....,level( inputl, high), 6. T. (2, P3') (4, 5)

Thus, the above system of rules is .complete; i.e. m any state .at least one of the rules is applicable.

Note that with use of generalized bd-resolution one can directly generate 6 from P3, 2 and 4. In fact, by putting q 1 = level(inputl, low), q 2 level(inputl,medium), and q 3 = level(inputl,high) we have F= 1 q 1 V q 2 V q 3 , where I is the assumed in­ terpretation. The direct application of generalized bd­ resolution simplifies the proof and makes it shorter.

In case of incomplete systems, bd-resolution can be used for generating formulae which describe the states for which there are some actions specified, i.e. for prov­ ing specific completeness. Some other application exam­ ples can be found in [Lig~za, 1992b].

5 Conclusions

The proposed approach based on first order logic and theorem proving dual to resolution method provides the­ oretical bases for improving the design of knowledge based systems. It suggests a possibility of checking the system for completeness based on first-order logic rather than simple exhaustive inspection of possible parame­ ters/conditions combinations. However, as shown in the above examples, it is likely that for practical applica­ tions the proposed algorithms should be equipped with domain-specific knowledge concerning the intended in­ terpretation. Moreover, hierarchization mechanisms and possibly -heuristics would further improve the efficiency of this method.

The advantage of bd-resolution over classical one with respect to completeness verification consists in direct ap­ plication of the method to formulae describing situations and preconditions in a simple, consistent with intuition way. Moreover, in case of incomplete systems, gener­ ation of formulae describing specific completeness (the states actually served) is straightforward.

The approach can be applied to rule-based systems, where precondition formulae are in the form of normal formulae defined here. Logical explicit negation should be used rather than the implicit one. For practical rea­ sons, the proposed generalized bd-resolution taking the advantage of knowing the intended interpretation is pro­ posed; its application can improve efficiency of the pro­ posed paradigm.

The outlined method is primarily aimed at applica­ tion to "single-layer" rules (such as the ones applied for control in knowledge-based control systems- see, for ex­ ample [Tzafestas and Lig~za, 1989; Lig~za, 1992b]); how­ ever, it seems that it can be useful for other systems with chaining rules if a hierarchization with regard to a con­ text similar to the one of [Cragun and Steudel, 1987] is performed. Further, it is likely that the combination of the described approach with methods based on exhaus­ tive test can be promising.