On the Relation of Resolution and Tableaux Proof Systems for Description Logics

1 Introduction

Recently a number of results concerning resolution de­ cision procedures for subclasses of first-order logic have been obtained. The considered subclasses are expres­ sive enough to encompass a variety of non-classical log­ ics, in particular, description logics and extended modal logics. De Nivelle [1998] describes a resolution decision procedure for the guarded fragment using a non-liftable ordering refinement. The guarded fragment is a general­ isation of the restricted quantifier fragment correspond­ ing to basic modal logic and allows for the embedding of a variety of extended modal logics and description logics [Gradel, 1998]. Expressions and knowledge bases of the description logic A.CC can also be embedded into Maslov's class K and its subclasses One-Free [Fermiiller et al., 1993] and the class of DL-clauses [Hustadt and Schmidt, 1999]. Again, ordering refinements of resolu­ tion provide decision procedures for these classes. A non­ standard translation into the Bernays-Schonfinkel class combined with resolution and arbitrary refinements pro­ vide decision procedures for the satisfiability of A.CC ex­ pressions [Schmidt, 1999]. This approach was adopted in the experiments of Hustadt, Schmidt, and Weiden­ bach [1997; 1998]. Experiments using the standard translation and a combination of a first-order theorem prover au&mented with a finite-model finder are de­ scribed in lParamasivam and Plaisted, 1998].

The problem of empirical investigations based on com­ petitive testing is the difficulty in identifying the major factors having a positive or negative influence on the per­ formance of a theorem prover. As long as the theorem provers which are being compared follow different proof strategies this difference is likely to have a dominating effect on the overall performance. This has· two conse­ quences. One, we can say little about the other factors influencing the performance, for example, fundamental differences between the underlying proof systems or so­ phisticated redundancy elimination techniques used by the theorem prover. Two, while it is easy to find bench­ mark problems illustrating the superiority of one theo­ rem prover it is just as easy to find benchmark problems showing the opposite. Therefore, it is always advisable to complement empirical investigations with a theoreti­ cal analysis of the relative ·proof and search complexity of the underlying proof systems. In the first case, the task is to determine whether a proof system A is able to polynomially simulate a proof system B. This is to say, for any given theorem <P there is a function g, com­ putable in polynomial time, mapping proofs of ¢ in B to proofs of <P in A. In the second case, the task is to determine the relative size of the search space, that is the potential number of inference steps performed until a proof is found [Plaisted and Zhu, 1997].

In this paper we focus on the aspect of relative proof complexity of tableaux proof systems and res­ olution proof systems for the description logic A.CC with general terminological sentences and ABox ele­ ments. This logic is of particular interest, since all tableaux proof systems presented in the literature re­ quire some form of blocking or loop-checking to force termination [Buchheit et al., 1993; Donini et al., 1996; Horrocks, 1997]. We describe a resolution proof system based on a selection refinement of resolution, instead of an ordering refinement, which provides a new resolution decision procedure for this logic. We show that this proof system is able to polynomially simulate tableaux proof systems for this logic. The technique for simulat­ ing blocking described in this paper can also be applied for obtaining other simulation results, for example, ana­ lytic modal KE tableaux proof systems or sequent proof systems for modal logics.

The structure of the paper is as follows. Section 2 de­ fines the syntax and semantics of A.CC and describes a standard tableaux proof system. We adopt the resolu­ tion framework of Bachmair and Ganzinger [1998] which is described briefly in Section 3. Section 4 presents the simulation result for the tableaux proof system and Sec­ tion 5 shows how termination of the resolution proof sys­ tem can be enforced in analogy to blocking in tableaux systems. In Section 6 we discuss some optimisations which are naturally available in the resolution framework and can be transferred to the corresponding tableaux proof systems.

2 Inference for A.CC

We work with a signature given by a tuple I: = (0, C, R) of three disjoint alphabets, the set C of concept sym­ bols , the set R of role symbols, and the set 0 of objects. Concept terms (or just concepts) are defined as follows. Every concept symbol is a concept. If C and D are con­ cepts, and R is a role symbol, then T, 1_, C n D, CUD, ·C, '</ R.C, and 3 R.C are concept terms. A concept symbol is also called a primitive concept.

A knowledge base has two parts: A TBox comprising of terminological sentences of the form C ~ D and an ABox comprising of assertional sentences of the form a E C and (a, b) E R, where C and Dare concepts, R is a role, and a and b are objects.

Although the language does contain any role forming operators, it is still possible to express properties of the domain and range of a role R [Buchheit et al., 1993].

The semantics is specified by the embedding into first­ order logic as follows . For sentences:

where g and Q are constants uniquely associated with a and b. For terms:

where X and Y are meta-variables for variables and con­ stants, and PA (respectively PR) denotes a unary (bi­ nary) predicate symbol uniquely associated with the con­ cept symbol A (role symbol R). The variable y is distinct from X.

All common inferential services for knowledge bases, like subsumption tests for concepts, TBox classification, realization, retrieval, can be reduced to tests of the satis­ fiability of a knowledge base. Our definition of a tableaux proof system, also called a constraint system, largely follows Buchheit et al. [1993]. All terminological sen­ tences C ~ D are assumed to have been replaced by T ~ -.C U D and all concepts in the resulting knowl­ edge based are assumed to have been transformed into negation normal form.

Let I be a subset of 0 such that no element of I occurs in r . Let -<1 be a well-founded total ordering on I. The elements of I are called introduced objects. We assume that the elements of I are introduced during inference according to -<1, that is, if a is introduced into r, then for all b E I with b -<1 a, b already occurs in f.

Following Buchheit et al. [1993] we define the following set of transformation rules for the purpose of testing the satisfiability of a knowledge base:

1. r =>n r U {a E C,a ED}, if a E (C n D) is in f, and a E C and a E D are not both in r.
2. r =>u r U {a E E}, if a E (CUD) is in r, neither a E C nor a E D is in f, and E = C or E = D.
3. f =>3 f U {(a,b) E R,b E C}, if a E 3R.C is in r, there is no d such that both (a, d) E R and d E C are in f, bE I is a newly introduced object.
4. r =>v ru {bE C}, if a E '<IR.C and (a, b) E Rare in f, and b E C is not in f.
5. f => 1. f U {a E 1_}, if a E A and a E ·A are in r, where A is a concept symbol.
6. r =>c r U {a E C}, if a occurs in rand a sentence T ~ C is in f, and a E C is not in f.

Let =>r.AB be the transitive closure of the union of the transformation rules given above. A knowledge base r contains a clash if a E l_ is in f. A knowledge base r is satisfiable if there exists a knowledge base r' such that (i) r =>r.AB r') (ii) no further applications of =>r.AB to r' are possible, and (iii) f' is clash-free. Note that the rule =>u is don't know nondeterministic.

3 The Resolution Framework

As usual clauses are assumed to be multisets of liter­ als. The components in the variable partition of a clause are called split components, that is, split components do not share variables. A clause which is identical to its split component is indecomposable. The condensa­ tion Cond( C) of a clause C is a minimal subclause of C which is a factor of C.

The calculus is parameterised by an ordering >- and a selection function S. The ordering has to satisfy cer­ tain restrictions as detailed in [Bachmair and Ganzinger, 1998], in particular, it is required to be a reduction or­ dering. A selection function assigns to each clause a possibly empty set of occurrences of negative literals. If C is a clause, then the literal occurrences in S(C) are selected. No restrictions are imposed on the selection function.

The calculus consists of general expansion rules (over clause sets)

each representing a finite derivation of the leaves N1 , ... , Nk from the root N. The following rules de­ scribe how derivations can be expanded at leaves.

Deduce:

N

N u {Cond(C)}

if C is either a resolvent or a factor of clauses in N.

Delete:

if C is a tautology or N contains a clause which is a variant of C.

if C and D are variable-disjoint.

Resolvents and factors are derived by the following rules .

where (i) C7 is the most general unifier of A1 and A2, (ii) no literal is selected in C and A1 C7 is strictly >--maximal with respect to CO", and (iii) -.A2 is either selected, or -.A2 e7 is maximal in DO" and no literal is selected in D. C V A1 is called the positive premise and D V ·A2 the negative premise. 1

Ordered Factoring:

where (i) C7 is the most general unifier of A1 and A2; and (ii) no literal is selected in C and A1 C7 is >--maximal with respect to C C7.

Let N be a set of ground clauses. A ground clause C is redundant in N if there are clauses C1, ... , Cn in N such that C1, .. . , Cn are smaller than C with respect to >- and logically imply C. The notion of redundancy is lifted to the non-ground case in the expected way. An inference is redundant if one of the parent clauses or its conclusion is redundant.

Theorem 1 (Bachmair and Ganzinger [1998]).

Let N be a set of clauses. Then N is unsatisfiable iff the saturation of N up to redundancy contains the empty clause.

4 Simulation by Resolution

Our intention is to restrict resolution inferences in such a way that admissible resolution steps correspond to in­ ference steps in tableaux proof systems. FUrthermore, the resolution proof system will be a decision procedure whenever the tableaux system terminates without the help of loop-checking or blocking techniques.

It is necessary to modify the translation mapping II slightly. Without loss of generality, all expressions oc­ curring in r are assumed to be in negation normal form. Let ~ be a concept symbol not occurring in r. Intu­ itively, ~ has the same semantics as the concept symbol T. But while T is translated to the true formula and will vanish during the conversion to clausal form, the translation treats ~ as an ordinary concept symbol. By adding certain formulae to the translation of the knowl­ edge base we provide sufficient information about ~ to ensure that the introduction of ~ preserves satisfiability equivalence. This allows us to obtain the desired com­ putational behaviour in our resolution proof system.

1 As usual we implicitly assume that the premises have no common variables.

The modified translation IT is defined as follows .

The occurrence of 1r(~, x) on the left-hand side of the implication ensures that all clauses in the clausal form contain the negative literal ·p.(x) . Since

it is immaterial whether the terminological sentences in r take the first or second form.

The conversion to clausal form of first-order formulae resulting from the translation of A.CC knowledge bases, makes use of a particular form of structural transforma­ tion 2 [Baaz et al., 1994), which is based on two map­ pings 21 and 22.

Let Pos( ¢>) be the set of positions of a formula ¢> . If A is a position in ¢>, then ¢>1>. denotes the subformula of ¢> at position A and 1/>[A+-1/J] is the result of replacing ¢> at position A by 1/J. We associate with each element A of A ~ Pos( ¢>) a predicate symbol Q >. and a literal Q >. (x1, ... , Xn), where the Xi are the free variables of ¢>1>., Q>. does not occur in ¢> and two symbols Q>. and Q>.' are equal iff¢>>. and ¢>>.' are variant formulae . 31 uses definitions of the form

Now, define DefA(¢>) inductively by: Def0(¢>) =¢>and

where A is maximal in AU {A} with respect to the prefix ordering on positions. Let Posd( ¢>) be the set of positions of subformulae of ¢> corresponding to positions of non­ primitive concepts in the knowle<!ge base f. By 3 1 we denote the transformation taking II(f) to its definitional form

Note that in this case, every predicate symbol Q>. is a unary predicate associated with a concept C (although not necessarily uniquely associated). Thus, we will henceforth denote Q>. by PC· By 22 we denote the func­ tion which produces for every unary predicate symbol p occurring in 21ll(f) the conjunction of all formulae

Theorem 2. Let f be any knowledge base. 3ll(f) can be computed in polynomial time, and r is satisfiable iff 3ll(f) is satisfiable.

The clausal form of 2ll(f) consists of three types of clauses: (i) clauses stemming from terminological axioms which all contain an occurrence of the negative literal ·py(x), (ii) clauses stemming from formulae introduced by S1 and S2 which all contain an occurrence of some negative literal·pc(x), and (iii) clauses originating from the translation of assertional sentences which are ground unit clauses.

Our selection function STAB selects the literal ·P· (x) in clauses of type (i) and ·pc(x) in clauses of types (ii). In addition, a binary literal of the form 'PR(s, t) is selected whenever s is a ground term and t is a variable. All clauses stemming from a terminological sentence or from an additional formula introduced by 3 contain negative literals, one of which is selected. We will mark selected literals by ·+· For Theorem 3 an arbitrary reduction ordering >-- may be used.

For every concept C and every role R, which may pos­ sibly occur in a knowledge base during a satisfiability test, there exist correspon<_!!ng_Eredicate symbols pc and PR in the clausal form of SII(r). Likewise every object a is associated with a term ta.

We show that every application of one of the trans­ formation rules is simulated by at most two resolution inference steps.

1. The =>n rule, by two resolution inference steps between the ground clause {PcnD(ta)} and clauses { ·PcnD(x)+,Pc(x)} and { ·PcnD(x)+,PD(x)}, generat­ ing the resolvents {pc(ta)} and {PD(ta)}.

2. The =>u rule, by an inference step between the ground unit clause {PcuD(ta)} and { ·PcuD(x)+,Pc(x),PD(x)}, followed by an application of the splitting rule to the conclusion {pc(ta),pD(ta)} which will generate two branches, one on which the set of clauses contains {pc(ta)} and one on which it contains {PD(ta)}.

3. The =>3 rule, by resolution inference steps between the clauses {P3R.c(ta)}, { 'P3R.c(x)+,PR(x, j(x))}, and { 'P3R.c(x)+,Pc(f(x))}. This will add {PR(ta, f(ta))} and {pc(/(ta))} to the clause set. The term j(ta) cor­ responds to the object b E I introduced by the =>3 rule, that is, tb = f(ta).

4. The =>v rule, by two consecutive resolution infer­ ence steps. Here, the set of clauses contains {PvR.c(ta)} and {PR(ta, tb)}. First, the clause {PvR.c(ta)} is re­ solved with {·PvR.c(x)+,'PR(x,y),pc(y)} to obtain the clause { 'PR(ta, Y)+,Pc(y)}. Then the conclusion is resolved with {PR(ta, tb)} to obtain {pc(tb)}.

5. The=> ..L rule, by two consecutive inference steps using {PA(ta) }, {P~A(ta)}, and { ·P~A(x)+, ·PA (x)} (which is the clausal form of the definition of ·A) to derive the empty clause.

6. The =>c rule is simulated as follows. Since the ob­ ject a occurs in r, the corresponding term ta occurs in our set of clauses. In particular, there is a ground unit clause {PD(ta)}, a clause {·PD(x)+,P·(x)} introduced by S2, and a clause {·py(x)+,Pc(x)} stemming from the translation of the terminological sentence T ~ C. By two resolution inference steps we obtain {Pc(ta)} which corresponds to the sentence a E C added by =>c tor. Note that all the inference steps strictly obey the restric­ tions enforced by the selection function STAB and are in accordance with the resolution calculus. This proves:

Theorem 3. The resolution proof system with selection function STAB p-simulates the tableaux proof system for A.CC.

Interestingly, factoring plays no role for the clause sets under consideration, that is, the only possible factoring steps are condensations of ground conclusions. More­ over, no resolution inference steps other than those of the simulation are possible. Thus, the following stronger result holds.

Theorem 4. Let r be a knowledge base and N the clausal form of 3rr(r). Then the search space of the resolution procedure for N can be polynomially reduced to the search space of the tableaux procedure for r.

5 Termination

By C(r, a) we denote the set of all concep' ':such that a E C is an element of the knowledge · _,e r. Two objects a, b E I are r -equivalent, denoted by a =:r b, if C(r, a) = C(r, b). If b -<1 a and a =r b, then b is a witness for a. Similarly, let P(N, t) denote the set of predicate symbols {p I {p(t)} E N} in a clause set N. (Remember whenever a E ·A is an element of r, then the positive clause {P~A(ta)} is an element of N.)

The strategy (S) employed by Buchheit et al. [1993) restricts the application of rules as follows: (i) apply a transformation to an introduced object only if no rule is applicable to an object a E 0 \ I, (ii) apply a rule to an introduced object a only if no rule is applicable to an introduced object b such that b -<1 a, (iii) apply =>3 only if no other rule is applicable, and (iv) apply =>3 to an introduced object a in r only if there is no witness for a. Restrictions (i)- (iii) ensure that whenever =>3 becomes applicable to an introduced object a in a knowledge base r, then for every r' with r => * r' we have C(r, a) = C(r', a). The strategy guara~es the termination of the tableaux proof system.

Restriction (iv) may be viewed as an instance of the Leibniz principle, identifying two objects which are in­ distinguishable with respect to their properties. Since we confine ourselves to ·applications of this principle to introduced objects, it is sufficient to consider properties expressible by concepts. In this case, the principle can be expressed as a set of first-order formulae of the form

with the antecedents representing all possible truth as­ signments to concepts and subconcepts occurring in r. (That is, each pc, corresponds to a concept C; in rand for every subconcept C in r, either pc or P~c occurs in each formula.) The notion of =r-equivalence also has a non-monotonic aspect: During a tableaux derivation it can happen that a =r b at one state and a t:r b at a later state. But restrictions (i)-(iii) ensure that eventually ei­ ther a =r b or a t:r b holds for all future states in the derivation. Furthermore, it is assumed that for concepts C not occurring in C(r, a) or C(r, b) we can assume that neither a nor bare in the semantical interpretation of C.

To account for these aspects and to reduce the com­ putational overhead introduced by these formulae we choose to add a special expansion rule instead.

Blocking: N

where (i) ta and tb are distinct ground, functional terms, and (ii) P(N, ta) = P(N, tb)· ('::::::'is the equality symbol.)

This rule is sound. Using the correspondence between the application of one of the propagation rules and par­ ticular resolution inference steps, we can restrict our­ selves to a corresponding strategy in the resolution proof system. It follows that whenever resolution inference steps corresponding to =}3 become applicable to a term ta in the clause set N, then for every clause set N' deriv­ able from N we have P(N,ta) = P(N',ta).

On the basis of the ordering ~~ on introduced objects we will now define a reduction ordering >-T.AB · Suppose a and b are introduced objects and ta and tb are the corre­ sponding terms according to the simulation result above. Let >-T...w be a reduction ordering with the following prop­ erties: (i) if b ~~ a then ta >-T.AB tb, and (ii) for arbitrary non-equality atoms A, if ta >-TAB tb, then A[ta) >-T...w A[tb] and A[ta] >-T...w (ta :::::: tb)· It is not difficult to show that such a reduction ordering exists. Note that it is sufficient that only ground expressions are ordered by >-T.AB·

Assume now that by restriction (iv) of strategy (S) the rule =}3 is not applicable to an introduced object a in r, because there is a witness b for a. Then there are terms ta and tb such that P(N, ta) = P(N, tb)· In this situation an application of the blocking expansion rule will add an equation { ta :::::: tb} to N. Since b ~~ a, it follows ta >-T.AB tb, and the ground clauses {Pc(tb)} and {tb :::::: ta} are smaller than {pc(ta)} with respect to >-T...w· Also, {Pc(tb)} and {tb :::::: ta} logically imply {pc(ta)}. Consequently, the clause {pc(ta)} is redun­ dant and does not participate in any further inferences. This mimics restriction (iv) of strategy (S). To establish logical implications of this form, the redundancy elimi­ nation algorithm will require some form of equality rea­ soning, for example, superposition. In our special case, all that is required are one-step rewrite transformations.

Theorem 5. The strategy (S) for tableaux proof systems can be polynomially simulated by blocking and redun­ dancy elimination as outlined above.

It is now straightforward to show that any inference in our resolution proof system terminates.

Theorem 6. Let r be a knowledge base and let N be the clausal form of 3IT(f). Then any derivation from N by (ordered) resolution with selection as determined by ST...w and blocking following the strategy outlined above terminates.

Corollary 7. The resolution proof system and the tableaux proof system have the same time complexity, namely NEXPTIME [Buchheit et al., 1993}.

6 Optimisations

In practice a principal cause for intractability is the pres­ ence of a large number of terminological sentences. Ev­ ery application of the '*c rule to an object a and ter­ minological sentence T ~ ·C U D will be followed by an application of '*u to a E ·C U D . The number of branches in the search space generated in this way is too large to be manageable for implementations relying on chronological backtracking to systematically investigate all the branches.

As indicated by Horrocks and Patel-Schneider [1998) arid Hustadt and Schmidt [1998) one possible optimisa­ tion is the use of more sophisticated backtracking tech­ niques like backjumping or branch condensing. However, it is even more desirable to avoid unnecessary branching in the first place. A closer look at the intention be­ hind the introduction of · in the modified translation IT reveals one possible optimisation in this direction. Sup­ pose the knowledge base contains a terminological sen­ tence of the form ·A ~ C. Using the standard embed­ ding II we obtain a clause {PA(x),pc (x)} which contains no negative literal we could select. Using IT we obtain {·p-.(x) ,PA(x),pc(x)} which contains a selectable lit­ eral. However, whenever for a terminological sentence C ~ D, the concept nnf(·C) U D contains a negative occurrence of a primitive concept A, the corresponding clauses under the standard embedding II will contain a selectable negative literal ·PA ( x). The transformation 3 1 is modified such that these occurrences are preserved. Now the selection function can select an arbitrary nega­ tive literal. For example, if we have a terminological sen­ tence of the form A1 n .. . nAn ~ C, the selection function can choose an arbitrary 'PA, (x) among the negative lit­ erals in C1 = {·PA 1 (x) , ... ,·PAn(x),pc(x)}. This pre­ vents any inference with C1 until a unit clause {Ai(ta)} has been derived. Independent of these consideration, this optimisation has been incorporated in the FaCT sys­ tem [Horrocks, 1997].

From correspondences with propositional dynamic logic it is known that the satisfiability problem for gen­ eral A.CC knowledge bases is in EXPTIME. The algo­ rithms presented in Sections 2 and 4 require double ex­ ponential time in the worst case. Buchheit et al. [1993) note that this can be improved by caching contradic­ tory sets C(r, a) of previously investigated branches in­ troduced by applications of the '*u rule. This has been formalised in [Donini et al. , 1996). Evidently, this form of caching will have the same effects for the resolution procedure described in this paper.

7 Conclusion

The prime motivation for this work has been our in­ terest in possible links between different proof systems for description logics and modal logics. This paper fo­ cuses on a particular tableaux proof system for descrip­ tion logics with general inclusion sentences and shows how this system and certain optimisations can be sim­ ulated with polynomial overhead in the context of resolution. Our results provide new insight into the relative proof complexity of these systems similar to correspond­ ing results for propositional logic. Although we have considered only the logic A.CC, our results may be ex­ tended to description logics with role conjunction and role hierarchies. We expect similar results can also be obtained for other forms of tableaux proof systems or se­ quent calculi. Resolution procedures following tableaux proof strategies have the advantage that proofs may be easily translated back into tableaux or sequent-style proofs of the original source logic. Related work on backward translation is by Caferra and Demri [1993; 1995].

The resolution decision procedure described in this paper offers just one of many possible search strate­ gies. Other resolution strategies utilised in the litera­ ture, mentioned in the Introduction, are implemented by ordering strategies which do not rely on blocking or loop-checking techniques. Such techniques are also not needed in the ordered chaining calculus for modal log­ ics with transitive modalities, or A.CC with transitive roles [Ganzinger et al., 1999].

Although experimental results with SPASS using or­ dered resolution are encouraging [Hustadt and Schmidt, 1997; Hustadt et al., 1998], there are clas~s of prob­ lems on which tableaux proof systems have '!better per­ formance. The results of this paper now provide a ba­ sis for the scientific testing of the comparative perfor­ mance of the two orthogonal strategies for resolution proof systems, and for establishing guidelines indicating which strategy is most appropriate for particular classes of problems.