A Correspondence Theory for Terminological Logics: Preliminary Report

1 Motivation

We shall establish correspondences between terminolog­ ical logics and propositional modal and dynamic logics. These correspondences turn out to be highly produc­ tive because formerly unrelated fields are brought to­ gether. In the area of terminological logics, running sys­ tems such as BACK, CLASSIC, KL-ONE, KRYPTON, and LOOM have been developed since the late seven­ ties. Only recently theoretical investigations have been undertaken mainly concerning the computational complexity of terminological logics. 1 In the very contrast to that, elaborated theories for modal and dynamic log­ ics have been developed much earlier. 2 Particularly for modal logic there is-apart from first order logic-the most elaborated theory, and dynamic logic has bene­ fited from these results. By detecting these correspon­ dences, we gain new insights into terminological logics solely by expounding the theorems of modal and dy­ namic logic as theorems of the corresponding termino­ logical logic. There can also be redundant research if correspondences are overlooked. For instance, Ladner [1977] showed that the propositional modal logic K(m) is PSPACE-complete, and twelve years later this was reproved by Schmidt-SchauB and Smolka [1991] for its notational variant A.CC.

*T his work was partially supported by the Commission of the European Communities and is part of the ESPRIT Project 5210.

2 Preliminaries

To understand the complexity results to be presented, you should know the complexity classes P, NP, PSPACE, and EXPTIME: P is the class of problems decidable in deterministic polynomial time, NP are those problems decidable in nondeterministic polynomial time, PSPACE are the problems decidable in deterministic polynomial space, and EXPTIME are those problems decidable in deterministic exponential time. Furthermore, you should know that a problem L is PSPACE-comp/ete iff both L E PSPACE and each problem in PSPACE is log space reducible to L; a problem M is log space reducible to L iff there is a function f : M -+ L computable in space log (and therefore also computable in polynomial time) such that for all x, x EM iff f(x) E L. Be aware of the complexity hierarchy P ~ NP ~ PSPACE ~ EXPTIME for which it is only known that P :f. EXPTIME.

3 Terminological Logics and Modal Logics

We first consider a terminological logic investigated by Schmidt-SchauB and Smolka [1991], named A.CC. Like any other terminological logic, A.CC comprises concepts, denoting sets, as well as roles, which denote binary rela­ tions. Contrary to roles, concepts can be compound, viz . by intersection n, union U, complementation-., and the value restrictions V. and 3. taking a role and a concept as their arguments. V R.C is to be read as "all objects for which all R's are in C ," whereas 3R.C is to be read as "all objects for which there exists an R in C." So we can express concepts such as 'mothers having only sons' by the A.CC-expression womenn-.menn(3child.men)nVchild.(menn-.women).

1 Confer [Nebel, 1990] for a good overview of the systems and the complexity results.

2 For the history of modal logic confer [Hughes and Cress­ well, 1984], and for that of dynamic logic confer [Hare!, 1984].

Formally, A.CC is given by the following formation rules, where c denotes a concept symbol and r a role symbol:

As usually, we specify the formal semantics of A.CC by an extension function. Let V be any set, called the domain. An extension function £ over V is a function mapping concepts to subsets of V and roles to subsets of V x V such that

Using extension functions, we can define the seman­ tic notions subsumption, equivalence, and coherence: D subsumes C, written f= C ~ D, iff for each extension function£, £(C] ~ £[D], whereas C and D are equiva­ lent, written f= C = D, iff for each extension function £, £[C] = £[D]. Finally, Cis coherent iff there is an ex­ tension function £ with £[C] =/= 0, called a model for C; otherwise C is incoherent. The following lemma justifies merely investigating subsumption in A.CC:

Lemma 1 Subsumption, equivalence, and incoherence are log space reducible to each other in any terminological logic comprising Boolean operations on concepts.

Proof: Since f= C ~ D iff f= C n D = C, subsumption is log space reducible to equivalence in presence of n. Equivalence in turn is log space reducible to incoherence in presence of n as well as ....., because f= C = D iff ( C n -.D) u (D n -.C) is incoherent. And finally, incoherence clearly is log space reducible to subsumption in presence of ---, T since C is incoherent iff f= C ~ ---, T . 0

We take the union of concepts U and the operation 3. dual to V. with £[3R.C] = {dE V : 3(d, e) E £[R].e E t'[C]} as abbreviations for linearly length-bounded A.CC­ expresstons:

It is well known that A.CC is a sub language of first or­ der logic since atomic concepts correspond to one-place predicates and atomic roles to two-place predicates. The A.CC-concept -.c1 U Vr.(c2 n c3 ), for instance, can be ex­ pressed by the first order formula ·c1(x) V Vy.r(x, y)::::} c2(y) 1\ ca(y).

Viewing A.CC from the modal logic perspective, atomic concepts simply can be expounded as atomic propositional formulae, and can be interpreted as the set of worlds in which the atomic propositional for­ mula holds . In this case V. becomes a modal operator since it is applied to formulae. Thus ·c1 U Vr.(c2 n c3 ) can be expressed by the propositional modal formula -.cl V Kr(c2 1\ ca). Kr(c2 1\ ca) is to be read as "agent r knows proposition c2 1\ ca," and means that in every world accessible for r, both c2 and c3 hold. Actually

• the domain of an extension function can be read as a set of worlds.
• atomic concepts can be interpreted as the set of worlds in which they hold, if expounded as atomic formulae.
• atomic roles can be interpreted as accessibility rela­ tions.

Hence VR.C can be expounded as "all worlds in which agent R knows proposition C" instead of "all objects for which all R's are in C."

It is not essential for the following to know propo­ sitional modal logic except for establishing the corre­ spondence. To begin with, we inductively fix the syn­ tax of Kern)· The atomic propositions Pl,P2, ... as well as true are Kem)-formulae, and, if a and {3 are Kernt formulae, so are a 1\ j3, ·a, K1 a, ... , and Krna. The meaning of a Kem)-formula is given by a Kripke struc­ ture M = (V, 1r, P1, ... , Pm}, where Vis any set of worlds, P1, ... , Pm ~ V x V are accessibility relations, and 1r is a truth assignment mapping atomic propositions to sub­ sets of V. d E 1r(p) says that p holds in the world d, and dP;e denotes that in world d agent i consid­ ers world e to be possible. We call Kern) normal be­ cause there are no restrictions on the accessibility rela­ tions. The denotation of arbitrary formulae is given by a valuation VM mapping K(m)-formulae to subsets of V. VM is uniquely defined w.r.t. a Kripke structure M = (V, 1r, P1, ... , Pm} by VM(true) = V, VM(P;) = 1r(p;), VM(a /\j3) = VM(a) n VM(f3), VM(-.a) = 'D \ VM(a), and VM(Kia) ={wE V: V(w,w'} E P;.w' E VM(a)}. Now a K(rn)-formulaa is satisfiable iff there is a valuation VM with VM(a) =/= 0, and a is valid iff -.a is not satisfiable. For a slightly more comprehensive introduction to Kern) confer [Halpern and Moses, 1985].

To establish the correspondence, consider the function f mapping A.CC-concepts to Kern)-formulae with f(c) = c, f(T) = true, f(C n D) = f(C) 1\ f(D), f(-.C) = ·f(C), and f(VR.C) = KRf(C). It could easily be shown by induction on the complexity of A.CC-concepts that f is a linearly length-bounded isomorphism such that an A.CC-concept C is coherent iff the Kern)-formula f(C) is satisfiable. Hence we can conclude:

Theorem 1 A.CC is a notational variant of the proposi­ tional modal logic Kern), and satisfiability in Kern) has the same computational complexity as coherence in A.CC.

By this correspondence, several theoretical results for Kern) can easily be carried over to A.CC. We immedi­ ately know, for example, that without loss of generality, it suffices to consider either finite A.CC-models of expo­ nential size or a single infinite canonical.A.CC-model ( cf. e.g. [Hughes and Cresswell, 1984]). We shall expose two other outcomes of the correspondence, namely an axiom­ atization of A.CC and the complexity of A.CC somewhat closer.

Proposition 1 (An Axiomatization of A.CC)

The axioms forcing (T, n, --.) to be a Boolean algebra to­ gether with

are a sound and complete axiomatization of A.CC­ equivalence [Lemmon, 1966}.

Now we shall prove that deciding subsumption in A.CC is PSPACE-complete. Of course, this is not a new result, but its proof is much simpler than the original six-page one in [Schmidt-SchauB and Smolka, 1991]. The reason is that Ladner [1977] proved the PSPACE-completeness of validity in K(m) form= 1, and, as Halpern and Moses [1985] noted, this result also holds for each m 2:: 1. Using Theorem 1 and Lemma 1, we can immediately conclude:

Proposition 2 (Complexity of .A.CC)

Deciding subsumption in .A.CC is PSPA CE-complete, even if involving only a single atomic role [Ladner, 1977]. An algorithm for deterministically computing coherence in A.CC in quadratic space is also given in [Ladner, 1977].

4 Terminological Logics and Dynamic Logics

Although concepts can be composed in A.CC, we are not able to form compound roles. To overcome this deficiency, we shall introduce an extension of .A.CC, named T S.C. Based on the role parent, for instance, we can express in T S.C its transitive-reflexive closure by parent·, its inverse role 'has child' by parent- 1 , and the union of the roles parent and parenr 1, for example, by parentUparent- 1 . Thus in TS.C we could formalize the concept 'human beings' as follows:

Beside these operations, T S.C comprises the composi­ tion of roles o and the operation id with id(C) denoting the identity relation over C. Using both we can express, for instance, the role 'mother' by parent o id( women).

To be exact, TS.C is given by the same concept­ formation rule as A.CC together with the role-formation rule

To specify the formal semantics ofT S.C , we addition­ ally require an extension function £ to be a mapping with

The identity role self, the range restriction L defined by £[RLC] = {(d, e) E £[R] : e E £[C)}, and the transi­ tive closure of roles + all can be defined within T S.C:

However, only the first and the second definition are lin­ early bounded in their length whereas the third generally is not . Remarkably, we could have introduced the range restriction L and the role self into the logic and then define id(C) as selfLC.

Now it is important to realize that roles not only can be interpreted as accessibility relations but also as non­ deterministic programs. In this case (d, e) E £[R] de­ notes that there is an execution of the program R start­ ing in state d and ending in state e. To achieve this interpretation

• the domain of an extension function is to be read as a set of program states.
• atomic concepts are to be interpreted as the set of states in which they hold, if expounded as atomic formulae .
• atomic roles are to be interpreted as atomic nonde­ terministic programs.

Using this interpretation, compound T S.C-expressions can be expounded as follows:

• VR.C as "whenever program R terminates, proposition C holds on termination"
• R1 o R2 as "run R1 and R2 consecutively"
• R1 U R2 as "nondeterministically do R1 or R2"
• R* as "repeat program R a nondeterministically chosen number of times 2:: 0"
• R- 1 as "run R in reverse"
• id(C) as "proceed without changing the program state iff proposition C holds"

This illustrates that T S.C corresponds to propositional dynamic logic. Indeed, T S.C could easily be shown to be a notational variant of converse-PDL as given in [Fischer and Ladner, 1979]. There, Tis written as true, CnD as CAD, -.Cas ...... C, VR.C as [R]C, 3R.C as (R)C, Ro S as R;S, RU S as RUS, R-1 as R-, and id(C) as C?.

Theorem 2 T S..C is a notational variant of converse­ PDL, the propositional dynamic logic PDL with the converse-operator. Moreover, satisfiability in converse­ PDL has the same computational complexity as coher­ ence in T S.C.

For an excellent introduction to dynamic logic you may confer [Harel, 1984]. There, one can find a survey of interesting theorems of dynamic logic which can now be expounded as theorems ofT S.C. Hence, for instance, we can narrow down the computational complexity ofT S.C. Fischer and Ladner [1979] showed that PDL-validity is EXPTIME-hard, even if involving only a single atomic program and its transitive-reflexive closure as programs . Using Theorem 2, we can infer:

Proposition 3 (Lower Com pl. Bound ofT Se)

Deciding subsumption in AeC extended with the transitive-reflexive closure of roles is EXPTIME-hard, even if involving only a single atomic role [Fischer and Ladner, 1979].

Concerning the upper comlexity bound, Pratt [1979] gave an algorithm for deciding PDL-satisfiability requir­ ing at most exponential time . As Hare! [1984, Sec­ tion 2.5.6] pointed out, the algorithm can easily be extended to deal with - 1 . The reason is that with­ out loss of generality, we can assume - 1 applied only to atomic roles. To see this, realize that for each & , &[(RoS)- 1 ] = &[S- 1 oR- 1 ], &[(Rus)- 1 ] = &[R- 1 us- 1 ], and &[(R·)-1] = &[(R-1)*] . Using Theorem 2, we know that T Se-coherence is contained in EXPTIME, and therefore T Se-subsumption is in co-EXPTIME. How­ ever , co-EXPTIME is the same as EXPTIME. So we have:

Proposition 4 (Upper Com pl. Bound ofT Se)

Subsumption in T Se can be decided in exponential time [Pratt, 1979, Hare/, 1984, Section 2.2/2.5.6].

As another by-product of the correspondence we gain an axiomatization of TSe which assumes - 1 to be ap­ plied only to atomic roles.

Proposition 5 (An Axiomatization of TSe)

Let C ~ D be defined as C n D = C . The axioms for AeC together with

VRUS.C = (VR.C)n(VS.C)

VRoS.C VR.VS.C

Vid(C).D ...,cuD

VR*.c = cnvR+.c

CnVR* .(...,CUVR.C) C VR*.C

C c Vr.3r-1.C

C c Vr- 1 .3r.C

are a sound and complete axiomatization of T Se­ equivalence [Pratt, 1979, Hare/, 1984, Section 2.5.6].

By the way, the first three axioms indicate that T Se without · and - 1 is reduced to AeC since U, o, id can be eliminated linearly.

The correspondence theorem additionally provides us with an elaborated model theory. The main model theo­ rem for converse-PDL says that it suffices to consider only finite connected models of exponential size. To carry over this result, we call an extension function & over V mapping the atomic roles r1, ... , rm connected iff for every d, e E V, (d, e) E &[(r1Ur! 1 ... UrmUr; 1 )*]. Furthermore, l( C) denotes the length of the concept C re­ garded as a string over T,n,u,...,,V.,o,· ,- 1 , and atoms.

Proposition 6 (Finite TSe-Models)

Every coherent T Se-concept C has a connected model over V with lVI ~ 2 1 (C) [Fischer and Ladner, 1979].

In contrast to that, the finite model property does not hold for T se augmented with the intersection of roles, called TS.C'R. The reason is that every model & for

has an infinite acyclic &[r]-chain.

Proposition 7 (Infinite T sen-Models)

There is a coherent T sen-concept which has no finite model [Hare/, 1984, Theorem 2.35].

Note that this does not mean that T sen is undecid­ able . Actually, the decidability of T sen seems to be unknown. It is known, however , that T se extended with the complementation of roles is undecidable [Hare!, 1984, Theorem 2.34], and that T sen with features is highly undecidable as we shall see in the next section.

4.1 T se with Features

In T se we are able to force, for instance, that something has at least two parents, namely a female and a male one:

Unfortunately, this expression does not stipulate that something has exactly two parents. The reason is that we have expressed 'has mother' as the role parentLwomen. However, 'has mother' rather is a partial function than a relation. If something has a mother, it has exactly one. This suggests to extend T Se with features , denot­ ing atomic partial functions . If mother and father were features, the above expression indeed would force that each human being has exactly one mother and father.

We define :FS.C by the same formation rubs as TS£ execpt that an :FSe-role additionally can be a feature symbol. Moreover, we require an extension function & over V to be a mapping such that for each feature symbol f, £[!] is a partial function mapping V to V.

Note that !I o h and id(C) denote partial functions, whereas h u h, r' and J- 1 generally denote binary relations.

Clearly, features correspond to atomic deterministic programs considered in dynamic logic. Thus [Parikh, 1979, §7] can be read to show that any atomic role r is expressible by fr o (/new)*, where fr is the fea­ ture uniquely corresponding to r and !new is a new fea­ ture. In this manner each non-feature atomic role in aT Se-expression can be eliminated without increasing its length more than linearly. 3 Thus we can assume that the only atomic roles which :FS£ comprises are features. So, it is obvious that :FSe is a notational variant of the deterministic version of converse-PDL.

Theorem 3 :FSe is a notational variant of converse­ DPDL, the deterministic propositional dynamic logic DPDL with the converse-operator. Moreover, satisfiabil­ ity in converse-DPDL has-up to linear time-the same computational complexity as coherence in :FSe.

Ben-Ari et a/. [1982] showed that DPDL-satisfiability is contained in EXPTIME, and Vardi [1985] pointed out that satisfiability in converse-DPDL can be decided in double exponential time . Utilizing Theorem 3 and Lemma 1, we can conclude:

Proposition 8 (Complexity of :FSe)

Subsumption in :F Se without - 1 can be decided in ex­ ponential time [Ben-Ari et al., 1982], and deciding sub­ sumption in :F Se can be done in double exponential time

3 By the way this means that in the presence of · deciding subsumption in feature logics is at least as hard as deciding subsumption in the corresponding terminological logic.

[Vardi, 1 985]. Furthermore, both problems are EX P­ TIME-hard [Parikh, 1979, § 7}.

We now present a sound and complete algorithm for deciding coherence of - 1-free F S.C-concepts in determin­ istic exponential time as described in [Ben-Ari et al., 1982). To test the coherence of a concept C, the algo­ rithm builds a tree with nodes labelled by sets of FS.C­ concepts with root { C}, where double negations occur­ ring in concepts are assumed to be eliminated. The al­ gorithm uses three functions to build the tree, namley 1\-succ, V -succ, and f -succ. 1\-succ and V -succ are non­ deterministic functions to generate necessary and possi­ ble consequences of a set of FS.C-concepts represented by an and-or-tree.

f -succ is a function to generate the /-successors of a node, defined for each feature f by

To compute the coherence of an - 1-free FS.C-concept, the algorithm performs the following steps:

1. Replace each occurrence of a non-feature atomic role r in C by fr o Cfnew )*, where fr is the fea­ ture uniquely corresponding to r and !new is a new feature.
2. Take the tree consisting solely of the root { C} as the current tree.
3. Apply 1\-succ and V-succ to the not yet eliminated leaves until every node thus obtainable already is on the tree.
4. Repeatedly eliminate each leaf r violating either (a) s ~ r for every s = 1\-succ(r), (b) sl ~ r or S2 ~ r for every (S1,S2) = V-succ(f), or (c) C E r iff -.C ¢ r for each C. Call the set of nodes of the current tree N.
5. For each feature /, apply f-succ to all not yet eliminated leaves where two nodes f-succ(f) and f' -succ(f) are to be identified if they are equal. Now define for each feature /, E[f] ~ N x N such that (r, , ft) E E[/) iff f 1 is a node of the tree with root f -succ(r,) generated by 1\-succ and V -succ. For each node r, E N check (in polynomial time) whether for every 3R.D E f. there is aft such that (f,, f 1) E E[R) and D Eft . Eliminate each node not satisfying this condition and all edges leading from and to that node. Continue with 3. until all leaves do satisfy the condition.
6. Return 'yes' if C is an element of a not eliminated node; otherwise return 'no.'

To test 3f* .c, for instance, the algorithm first gener­ ates the root fo = {3f*.c} and its V-successors f1 = {3/* .c,c} and f2 = {3f*.c,3f.3f*.c} . Then the/­ successor of f 2, f 3 = {3/*.c}, is generated. E[f] is de­ fined as {(r2, fo), (r2, r1), (r2, r2)} because r1 as well as f2 are V-successors of /-succ(f2). Now for each 3R.C E f 2 there is a node r such that (f2, f) E t:[R) and C E f. Therefore no leaf has to be eliminated. The algorithm halts returning 'yes' because each V-successor of f3 is already on the tree and 3/* .c E fo.

Surprisingly, allowing the intersection of roles does not preserve the decidability of FS.C.

Proposition 9 (Undecidability of FS.CR)

Subsumption in FS.C augmented with role intersection is highly undecidable, even if involving only features as atomic roles [Hare/, 1984, Theorem 2.36].

With Theorem 3 we gain new model theoretic insights into FS.C . For the ability to force an FS.C-model to be infinite, both features and -l are essential. To see this, first realize that each model t: for

has an infinite acyclic £[/)-chain if f is a feature. Re­ quiring f to be a feature is necessary to preclude cyclic models such as t: over V = { d, e} with E[c) = { e} and E[f] = { (d, e), (d, d)}, where E[f] is not functional.

Proposition 10 (Infinite FS.C-Models)

There is a coherent FS.C-concept which has no finite model [Vardi, 1985].

In contrast to this result, the finite model property holds for - 1-free FS.C.

Proposition 11 (Finite Models for - 1-free FS.C) Every coherent - 1 -free FS.C-concept C has a connected model overV with lVI:::; 4nn 2 , where n =/(C) [Ben-Ari et al., 1982].

4.2 Concept Equations and Inequations

The terminological logics investigated seem to be very expressive. Nevertheless, they do not support concept definitions and constraints. We could want to define, for instance, human beings by

Of course, we want to know the consequences of such definitions and constraints. Like in dynamic logic we say, for example, that human [;;;; 'v'parent· .human is a global consequence of the set r = {(1)} and write:

Formally, we pin this down as follows: Let r U { E} be a set of concept equations and inequations. E is a global consequence of r, written r I= E, iff each exten­ sion function t: satisfying all elements of r' also satisfies E; where [ satisfies C = D iff E[C) = t:[D], and [ sat­ isfies C # D iff t:[C) # t:[D].

We treat C [;;;; D as an abbreviation for C n D = C, and each element of r of this form is called universal implication.

Now there is the question whether the ability to de­ fine and constrain sets actually increases the expres­ sive power ofT SC. It will turn out that for finite r, global consequence in T SC is reducible to subsumption in T SC. To show this, we need two lemmata. The first signifies that only connected models are relevant for global consequence in T SC. This can easily be proved by utilizing the so-called collapsed model property of T SC stating that every T S£-model can be collapsed into a finite connected one [Harel, 1984, Theorem 2.13].

Lemma 2 Let r U { E} be a set ofT SC-concept equa­ tions and inequations. Then r f= E iff each connected extenSiOn function & Satisfying all elementS of r 1 alSO satisfies E.

The following lemma states that universally quanti­ fied expressions are expressible in connected models­ viz . by c(C) defined as V(r1 U r1 1 ... U rm U r;;,1)*.C, where r 1 , ... , rm are the atomic roles and features of the language in question. Note that c owes its name to the common knowledge operator ( cf. [Halpern and Moses, 1985]).

Lemma 3 Let C be any T SC-concept and & any con­ nected extension function over 'D. &[C] = 1) iff &[c(C)] = 'D, and moreover&[c(C)] -:f 1) iff &[c(C)] = 0.

Theorem 4 For finite sets of concept equations and in­ equations, global consequence in T SC is log space re­ ducible to subsumption in T SC.

Proof: Let eq(C,D) be c(-.CUD)nc(-.DUC). Accord­ ing to the last two lemmata, it is obvious that { cl = Dl} u r F c!; D iff r F eq(Cl, Dl) n c!; D and that {C1 -:f Dl} ur F= c!; D iff r F= -.eq(C1,D!) nc!; D. Taking this as induction step, it can be easily shown by induction on If! that all elements of r can be eliminated linearly. 0

However, the proof does not work for infinite r since T SC lacks compactness. This becomes obvious when considering the infinite set r = { c !; \lr.d, c !; \lr 0 r.d, ... }. Clearly, c !; \fr+ .d is a global consequence of r but not a global consequence of any finite subset of r. In fact, global consequence in T SC is known to be highly undecidable [Hare!, 1984, Section 2.4]. However, Theorem 4 also holds for :FSC since Vardi [1985] proved the collapsed model property for :FSC.

5 Conclusions

So far we have seen that correspondences between ter­ minological logics and propositional modal and dynamic logics can be used to gain new insights into the nature of terminological logics. However, this work can be ex­ tended in two ways. First, we can further exploit the correspondences already established by carefully study­ ing the corresponding theories of modal and dynamic logic. For example, we proved that a syntactically re­ stricted form of global consequence in T SC, known in dynamic logic as partial completeness assertions, is NP­ complete. Secondly, we can establish further correspon­ dences. Constants in terminological logics, for instance, correspond to names (atomic formulae denoting single element sets) in dynamic logic. Similarly, temporal ex­ pressions can be integrated into terminological logics.