1: \documentclass[11pt]{article}
2: %\usepackage{proceedings}
3:
4: \usepackage{xspace}
5: \usepackage{theorem}
6: \usepackage{amsmath,amsfonts,amssymb}
7: \usepackage{pstricks,pst-node}
8: \usepackage{verbatim}
9: \usepackage{graphicx}
10:
11:
12:
13:
14:
15: \newcommand{\Calig}[1]{% calligraphic text
16: \ensuremath{\mathcal{#1}}}
17:
18: \newcommand{\DL}{DL\xspace}
19: \newcommand{\KB}{KB\xspace}
20: \newcommand{\DB}{DB\xspace}
21:
22: \newcommand{\ALC}{\Calig{ALC}\xspace}
23: \newcommand{\Galen}{\textsc{Galen}\xspace}
24: \newcommand{\Fact}{FaCT\xspace}
25: \newcommand{\Dlp}{DLP\xspace}
26: \newcommand{\Kris}{\textsc{Kris}\xspace}
27:
28: \newcommand{\I}{\Calig{I}\xspace}
29: \newcommand{\Ifunc}{^\I}
30: \newcommand{\Domain}{\ensuremath{\Delta\Ifunc}\xspace}
31: \newcommand{\Doti}{\ensuremath{\cdot\Ifunc}\xspace}
32: \newcommand{\Tau}{\Calig{T}\xspace}
33: \newcommand{\Rplus}{\ensuremath{\mathbf{R}_+}\xspace}
34:
35: \newcommand{\Not}{\ensuremath{\neg}}
36: \newcommand{\Some}[2]{%
37: \ensuremath{\exists #1.#2}}
38: \newcommand{\All}[2]{%
39: \ensuremath{\forall #1.#2}}
40: \newcommand{\Atmost}[2]{%
41: \ensuremath{\mathopen{\leqslant} #1 #2}}
42: \newcommand{\Atleast}[2]{%
43: \ensuremath{\mathopen{\geqslant} #1 #2}}
44: \newcommand{\AtmostQ}[3]{%
45: \ensuremath{\mathopen{\leqslant} #1 #2.#3}}
46: \newcommand{\AtleastQ}[3]{%
47: \ensuremath{\mathopen{\geqslant} #1 #2.#3}}
48:
49: \newcommand{\Cname}[1]{\mbox{\small \textsf{#1}}}
50: \newcommand{\Rname}[1]{\mbox{\small \textsf{\textsl{#1}}}}
51:
52: \newcommand{\Norm}{\ensuremath{\mathop{\mathsf{Norm}}}}
53: \newcommand{\Simp}{\ensuremath{\mathop{\mathsf{Simp}}}}
54: \newcommand{\Unfold}{\ensuremath{\mathop{\mathsf{Unfold}}}}
55: \newcommand{\Lab}{\Calig{L}}
56: \newcommand{\Conj}{\ensuremath{\mathopen{\sqcap}}}
57: \newcommand{\Edge}[2]{%
58: \ensuremath{\langle #1,#2 \rangle}}
59: \newcommand{\Tree}{%
60: \ensuremath{\mathbf{T}}\xspace}
61:
62: \newcommand{\Implies}{\ensuremath{\Rightarrow}}
63: \newcommand{\Iff}{\ensuremath{\mathbin{\mathsf{iff}}}}
64: \newcommand{\Bd}{\ensuremath{b}}
65:
66: \newcommand{\Key}[1]{\texttt{#1}}
67:
68: \newcommand{\Exptime}{\textsc{Exptime}\xspace}
69: \newcommand{\Pspace}{\textsc{Pspace}\xspace}
70: \newcommand{\ptime}{\textsc{PTime}\xspace}
71: \newcommand{\logspace}{\textsc{LogSpace}\xspace}
72: \newcommand{\SIN}{\Calig{SIN}\xspace}
73:
74: \newfont{\bigmathxx}{cmsy10 scaled 2000}
75: \newcommand{\bigsqcap}{\mathop{\mathop{\mbox{\bigmathxx\symbol{117}}}}\limits}
76:
77:
78: \theoremstyle{plain}
79: \theoremheaderfont{\bf\boldmath}
80: \newtheorem{satz}{Satz}[section]
81: \newtheorem{theorem}[satz]{Theorem}
82: \newtheorem{definition}[satz]{Definition}
83: \theoremstyle{plain}
84: \newtheorem{lemma}[satz]{Lemma}
85: \newtheorem{korollar}[satz]{Korollar}
86: \newtheorem{corollary}[satz]{Corollary}
87: \newtheorem{claim}[satz]{Claim}
88: \newtheorem{fact}[satz]{Fact}
89:
90:
91: \newcommand{\cL}{\Calig{L}\xspace}
92: \newcommand{\cW}{\Calig{W}\xspace}
93: \newcommand{\sL}{\ensuremath{\mathsf{L}}\xspace}
94:
95: \newcommand{\cT}{\Calig{T}\xspace}
96: \newcommand{\cC}{\Calig{C}\xspace}
97: \newcommand{\Int}{\ensuremath{\mathsf{Int}}}
98: \newcommand{\NC}{\ensuremath{\mathsf{NC}}\xspace}
99: \newcommand{\NR}{\ensuremath{\mathsf{NR}}\xspace}
100:
101: \newenvironment{proof}{\noindent \textit{Proof.}}{}
102:
103: \newenvironment{stephan}{ \noindent \hspace{-1cm} \textsc{Stephan:} \itshape }{}
104: \newenvironment{ian}{\noindent \hspace{-1cm} \textsc{Ian:} \itshape }{}
105:
106: \newenvironment{techrep}{\noindent \hspace{-1cm} \textsc{Begin TechRep} \sffamily
107: }{ \newline \hspace{-1cm} \textsc{End TechRep} }
108: \newenvironment{extabst}{\noindent \hspace{-1cm} \textsc{ExtAbst:} \sffamily }{}
109:
110:
111:
112: \newcommand{\qed}{\hfill \vrule height4pt width 4pt depth0pt}
113:
114: \newcommand{\witn}[1]{(\textsf W#1)}
115: \newcommand{\adms}[1]{(\textsf A#1)}
116: \newcommand{\simpl}[1]{(\textsf S#1)}
117: \newcommand{\interp}[1]{(\textsf I#1)}
118: \newcommand{\funn}[1]{(\textsf F#1)}
119: \newcommand{\mono}[1]{(\textsf M#1)}
120: \newcommand{\wrt}{w.r.t.\ }
121:
122: \newcommand{\J}{\Calig{J}\xspace}
123:
124:
125: \newcommand{\LabW}{\ensuremath{\Lab^\cW}\xspace}
126: \newcommand{\Tu}{\ensuremath{\mathcal{T}_u}\xspace}
127: \newcommand{\Tg}{\ensuremath{\mathcal{T}_g}\xspace}
128:
129: \title{Reasoning with Axioms: Theory and Practice\thanks{This paper appeared
130: in the Proceedings of the Seventh International Conference on Priciples of
131: Knowledge Representation and Reasoning (KR'2000).}}
132: \author{
133: {\bf Ian Horrocks}\\
134: Department of Computer Science\\
135: University of Manchester, UK\\
136: {\tt horrocks@cs.man.ac.uk} \and
137: {\bf Stephan Tobies}\\
138: LuFg Theoretical Computer Science\\
139: RWTH Aachen, Germany \\
140: {\tt tobies@informatik.rwth-aachen.de}}
141: \date{}
142:
143:
144:
145:
146: \begin{document}
147:
148: \maketitle
149:
150: \begin{abstract}
151: When reasoning in description, modal or temporal logics it is often useful
152: to consider axioms representing universal truths in the domain of discourse.
153: Reasoning with respect to an arbitrary set of axioms is hard, even for
154: relatively inexpressive logics, and it is essential to deal with such axioms
155: in an efficient manner if implemented systems are to be effective in real
156: applications. This is particularly relevant to Description Logics, where
157: subsumption reasoning with respect to a terminology is a fundamental
158: problem. Two optimisation techniques that have proved to be particularly
159: effective in dealing with terminologies are lazy unfolding and absorption.
160: In this paper we seek to improve our theoretical understanding of these
161: important techniques. We define a formal framework that allows the
162: techniques to be precisely described, establish conditions under which they
163: can be safely applied, and prove that, provided these conditions are
164: respected, subsumption testing algorithms will still function correctly.
165: These results are used to show that the procedures used in the \Fact system
166: are correct and, moreover, to show how efficiency can be significantly
167: improved, while still retaining the guarantee of correctness, by relaxing
168: the safety conditions for absorption.
169:
170:
171: \end{abstract}
172:
173:
174:
175:
176: \section{MOTIVATION}\label{sec:motivat}
177:
178: Description Logics (DLs) form a family of formalisms which have grown
179: out of knowledge representation techniques using frames and semantic
180: networks. DLs use a class based paradigm, describing the domain of
181: interest in terms of concepts (classes) and roles (binary relations)
182: which can be combined using a range of operators to form more complex
183: structured concepts~\cite{Baader91b}. A DL \emph{terminology}
184: typically consists of a set of asserted facts, in particular asserted
185: subsumption (is-a-kind-of) relationships between (possibly complex) concepts.\footnote{DLs can
186: also deal with assertions about individuals, but in this paper we
187: will only be concerned with \emph{terminological} (concept based)
188: reasoning}.
189:
190: One of the distinguishing characteristics of DLs is a formally defined
191: semantics which allows the structured objects they describe to be
192: reasoned with. Of particular interest is the computation of implied
193: subsumption relationships between concepts, based on the assertions in
194: the terminology, and the maintenance of a concept hierarchy (partial
195: ordering) based on the subsumption relationship~\cite{Woods92}.
196:
197: The problem of computing concept subsumption relationships has been
198: the subject of much research, and sound and complete algorithms are
199: now known for a wide range of DLs (for
200: example~\cite{Hollunder90b,Baader91e,Baader91c,DeGiacomo98a,Horrocks99j}).
201: However, in spite of the fundamental importance of terminologies in
202: DLs, most of these algorithms deal only with the problem of deciding
203: subsumption between two concepts (or, equivalently, concept
204: satisfiability), without reference to a terminology (but
205: see~\cite{Buchheit93,Calvanese96a,Donini96a,Horrocks99j}).
206: By restricting the kinds of assertion that can appear in a terminology,
207: concepts can be syntactically expanded so as to explicitly include all
208: relevant terminological information. This procedure, called \emph{unfolding},
209: has mostly been applied to less expressive DLs.
210: With more expressive DLs, in particular those
211: supporting universal roles, it is often possible to encapsulate an
212: arbitrary terminology in a single concept. This technique can be used
213: with satisfiability testing to ensure that the result is valid with
214: respect to the assertions in the terminology, a procedure called
215: \emph{internalisation}.
216:
217: Although the above mentioned techniques suffice to demonstrate the
218: theoretical adequacy of satisfiability decision procedures for
219: terminological reasoning, experiments with implementations have shown
220: that, for reasons of (lack of) efficiency, they are highly
221: unsatisfactory as a practical methodology for reasoning with DL
222: terminologies. Firstly, experiments with the \Kris system have shown
223: that integrating unfolding with the (tableaux) satisfiability algorithm
224: (\emph{lazy unfolding}) leads to a significant improvement in
225: performance~\cite{BFHNP94}. More recently, experiments with the
226: \Fact system have shown that reasoning becomes hopelessly intractable
227: when internalisation is used to deal with larger
228: terminologies~\cite{Horrocks98c}. However, the \Fact system has also
229: demonstrated that this problem can be dealt with (at least for
230: realistic terminologies) by using a combination of lazy unfolding and
231: internalisation, having first manipulated the terminology in order to
232: minimise the number of assertions that must be dealt with by
233: internalisation (a technique called \emph{absorption}).
234:
235: It should be noted that, although these techniques were discovered
236: while developing DL systems, they are applicable to a whole range of
237: reasoning systems, independent of the concrete logic and type of algorithm.
238: As well as tableaux based decision procedures, this includes
239: resolution based algorithms, where the importance of minimising the
240: number of terminological sentences has already been
241: noted~\cite{Hustadt99a}, and sequent calculus algorithms, where there
242: is a direct correspondence with tableaux algorithms~\cite{Horrocks99i}.
243:
244:
245: In this paper we seek to improve our theoretical understanding of
246: these important techniques which has, until now, been very limited.
247: In particular we would like to know exactly when and how they can be
248: applied, and be sure that the answers we get from the algorithm are
249: still correct. This is achieved by defining a formal framework that
250: allows the techniques to be precisely described, establishing
251: conditions under which they can be safely applied, and proving that,
252: provided these conditions are respected, satisfiability algorithms
253: will still function correctly.
254: %
255: %
256: These results are then used to show that the procedures used in the
257: \Fact system are correct\footnote{Previously, the correctness of these
258: procedures had only been demonstrated by a relatively ad-hoc
259: argument~\cite{Horrocks97b}.} and, moreover, to show how efficiency can
260: be significantly improved, while still retaining the guarantee of
261: correctness, by relaxing the safety conditions for absorption.
262: Finally, we identify several interesting directions for future
263: research, in particular the problem of finding the ``best'' absorption
264: possible.
265:
266:
267:
268:
269:
270:
271:
272:
273:
274: \section{PRELIMINARIES}
275:
276: Firstly, we will establish some basic definitions that clarify what we mean by
277: a \DL, a terminology (subsequently called a TBox), and subsumption and
278: satisfiability with respect to a terminology, . The results in this paper are
279: uniformly applicable to a whole range of \DL{}s, as long as some basic
280: criteria are met:
281:
282: \begin{definition}[Description Logic]
283: Let \sL be a \DL based on infinite sets of atomic concepts \NC and atomic
284: roles \NR. We will identify \sL with the sets of its well-formed concepts
285: and require \sL to be closed under boolean operations and sub-concepts.
286:
287: An interpretation is a pair $\I = (\Domain, \Doti)$, where \Domain is a
288: non-empty set, called the \emph{domain} of $\I$, and \Doti is a function mapping \NC
289: to $2^{\Domain}$ and \NR to $2^{\Domain \times \Domain}$. With each DL \sL
290: we associate a set $\Int(\sL)$ of \emph{admissible} interpretations for \sL.
291: $\Int(\sL)$ must be closed under isomorphisms, and, for any two
292: interpretations $\I$ and $\I'$ that agree on \NR, it must satisfy $\I \in
293: \Int(\sL) \Leftrightarrow \I' \in \Int(\sL)$. Additionally, we assume that
294: each \DL \sL comes with a semantics that allows any interpretation $\I \in
295: \Int(\sL)$ to be extended to each concept $C \in \sL$ such that it satisfies
296: the following conditions:
297: \begin{itemize}
298: \item[\interp 1] it maps the boolean combination of concepts to the
299: corresponding boolean combination of their interpretations, and
300: \item [\interp 2] the interpretation $C^\I$of a compound concept $C \in \sL$
301: depends only on the interpretation of those atomic concepts and roles that
302: appear syntactically in $C$.
303: \end{itemize}
304: \end{definition}
305:
306: This definition captures a whole range of \DL{}s, namely, the important DL
307: \ALC~\cite{SSSm91} and its many extensions. $\Int(\sL)$ hides restrictions on
308: the interpretation of certain roles like transitivity, functionality, or role
309: hierarchies, which are imposed by more expressive \DL{}s (e.g.,
310: \cite{Horrocks99j}), as these are irrelevant for our purposes. In these cases,
311: $\Int(\sL)$ will only contain those interpretations which interpret the roles
312: as required by the semantics of the logic, e.g., features by partial functions
313: or transitively closed roles by transitive relations. Please note that various modal
314: logics \cite{Schi91}, propositional dynamic logics \cite{DeLe94} and temporal
315: logics~\cite{Emerson85} also fit into this framework. We will use $C
316: \rightarrow D$ as an abbreviation for $\neg C \sqcup D$, $C \leftrightarrow D$
317: as an abbreviation for $(C \rightarrow D) \sqcap (D \rightarrow C)$, and
318: $\top$ as a tautological concept, e.g., $A \sqcup \neg A$ for an arbitrary $A
319: \in \NC$.
320:
321: A TBox consists of a set of axioms asserting
322: subsumption or equality relations between (possibly complex) concepts.
323:
324: \begin{definition}[TBox, Satisfiability]
325: A \emph{TBox} \cT for \sL is a finite set of axioms of the form $C_1
326: \sqsubseteq C_2$ or $C_1 \doteq C_2$, where $C_i \in \sL$. If, for some $A
327: \in \NC$, \Tau contains one or more axioms of the form $A \sqsubseteq C$ or
328: $A \doteq C$, then we say that $A$ is \emph{defined} in \Tau.
329:
330:
331: Let $\sL$ be a DL and \cT a TBox. An interpretation $\I \in
332: \Int(\sL)$ is a \emph{model} of \cT iff, for each $C_1 \sqsubseteq C_2 \in
333: \cT$, $C_1\Ifunc \subseteq C_2\Ifunc$ holds, and, for each $C_1 \doteq C_2
334: \in \cT$, $C_1\Ifunc = C_2\Ifunc$ holds. In this case we write $\I \models
335: \cT$. A concept $C \in \sL$ is \emph{satisfiable} with respect to a TBox
336: \cT iff there is an $\I \in \Int(\sL)$ with $\I \models \cT$ and $C\Ifunc
337: \neq \emptyset$.
338: A concept $C \in \sL$ \emph{subsumes} a
339: concept $D \in \sL$ \wrt \cT iff, for all $\I \in \Int(\sL)$ with $\I
340: \models \cT$, $C\Ifunc \supseteq D\Ifunc$ holds.
341:
342: Two TBoxes $\cT, \cT'$ are called \emph{equivalent} ($\cT \equiv
343: \cT')$, iff, for all $\I \in \Int(\sL)$, $\I \models \cT \Iff \I \models \cT'$.
344: \end{definition}
345:
346: We will only deal with concept satisfiability as concept subsumption can be
347: reduced to it for \DL{}s that are closed under boolean operations: $C$ subsumes
348: $D$ \wrt \cT iff $(D \sqcap \Not C)$ is not satisfiable \wrt \cT.
349:
350: For temporal or modal logics, satisfiability with respect to a set of formulae
351: $\{C_1, \dots, C_k\}$ asserted to be universally true corresponds to
352: satisfiability \wrt the TBox $\{\top \doteq C_1, \dots, \top \doteq C_n \}$.
353:
354: Many decision procedures for \DL{}s base their judgement on the existence of
355: models or pseudo-models for concepts. A central r\^ole in these algorithms is played
356: by a structure that we will call a \emph{witness} in this paper. It generalises the
357: notions of \emph{tableaux} that appear in \DL tableau-algorithms%
358: ~\cite{HoNS90,BaaderBuchheit+-AIJ-1996,Horrocks99j} as well as the
359: \emph{Hintikka-structures} that are used in tableau and automata-based
360: decision procedures for temporal logic \cite{Emerson85} and propositional
361: dynamic logic~\cite{VaWo86}.
362:
363: \begin{definition}[Witness]\label{def:witness}
364: Let \sL be a \DL and $C \in \sL$ a concept. A \emph{witness}
365: $\cW = (\Delta^\cW, \cdot^\cW, \LabW)$ for $C$ consists of a
366: non-empty set $\Delta^\cW$, a function $\cdot^\cW$ that maps \NR to
367: $2^{\Delta^{\cW} \times \Delta^{\cW}}$, and a function \LabW that
368: maps $\Delta^\cW$ to $2^{\sL}$ such that the following properties
369: are satisfied:
370: \begin{itemize}
371: \item[\witn 1] there is some $x \in \Delta^\cW$ with $C \in \LabW(x)$,
372: \item[\witn 2] there is an interpretation $\I \in \Int(\sL)$ that
373: \emph{stems} from \cW, and
374: \item [\witn 3] for each interpretation $\I \in \Int(\sL)$
375: that \emph{stems} from \cW, it holds that $D \in \LabW(x)$ implies
376: $x \in D\Ifunc$.
377: \end{itemize}
378: An interpretation $\I=(\Domain,\Doti)$ is said to stem from \cW if it
379: satisfies:
380: \begin{enumerate}
381: \item $\Domain = \Delta^\cW$,
382: \item $\Doti|_{\NR} = \cdot^\cW$, and
383: \item for each $A \in \NC$, $A \in \LabW(x) \ \Implies \ x \in
384: A\Ifunc$ and $\neg A \in \LabW(x) \ \Implies \ x \not\in A\Ifunc$.
385: \end{enumerate}
386:
387: A witness \cW is called \emph{admissible} with respect to
388: a TBox \cT if there is an interpretation $\I \in \Int(\sL)$ that stems from
389: \cW with $\I \models \cT$.
390: \end{definition}
391:
392: Please note that, for any witness \cW, \witn 2 together with Condition 3 of
393: ``stemming'' implies that, there exists no $x \in \Delta^\cW$ and $A \in \NC$,
394: such that $\{A, \neg A\} \subseteq \LabW(x)$. Also note that, in general,
395: more than one interpretation may stem from a witness. This is the case if, for
396: an atomic concept $A \in \NC$ and an element $x \in \Delta^\cW$, $\Lab^\cW(x)
397: \cap \{ A, \neg A \} = \emptyset$ holds (because two interpretations
398: $\I$ and $\I'$, with $x \in A^\I$ and $x \in \neg A^{\I'}$, could both
399: stem from \cW).
400:
401: Obviously, each interpretation $\I$ gives rise to a special witness, called
402: the \emph{canonical witness}:
403:
404: \begin{definition}[Canonical Witness]
405: Let \sL be a \DL. For any interpretation $\I \in \Int(\sL)$ we define the
406: \emph{canonical witness} $\cW_\I = (\Delta^{\cW_\I}, \cdot^{\cW_\I},
407: \Lab^{\cW_\I})$ as follows:
408: \begin{align*}
409: \Delta^{\cW_\I} & = \Domain \\
410: \cdot^{\cW_\I} & = \Doti|_{\NR} \\
411: \Lab^{\cW_\I} & = \lambda x.\{ D \in \sL \mid x \in D\Ifunc \}
412: \end{align*}
413: \end{definition}
414:
415: The following elementary properties of a canonical witness will be useful in
416: our considerations.
417:
418: \begin{lemma}\label{lem:canonical-witness}
419: Let \sL be a \DL, $C \in \sL$, and \cT a TBox. For each $\I \in
420: \Int(\sL)$ with $C\Ifunc \neq \emptyset$,
421: \begin{enumerate}
422: \item each interpretation $\I'$ stemming from $\cW_\I$ is isomorphic to \I
423: \item $\cW_\I$ is a witness for $C$,
424: \item $\cW_\I$ is admissible \wrt \cT iff $\I \models \cT$
425: \end{enumerate}
426: \end{lemma}
427:
428: \begin{proof}
429: \begin{enumerate}
430: \item Let $\I'$ stem from $\cW_\I$. This implies $\Delta^{\I'} = \Domain$
431: and $\cdot^{\I'}|_{\NR} = \Doti|_{\NR}$. For each $x \in
432: \Domain$ and $A \in \NC$, $\{A, \neg A\} \cap \Lab^{\cW_\I}(x) \neq
433: \emptyset$, this implies $\cdot^{\I'}|_{\NC} = \Doti|_{\NC}$ and hence \I and
434: $\I'$ are isomorphic.
435: \item Properties \witn 1 and \witn 2 hold by construction. Obviously, \I stems
436: from $\cW_\I$ and from (1) it follows that each interpretation $\I'$
437: stemming from $\cW_\I$ is isomorphic to \I, hence \witn 3 holds.
438: \item Since \I stems from $\cW_\I$, $\I \models \cT$ implies that $\cW_\I$
439: is admissible \wrt \cT. If $\cW_\I$ is admissible \wrt \cT, then there is an
440: interpretation $\I'$ stemming from $\cW_\I$ with $\I' \models \cT$. Since
441: $\I$ is isomorphic to $\I'$, this implies $\I \models \cT$. \qed
442: \end{enumerate}
443: \end{proof}
444:
445:
446: As a corollary we get that the existence of admissible witnesses is closely
447: related to the satisfiability of concepts \wrt TBoxes:
448:
449: \begin{lemma}\label{cor:witness-and-satisfiability}
450: Let \sL be a \DL. A concept $C \in \sL$ is satisfiable \wrt a TBox \cT iff
451: it has a witness that is admissible \wrt \cT.
452: \end{lemma}
453:
454: \begin{proof}
455: For the \emph{only if}-direction let $\I \in \Int(\sL)$ be an interpretation
456: with $\I \models \cT$ and $C\Ifunc \neq \emptyset$. From Lemma~\ref{lem:canonical-witness} it follows that
457: the canonical witness $\cW_\I$ is a witness for $C$ that is admissible
458: \wrt \cT.
459:
460: For the \emph{if}-direction let \cW be an witness for $C$ that
461: is admissible \wrt \cT. This
462: implies that there is an interpretation $\I \in \Int(\sL)$ stemming from \cW
463: with $\I \models \cT$. For each interpretation \I that stems from \cW, it
464: holds that $C\Ifunc \neq \emptyset$ due to \witn 1 and \witn 3. \qed
465: \end{proof}
466:
467:
468:
469:
470:
471:
472: From this it follows that one can test the satisfiability of a concept \wrt to
473: a TBox by checking for the existence of an admissible witness. We call
474: algorithms that utilise this approach \emph{model-building algorithms}.
475:
476:
477:
478:
479: This notion captures tableau-based decision procedures,
480: \cite{HoNS90,BaaderBuchheit+-AIJ-1996,Horrocks99j}, those using
481: automata-theoretic approaches \cite{VaWo86,CaDL99} and, due to their direct
482: correspondence with tableaux algorithms~\cite{Hustadt99a,Horrocks99i}, even
483: resolution based and sequent calculus algorithms.
484:
485: %This work develops a
486:
487: The way many decision procedures for \DL{}s deal with TBoxes exploits the
488: following simple lemma.
489:
490: \begin{lemma}\label{lem:simple-approach}
491: Let \sL be a \DL, $C \in \sL$ a concept, and \cT a TBox. Let \cW be a
492: witness for $C$. If
493: %, for each $x \in \Delta^\cW$,
494: \[
495: \begin{array}{lcl}
496: C_1 \sqsubseteq C_2 \in \cT & \Implies & \forall x \in \Delta^\cW.(
497: C_1 \rightarrow C_2 \in \LabW(x))\\
498: C_1 \doteq C_2 \in \cT \; & \Implies & \forall x \in \Delta^\cW.(C_1 \leftrightarrow C_2 \in \LabW(x))
499: \end{array}
500: \]
501: then \cW is admissible \wrt \cT.
502: \end{lemma}
503:
504: \begin{proof}
505: \cW is a witness, hence there is an interpretation $\I \in \Int(\sL)$
506: stemming from \cW. From \witn 3 and the fact that \cW satisfies the
507: properties stated in \ref{lem:simple-approach} it
508: follows that, for each $x \in \Domain$,
509: \[
510: \begin{array}{lcl}
511: C_1 \sqsubseteq C_2 \in \cT & \Implies & C_1 \rightarrow C_2 \in
512: \LabW(x) \\ & \Implies & x \in (C_1 \rightarrow C_2)\Ifunc\\
513: C_1 \doteq C_2 \in \cT & \Implies & C_1 \leftrightarrow C_2 \in \LabW(x)
514: \\
515: & \Implies & x \in (C_1 \leftrightarrow C_2)\Ifunc
516: \end{array}
517: \]
518: Hence, $\I \models \cT$ and \cW is admissible \wrt \cT. \qed
519: \end{proof}
520:
521: Examples of algorithms that exploit this lemma to deal with axioms can be
522: found in \cite{Donini96a,DeLe96,Horrocks99j}, where, for each axiom $C_1
523: \sqsubseteq C_2$ ($C_1 \doteq C_2$) the concept $C_1 \rightarrow C_2$ ($C_1
524: \leftrightarrow C_2$) is added to every node of the generated tableau.
525:
526: Dealing with general axioms in this manner is costly due to the high degree of
527: nondeterminism introduced. This can best be understood by looking at tableaux
528: algorithms, which try to build witnesses in an incremental fashion. For a
529: concept $C$ to be tested for satisfiability, they start with $\Delta^\cW = \{
530: x_0 \}$, $\LabW(x_0) = \{ C \}$ and $\cdot^\cW(R) = \emptyset$ for each $R \in
531: \NR$. Subsequently, the concepts in $\LabW$ are decomposed and, if necessary,
532: new nodes are added to $\Delta^\cW$, until either \cW is a
533: witness for $C$, or an obvious contradiction of the form $\{A,\neg A\}
534: \subseteq \LabW(x)$, which violates \witn 2, is
535: generated. In the latter case, backtracking search is used to explore
536: alternative non-deterministic decompositions (e.g., of disjunctions),
537: one of which could lead to the discovery of a witness.
538:
539: When applying Lemma~\ref{lem:simple-approach}, disjunctions are added
540: to the label of each node of the tableau for each general axiom in the
541: TBox (one disjunction for axioms of the form $C_1 \sqsubseteq C_2$,
542: two for axioms of the form $C_1 \doteq C_2$). This leads to an
543: exponential increase in the search space as the number of nodes and
544: axioms increases. For example, with 10 nodes and a TBox containing 10
545: general axioms (of the form $C_1 \sqsubseteq C_2$) there are already
546: 100 disjunctions, and they can be non-deterministically decomposed in
547: $2^{100}$ different ways. For a TBox containing large numbers of
548: general axioms (there are 1,214 in the \Galen medical terminology
549: \KB~\cite{Rector93a}), this can degrade performance to the extent that
550: subsumption testing is effectively non-terminating. To reason with
551: this kind of TBox we must find a more efficient way to deal with
552: axioms.
553:
554:
555:
556:
557:
558: \section{ABSORPTIONS}
559:
560: We start our considerations with an analysis of a technique
561: that can be used to deal more efficiently with so-called
562: primitive or acyclic TBoxes.
563:
564:
565:
566: \begin{definition}[Absorption]
567: Let \sL be a \DL and \cT a TBox. An \emph{absorption} of \cT is a pair of
568: TBoxes $(\Tu,\Tg)$ such that $\cT \equiv \Tu \cup \Tg$ and \Tu contains only
569: axioms of the form $A \sqsubseteq D$ and $\neg A \sqsubseteq D$ where $A \in
570: \NC$.% is an atomic concept.
571:
572: An absorption $(\Tu,\Tg)$ of \cT is called \emph{correct} if it satisfies
573: the following condition. For each witness \cW, if, for each $x \in \Delta^\cW$,
574: \[
575: \begin{array}{r@{\;}c@{\;}l}
576: A \sqsubseteq D \in \Tu \wedge A \in \LabW(x) & \Implies& D \in
577: \LabW(x)\\
578: \neg A \sqsubseteq D \in \Tu \wedge \neg A \in \LabW(x) & \Implies & D \in
579: \LabW(x)\\
580: C_1 \sqsubseteq C_2 \in \Tg & \Implies & C_1 \rightarrow C_2 \in
581: \LabW(x)\\
582: C_1 \doteq C_2 \in \Tg & \Implies & C_1 \leftrightarrow C_2 \in \LabW(x)
583: \end{array}
584: \]
585: then \cW is admissible \wrt \cT. We refer to this properties by $(*)$. A
586: witness that satisfies $(*)$ will be called \emph{unfolded \wrt \cT{}}.
587: \end{definition}
588:
589: If the reference to a specific TBox is clear from the context, we will often
590: leave the TBox implicit and say that a witness is unfolded.
591:
592:
593: How does a correct absorption enable an algorithm to deal with axioms more
594: efficiently? This is best described by returning to tableaux
595: algorithms. Instead of dealing with axioms as previously described, which may
596: lead to an exponential increase in the search space, axioms in $\Tu$ can now
597: be dealt with in a deterministic manner. Assume, for example, that we have to handle the axiom
598: $A \doteq C$. If the label of a node already
599: contains $A$ (resp.\ $\neg A$), then $C$ (resp.\ $\neg C$) is added to
600: the label; if the label contains neither $A$ nor $\neg A$, then
601: \emph{nothing} has to be done. Dealing with the
602: axioms in $\Tu$ this way avoids the necessity for additional non-deterministic
603: choices and leads to a gain in efficiency. A witness produced in this manner will be
604: unfolded and is a certificate for satisfiability \wrt \cT. This technique is generally known
605: as \emph{lazy unfolding} of primitive TBoxes~\cite{Horrocks98c}; formally, it is
606: justified by the following lemma:
607:
608: \begin{lemma}
609: Let $(\Tu,\Tg)$ be a correct absorption of \cT. For any $C \in \sL$, $C$ has
610: a witness that is admissible \wrt \cT iff $C$ has an unfolded witness.
611: \end{lemma}
612:
613: \begin{proof}
614: The \emph{if}-direction follows from the definition of ``correct
615: absorption''. For the \emph{only if}-direction, let $C \in \sL$ be a concept
616: and \cW a witness for $C$ that is admissible \wrt \cT. This implies the
617: existence of an interpretation $\I \in \Int(\sL)$ stemming from \cW such
618: that $\I \models \cT$ and $C^\I \neq \emptyset$. Since $\cT \equiv \Tu \cup
619: \Tg$ we have $\I \models \Tu \cup \Tg$ and hence the canonical witness
620: $\cW_\I$ is an unfolded witness for $C$. \qed
621: \end{proof}
622:
623: A family of TBoxes where absorption can successfully be applied are
624: \emph{primitive} TBoxes, the most simple form of TBox usually studied in the
625: literature.
626:
627: \begin{definition}[Primitive TBox]\label{def:primitive-tbox}
628: A TBox \cT is called \emph{primitive} iff it consists entirely of axioms of the form
629: $A \doteq D$ with $A \in \NC$, each $A \in \NC$ appears as at most one
630: left-hand side of an axiom, and \cT is acyclic. Acyclicity is defined as
631: follows: $A \in \NC$ is said to \emph{directly use} $B \in \NC$ if $A \doteq
632: D \in \cT$ and $B$ occurs in $D$; \emph{uses} is the transitive
633: closure of ``directly uses''. We say that \cT is \emph{acyclic} if there is
634: no $A \in \NC$ that uses itself.
635: \end{definition}
636:
637: For primitive TBoxes a correct absorption can easily be given.
638:
639: \begin{theorem}\label{theo:prim-tbox}
640: Let \cT be a primitive TBox, $\Tg = \emptyset$, and \Tu defined by
641: \[
642: \Tu = \{ A \sqsubseteq D, \neg A \sqsubseteq \neg D \mid A \doteq D \in \cT
643: \} .
644: \] %
645: Then $(\Tu,\Tg)$ is a correct absorption of \cT.
646: \end{theorem}
647:
648: \begin{proof}
649: Trivially, $\cT \equiv \Tu \cup \Tg$ holds. Given an unfolded witness $\cW$,
650: % = (\Delta^\cW,\cdot^\cW,\LabW)$
651: we have to show that
652: there is an interpretation \I stemming from \cW with $\I \models \cT$.
653:
654: We fix an arbitrary linearisation $A_1, \dots, A_k$ of the ``uses'' partial
655: order on the atomic concept names appearing on the left-hand sides of axioms
656: in \cT such that, if $A_i$ uses $A_j$, then $j < i$ and the defining concept
657: for $A_i$ is $D_i$.
658:
659: For some interpretation \I, atomic concept $A$, and set $X \subseteq
660: \Delta^\I$, we denote the interpretation that maps $A$ to $X$ and agrees
661: with $\I$ on all other atomic concepts and roles by $\I[A \mapsto X]$. For
662: $0 \leq i \leq k$, we define $\I_i$ in an iterative process starting from an
663: arbitrary interpretation $\I_0$ stemming from \cW and setting
664: \[
665: \I_i := \I_{i-1}[A_i \mapsto \{ x \in \Delta^\cW \mid x \in D_i^{\I_{i-1}}
666: \}]
667: \]
668:
669: Since, for each $A_i$ there is exactly one axiom in \cT, each step in this
670: process is well-defined. Also, since $\Int(\sL)$ may only restrict the
671: interpretation of atomic roles, $\I_i \in \Int(\sL)$ for each $0 \leq i \leq
672: k$. For $\I = \I_k$ it can be shown that \I is an interpretation stemming
673: from \cW with $\I \models \cT$.
674:
675: First we prove inductively that, for $0 \leq i \leq k$, $\I_i$ stems from \cW.
676: We have already required $\I_0$ to stem from \cW.
677:
678: Assume the claim was proved for $\I_{i-1}$ and $\I_i$ does not stem from
679: \cW. Then there must be some $x \in \Delta^\cW$ such that either (i) $A_i
680: \in \LabW(x)$ but $x \not \in A_i^{\I_i}$ or (ii) $\neg A_i \in \LabW(x)$
681: but $x \in A_i^{\I_i}$ (since we assume $\I_{i-1}$ to stem from \cW and
682: $A_i$ is the only atomic concept whose interpretation changes from
683: $\I_{i-1}$ to $\I_i$). The two cases can be handled dually:
684: \begin{itemize}
685: \item[(i)] From $A_i \in \LabW(x)$ it follows that $D_i \in \LabW(x)$,
686: because \cW is unfolded. Since $\I_{i-1}$ stems from \cW and \cW is a
687: witness, Property \witn 3 implies $x \in D_i^{\I_{i-1}}$. But this
688: implies $x \in A_i^{\I_i}$, which is a contradiction.
689: \item[(ii)] From $\neg A_i \in \LabW(x)$ it follows that $\neg D_i \in
690: \LabW(x)$ because \cW is unfolded. Since $\I_{i-1}$ stems from \cW and
691: \cW is an witness, Property \witn 3 implies $x \in (\neg
692: D_i)^{\I_{i-1}}$. Since $(\neg D_i)^{\I_{i-1}} = \Delta^\cW \setminus
693: D_i^{\I_{i-1}}$ this implies $x \not\in A_i^{\I_i}$, which is a
694: contradiction.
695: \end{itemize}
696: Together this implies that $\I_i$ also stems from \cW.
697:
698: To show that $\I \models \cT$ we show inductively that $\I_i \models A_j
699: \doteq D_j$ for each $1 \leq j \leq i$. This is obviously true for $i = 0$.
700:
701: The interpretation of $D_i$ may not depend on the interpretation of
702: $A_i$ because otherwise \interp 2 would imply that $A_i$ uses
703: itself. Hence $D_i^{\I_i} = D_i^{\I_{i-1}}$ and, by
704: construction, $\I_i \models A_i \doteq D_i$. Assume there is
705: some $j < i$ such that $\I_i \not\models A_j \doteq D_j$. Since $\I_{i-1}
706: \models A_j \doteq D_j$ and only the interpretation of $A_i$ has changed
707: from $\I_{i-1}$ to $\I_i$, $D_j^{\I_i} \neq D_j^{\I_{i-1}}$ must hold
708: because of \interp 2. But
709: this implies that $A_i$ occurs in $D_j$ and hence $A_j$ uses $A_i$
710: which contradicts $j < i$. Thus, we have $\I \models A_j = D_j$ for each
711: $1 \leq j \leq k$ and hence $\I \models \cT$. \qed
712: \end{proof}
713:
714:
715: Lazy unfolding is a well-known and widely used technique for optimising
716: reasoning \wrt primitive TBoxes~\cite{BFHNP94}. So far, we have only given a correctness
717: proof for this relatively simple approach, although one that is independent of a specific \DL or
718: reasoning algorithm. With the next lemma we show how we can extend correct
719: absorptions and hence how lazy unfolding can be applied to
720: a broader class of TBoxes. A further enhancement of the technique is presented
721: in Section~\ref{sec:performance}.
722:
723: \begin{lemma}\label{lem:extension-lemma}
724: Let $(\Tu,\Tg)$ be a correct absorption of a TBox
725: \cT.
726: \begin{enumerate}
727: \item If $\cT'$ is an arbitrary TBox, then $(\Tu,\Tg \cup \cT')$ is a
728: correct absorption of $\cT \cup \cT'$.
729: \item If $\cT'$ is a TBox that consists entirely of axioms of the form $A
730: \sqsubseteq D$, where $A \in \NC$ and $A$ is not defined in $\Tu$, then
731: $(\Tu \cup \cT',\Tg)$ is a correct absorption of $\cT \cup \cT'$.
732: \end{enumerate}
733: \end{lemma}
734:
735: \begin{proof} In both cases, $\Tu \cup \Tg \cup \cT' \equiv \cT \cup \cT'$ holds trivially.
736: \begin{enumerate}
737: \item Let $C \in \sL$ be a concept and $\cW$ be an unfolded witness for $C$
738: \wrt the absorption $(\Tu,\Tg \cup \cT')$. This implies that \cW is unfolded
739: \wrt the (smaller) absorption $(\Tu,\Tg)$. Since $(\Tu,\Tg)$ is a correct
740: absorption, there is an interpretation $\I$ stemming from \cW with $\I
741: \models \cT$. Assume $\I \not \models \cT'$. Then, without loss of
742: generality,\footnote{Arbitrary TBoxes can be expressed using only
743: axioms of the form $C \sqsubseteq D$.} there is an axiom $D
744: \sqsubseteq E \in \cT'$ such that there exists an $x \in D^\I \setminus
745: E^\I$. Since \cW is unfolded, we have $D \rightarrow E \in \Lab^\cW(x)$
746: and hence \witn 3 implies $x \in (\neg D \sqcup E)^\I =\Delta^\I \setminus
747: (D^\I \setminus E^\I)$, a contradiction. Hence $\I \models \cT \cup \cT'$
748: and \cW is admissible \wrt $\cT \cup \cT'$.
749: \item Let $C \in \sL$ be a concept and $\cW$ be an unfolded witness for $C$
750: w.r.t.\ the absorption $(\Tu \cup \cT',\Tg)$. From $\cW$ we define a new witness
751: $\cW'$ for $C$ by setting $\Delta^{\cW'} := \Delta^\cW$, $\cdot^{\cW'}
752: := \cdot^\cW$, and definig $\Lab^{\cW'}$ to be the function that, for
753: every $x \in \Delta^{\cW'}$, maps $x$ to the set
754: \[
755: \Lab^\cW(x) \cup \{ \neg A \mid A \sqsubseteq
756: D \in \cT', A \not \in \Lab^\cW(x) \}
757: \]
758:
759: It is easy to see that $\cW'$ is indeed a witness for $C$ and that $\cW'$
760: is also unfolded w.r.t.\ the absorption $(\Tu \cup \cT',\Tg)$. This
761: implies that $\cW'$ is also unfolded w.r.t.\ the (smaller) absorption
762: $(\Tu,\Tg)$. Since $(\Tu,\Tg)$ is a correct absorption of $\cT$, there
763: exists an interpretation \I stemming from $\cW'$ such that $\I \models
764: \cT$. We will show that $\I \models \cT'$ also holds. Assume $\I \not
765: \models \cT'$, then there is an axiom $A \sqsubseteq D \in \cT'$ and an $x
766: \in \Delta^\I$ such that $x \in A^\I$ but $x \not \in D^\I$. By
767: construction of $\cW'$, $x \in A^\I$ implies $A \in \Lab^{\cW'}(x)$
768: because otherwise $\neg A \in \Lab^{\cW'}(x)$ would hold in contradiction
769: to \witn 3. Then, since $\cW'$ is unfolded, $D \in \Lab^{\cW'}(x)$, which,
770: again by \witn 3, implies $x \in D^\I$, a contradiction.
771:
772: Hence, we have shown that there exists an interpretation $\I$ stemming
773: from $\cW'$ such that $\I \models \Tu \cup \cT' \cup \Tg$. By construction
774: of $\cW'$, any interpretation stemming from $\cW'$ also stems from $\cW$,
775: hence $\cW$ is admissible \wrt $\cT \cup \cT'$. \qed
776: \end{enumerate}
777: \end{proof}
778:
779:
780:
781:
782:
783:
784:
785:
786:
787:
788:
789:
790:
791:
792:
793:
794:
795:
796:
797:
798:
799:
800: \section{APPLICATION TO \Fact}
801: \label{sec:application}
802:
803: \newcommand{\Tprim}{\ensuremath{\cT_{\text{prim}}}\xspace}
804: \newcommand{\Trest}{\ensuremath{\cT_{\text{inc}}}\xspace}
805:
806:
807: In the preceeding section we have defined correct absorptions and discussed
808: how they can be exploited in order to optimise satisfiability procedures. However, we have said
809: nothing about the problem of how to find an absorption given an arbitrary
810: terminology. In this section we will describe the absorption algorithm used by
811: \Fact and prove that it generates correct absorptions.
812:
813: Given a TBox $\cT$ containing arbitrary axioms, the absorption algorithm used
814: by \Fact constructs a triple of TBoxes $(\Tg,\Tprim,\Trest)$ such that
815: \begin{itemize}
816: \item $\cT \equiv \Tg \cup \Tprim \cup \Trest$,
817: \item $\Tprim$ is primitive, and
818: \item $\Trest$ consists only of axioms of the form $A \sqsubseteq D$ where $A
819: \in \NC$ and $A$ is not defined in $\Tprim$.
820: \end{itemize}
821: We refer to these properties by $(*)$. From Theorem~\ref{theo:prim-tbox}
822: together with Lemma~\ref{lem:extension-lemma} it follows that,
823: for
824: \[
825: \Tu := \{ A \sqsubseteq D, \neg A \sqsubseteq \neg D \mid A \doteq D \in
826: \Tprim \} \cup \Trest
827: \]
828: (\Tu,\Tg) is a correct absorption of $\cT$; hence satisfiability for a
829: concept $C$ \wrt \cT can be decided by checking for an unfolded witness for $C$.
830:
831:
832:
833:
834: In a first step, \Fact distributes axioms from \Tau amongst $\Trest$,
835: $\Tprim$, and $\Tg$, trying to minimise the number of axioms in $\Tg$
836: while still maintaining $(*)$. To do this, it initialises $\Tprim,
837: \Trest$, and $\Tg$ with $\emptyset$, and then processes each axiom $X
838: \in \Tau$ as follows.
839: %
840: \begin{enumerate}
841: \item If $X$ is of the form $A \sqsubseteq C$, then
842: \begin{enumerate}
843: \item if $A \in \NC$ and $A$ is not defined in $\Tprim$ then $X$
844: is added to $\Trest$,
845: \item otherwise $X$ is added to $\Tg$
846: \end{enumerate}
847: \item If $X$ is of the form $A \doteq C$, then
848: \begin{enumerate}
849: \item if $A \in \NC$, $A$ is not defined in
850: $\Tprim$ or $\Trest$ and $\Tprim \cup \{X\}$ is primitive, then $X$ is added
851: to $\Tprim$,
852: \item otherwise, the axioms $A \sqsubseteq C$ and $C \sqsubseteq A$
853: are added to $\Tg$.
854: \end{enumerate}
855: \item If $X$ is of the form $C \sqsubseteq D$, then add $X$ to $\Tg$
856: \item If $X$ is of the form $C \doteq D$, then add $C \sqsubseteq D, D
857: \sqsubseteq C$ to $\Tg$.
858: \end{enumerate}
859:
860: It is easy to see that the resulting TBoxes $\Tg, \Tprim, \Trest$ satisfy
861: $(*)$. In a second step, \Fact processes the axioms in $\Tg$ one at a
862: time, trying to absorb them into axioms in $\Trest$. Those axioms
863: that are not absorbed remain in $\Tg$.
864: To
865: give a simpler formulation of the algorithm, each axiom $(C \sqsubseteq D) \in
866: \Tg$ is viewed as a clause $\mathbf{G}=\{D, \Not C\}$, corresponding to
867: the axiom $\top \sqsubseteq C \rightarrow D$, which is equivalent to $C
868: \sqsubseteq D$. For each such axiom \Fact applies the following absorption procedure.
869: %
870: \begin{enumerate}
871: \item \label{09-item:abs2} Try to absorb $\mathbf{G}$. If there is a concept
872: $\neg A \in \mathbf{G}$ such that $A \in \NC$ and $A$ is not defined in
873: $\Tprim$, then add $A \sqsubseteq B$ to $\Trest$, where $B$ is the
874: disjunction of all the concepts in $\mathbf{G} \setminus \{\neg A\}$, remove
875: $\mathbf{G}$ from $\Tg$, and exit.
876: \item Try to simplify $\mathbf{G}$.
877: \begin{enumerate}
878: \item If there is some $\Not C \in \mathbf{G}$ such that $C$ is of
879: the form $C_1 \sqcap \ldots
880: \sqcap C_n$, then substitute $\Not C$ with $\Not C_1 \sqcup \ldots
881: \sqcup \Not C_n$, and %return to step~\ref{09-item:abs2}.
882: continue with step~\ref{09-item:abs2b}.
883: \item \label{09-item:abs2b} If there is some $C \in \mathbf{G}$ such that $C$ is of the
884: form $(C_1 \sqcup \ldots \sqcup C_n)$, then apply associativity by
885: setting $\mathbf{G} = \mathbf{G} \cup \{C_1, \ldots, C_n\}
886: \setminus \{(C_1 \sqcup \ldots \sqcup C_n)\}$, and return to
887: step~\ref{09-item:abs2}.
888: \end{enumerate}
889: \item Try to unfold $\mathbf{G}$. If, for some $A \in \mathbf{G}$
890: (resp.\ $\neg A \in \mathbf{G}$), there is an axiom $A \doteq C$ in
891: $\Tprim$, then substitute $A \in \mathbf{G}$ (resp.\ $\neg A \in
892: \mathbf{G}$) with $C$ (resp.\ $\neg C$) and return to
893: step~\ref{09-item:abs2}.
894: \item If none of the above were possible, then absorption of $\mathbf{G}$
895: has failed. Leave $\mathbf{G}$ in $\Tg$, and exit.
896: \end{enumerate}
897: %
898:
899:
900: For each step, we have to show that $(*)$ is maintained. Dealing with clauses
901: instead of axioms causes no problems. In the first step, axioms are moved
902: from $\Tg$ to $\Trest$ as long as this does not violate $(*)$.
903: The second and the third step replace a clause by an equivalent one and hence
904: do not violate $(*)$.
905:
906: Termination of the procedure is obvious. Each axiom is considered only
907: once and, for a given axiom, simplification and unfolding can only be
908: applied finitely often before the procedure is exited, either by
909: absorbing the axiom into $\Trest$ or leaving it in $\Tg$. For
910: simplification, this is obvious; for unfolding, this holds because
911: $\Tprim$ is acyclic. Hence, we get the following:
912:
913:
914: \begin{theorem}
915: For any TBox \Tau, \Fact computes a correct absorption of \Tau.
916: \end{theorem}
917:
918:
919:
920: \section{IMPROVING PERFORMANCE}
921: \label{sec:performance}
922:
923: \newcommand{\dotcup}{\mathbin{\dot \cup}}
924: \newcommand{\shiq}{\ensuremath{\mathcal{SHIQ}}\xspace}
925:
926: The absorption algorithm employed by \Fact already leads to a dramatic
927: improvement in performance. This is illustrated by
928: Figure~\ref{fig:graph1}, which shows the times taken by \Fact to
929: classify versions of the \Galen KB with some or all of the general
930: axioms removed. Without absorption, classification time increased
931: rapidly with the number of general axioms, and exceeded 10,000s with
932: only 25 general axioms in the KB; with absorption, only 160s was taken
933: to classify the KB with all 1,214 general axioms.
934:
935: \begin{figure*}[htb]
936: \begin{center}
937: \includegraphics[width=0.75\linewidth]{results2.eps}
938: \end{center}
939: \caption{Classification times with and without absorption}
940: \label{fig:graph1}
941: \end{figure*}
942:
943: However, there is still considerable scope
944: for further gains. In particular, the following definition for a
945: \emph{stratified} TBox allows lazy unfolding to be more generally
946: applied, while still allowing for correct absorptions.
947:
948:
949:
950:
951:
952: \begin{definition}[Stratified TBox]\label{def:monotone-tbox}
953: A TBox \cT is called \emph{stratified} iff it consists entirely of axioms of the form
954: $A \doteq D$ with $A \in \NC$, each $A \in \NC$ appears at most once
955: on the left-hand side of an axiom, and \cT can be arranged
956: monotonously, i.e., there is a
957: disjoint partition $\cT_1 \dotcup \cT_2 \dotcup \dots \dotcup \cT_k$ of $\cT$, such that
958: \begin{itemize}
959: \item for all $1 \leq j < i \leq k$, if $A \in \NC$ is defined in $\cT_i$,
960: then it does not occur in $\cT_j$, and
961: \item for all $1\leq i \leq k$, all concepts which appear on the right-hand
962: side of axioms in $\cT_i$ are monotone in all atomic concepts defined in
963: $\cT_i$.
964: \end{itemize}
965: A concept $C$ is monotone in an atomic concept $A$ if, for any
966: interpretation $\I \in \Int(\sL)$ and any two sets $X_1,X_2 \subseteq
967: \Delta^\I$,
968: \[
969: X_1 \subseteq X_2 \ \Implies \ C^{\I[A \mapsto X_1]} \subseteq
970: C^{\I[A \mapsto X_2]} .
971: \]
972: \end{definition}
973:
974: For many DLs, a sufficient condition for monotonicity is \emph{syntactic}
975: monotonicity, i.e., a concept $C$ is syntactically monotone in some atomic
976: concept $A$ if $A$ does no appear in $C$ in the scope of an odd number of
977: negations.
978:
979: Obviously, due to its acyclicity, every primitive TBox is also stratified and
980: hence the following theorem is a strict generalisation of
981: Theorem~\ref{theo:prim-tbox}.
982:
983: \begin{theorem}\label{theo:monotone-tbox}
984: Let \cT be a stratified TBox, $\Tg = \emptyset$ and \Tu defined by
985: \[
986: \Tu = \{ A \sqsubseteq D, \neg A \sqsubseteq \neg D \mid A \doteq D \in \cT
987: \} .
988: \]
989: Then $(\Tu,\Tg)$ is a correct absorption of \cT.
990: \end{theorem}
991:
992: The proof of this theorem follows the same line as the proof of
993: Theorem~\ref{theo:prim-tbox}. Starting from an arbitrary interpretation $\I_0$
994: stemming from the unfolded witness, we incrementally construct interpretations
995: $\I_1, \dots, \I_k$, using a fixed point construction in each step. We show
996: that each $\I_i$ stems from \cW and that, for $1 \leq j < i \leq k$, $\I_i
997: \models \cT_j$, hence $\I_k \models \cT$ and stems from $\cW$.
998:
999: Before we prove this theorem, we recall some basics of lattice theory.
1000: For any set $\mathcal{S}$, the powerset of $\mathcal{S}$, denoted by
1001: $2^{\mathcal{S}}$ forms a complete lattice, where the ordering, join and meet
1002: operations are set-inclusion $\subseteq$, union $\cup$, and intersection
1003: $\cap$, respectively. For any complete lattice $\mathcal{L}$, its $n$-fold
1004: cartesian product $\mathcal{L}^n$ is also a complete lattice, with ordering,
1005: join, and meet defined in a pointwise manner.
1006:
1007: For a lattice $\mathcal{L}$, a function $\Phi : \mathcal{L} \rightarrow
1008: \mathcal{L}$ is called monotone, iff, for $x_1,x_2 \in \mathcal{L}$, $x_1
1009: \sqsubseteq x_2$ implies $\Phi(x_1) \sqsubseteq \Phi(x_2)$.
1010:
1011: By Tarski's fixed point theorem \cite{Tars55}, every monotone function $\Phi$
1012: on a complete lattice, has uniquely defined least and greatest fixed points,
1013: i.e., there are elements $\overline x, \underline x \in \mathcal{L}$ such that
1014: \[
1015: \overline x = \Phi(\overline x) \textsf{ and } \underline x = \Phi(\underline x)
1016: \]
1017: and, for all $x \in \mathcal{L}$ with $x = \Phi(x)$,
1018: \[
1019: \underline x \sqsubseteq x \textsf{ and } x \sqsubseteq \overline x .
1020: \]
1021:
1022:
1023: \noindent \textit{Proof of Theorem~\ref{theo:monotone-tbox}.}
1024: $\Tu \cup \Tg \equiv \cT$ is obvious. Let $\cW =
1025: (\Delta^\cW,\cdot^\cW,\LabW)$ be an unfolded witness. We have to show that
1026: there is an interpretation \I stemming from \cW with $\I \models \cT$. Let
1027: $\cT_1, \dots, \cT_k$ be the required partition of $\cT$. We will define \I
1028: inductively, starting with an arbitrary interpretation $\I_0$ stemming from
1029: \cW.
1030:
1031: Assume $\I_{i-1}$ was already defined. We define $\I_i$ from $\I_{i-1}$ as
1032: follows: let $\{ A^i_1 \doteq D^i_1, \dots, A^i_m \doteq D^i_m \}$ be an
1033: enumeration of $\cT_i$. First we need some auxiliary notation: for any
1034: concept $C \in \sL$ we define
1035: \[
1036: C^\cW := \{ x \in \Delta^\cW \mid C \in \LabW(x) \} .
1037: \]
1038:
1039: Using this notation we define the function $\Phi$ mapping subsets
1040: $X_1,\dots,X_m$ of $\Delta^\cW$ to
1041: \begin{gather*}
1042: \begin{array}{l@{\;}l@{\;}l}
1043: ( & ( (A^i_1)^\cW
1044: %\{x \mid A^i_1 \in \Lab^\cW(x) \}
1045: \cup
1046: (D^i_1)^{\I_{i-1}(X_1,\dots,X_m)} ) \setminus
1047: (\neg A^i_1)^\cW, \\
1048: %\{ x \mid \neg A^i_1 \in \Lab^\cW(x) \}, \\
1049: & \dots, \\
1050: & ( (A^i_m)^\cW
1051: % \{x \mid A^i_m \in \Lab^\cW(x) \}
1052: \cup
1053: (D^i_m)^{\I_{i-1}(X_1,\dots,X_m)}) \setminus
1054: (\neg A^i_m)^\cW
1055: %\{ x \mid \neg A^i_m \in \Lab^\cW(x) \}
1056: &)
1057: \end{array}\\
1058: \intertext{where}
1059: \I_{i-1}(X_1,\dots,X_m) := \I_{i-1}[A^i_1 \mapsto X_1, \dots, A^i_m
1060: \mapsto X_m]
1061: \end{gather*}
1062: Since all of the $D^i_j$ are monotone in all of the $A^i_m$, $\Phi$ is a
1063: monontone function. This implies that $\Phi$ has a least fixed point, which
1064: we denote by $(\underline X_1, \dots, \underline X_m)$. We use this fixed
1065: point to define $\I_i$ by
1066: \[
1067: \I_i := \I_{i-1}[A^i_1 \mapsto \underline X_1, \dots, A^i_m \mapsto \underline X_m]
1068: \]
1069:
1070: \noindent \textsc{Claim 1:} For each $0 \leq i \leq k$, $\I_i$ stems
1071: from \cW.
1072:
1073: We show this claim by induction on $i$. We have already required $\I_0$ to
1074: stem from $\cW$. Assume $\I_{i-1}$ stems from $\cW$. Since the only thing that
1075: changes from $\I_{i-1}$ to $\I_i$ is the interpretation of the atomic
1076: concepts $A^i_1, \dots, A^i_m$, we only have to check that $A^i_j \in
1077: \Lab^\cW(x)$ implies $x \in (A^i_j)^{\I_i}$ and $\neg A^i_j \in \Lab^\cW(x)$
1078: implies $x \not \in (A^i_j)^{\I_i}$.
1079:
1080: By definition of $\Phi$, and because $\{x \mid A^i_j \in \Lab^\cW(x) \} \cap
1081: \{x \mid \neg A^i_j \in \Lab^\cW(x) \} = \emptyset$, $A^i_j \in \Lab^\cW(x)$
1082: implies $x \in (A^i_j)^{\I_i}$. Also by the definition of $\Phi$,
1083: $\neg A^i_j \in \Lab^\cW(x)$ implies $x \not \in (A^i_j)^{\I_i}$. Hence,
1084: $\I_i$ stems from $\cW$.
1085:
1086: \noindent \textsc{Claim 2:} For each $1 \leq j \leq i \leq k$, $\I_i \models \cT_j$.
1087:
1088: We prove this claim by induction over $i$ starting from $0$. For $i=0$,
1089: there is nothing to prove. Assume the claim would hold for $\I_{i-1}$. The
1090: only thing that changes from $\I_{i-1}$ to $\I_i$ is the interpretation of
1091: the atomic concepts $A^i_1,\dots A^i_m$ defined in $\cT_i$. Since these
1092: concepts may not occur in $\cT_j$ for $j < i$, the interpretation of the
1093: concepts in these TBoxes does not change, and from $\I_{i-1} \models \cT_j$
1094: follows $\I_i \models \cT_j$ for $1 \leq j \leq i-1$.
1095:
1096: It remains to show that $\I_i \models \cT_i$. Let $A^i_j \doteq D^i_j$ be an
1097: axiom from $\cT_i$. From the definition of $\I_i$ we have
1098: \begin{equation}
1099: \label{eq:eq1}
1100: (A^i_j)^{\I_i} = ( (A^i_j)^\cW
1101: % \{ x \mid A^i_j \in \Lab^\cW(x) \}
1102: \cup (D^i_j)^{\I_i} )
1103: \setminus
1104: (\neg A^i_j)^\cW .
1105: % \{ x \mid \neg A^i_j \in \Lab^\cW(x) \} .
1106: \end{equation}
1107:
1108: $\cW$ is unfolded, hence $A^i_j \in \Lab^\cW(x)$ implies $D^i_j \in
1109: \Lab^\cW(x)$ and, since $\I_i$ stems from $\cW$, this implies $x \in
1110: (D^i_j)^{\I_i}$, thus
1111: \begin{equation}
1112: \label{eq:eq2}
1113: (A^i_j)^\cW
1114: % \{ x \mid A^i_j \in \Lab^\cW(x) \}
1115: \cup (D^i_j)^{\I_i} = (D^i_j)^{\I_i}
1116: \end{equation}
1117: Furthermore, $\neg A^i_j \in \Lab^\cW(x)$ implies $\neg D^i_j \in
1118: \Lab^\cW(x)$ implies $x \in (\neg D^i_j)^{\I_i}$, thus
1119: \begin{equation}
1120: \label{eq:eq3}
1121: (D^i_j)^{\I_i} \setminus
1122: (\neg A^i_j)^\cW
1123: % \{ x \mid \neg A^i_j \in \Lab^\cW(x) \}
1124: = (D^i_j)^{\I_i}
1125: \end{equation}
1126:
1127: Taking together (\ref{eq:eq1}), (\ref{eq:eq2}), and (\ref{eq:eq3}) we get
1128: \[
1129: (A^i_j)^{\I_i} = (D^i_j)^{\I_i} ,
1130: \]
1131: and hence $\I_i \models A^i_j \doteq D^i_j$.
1132:
1133: Together, Claim 1 and Claim 2 prove the theorem, since $\I_k$ is an
1134: interpretation that stems from $\cW$ and satisfies $\cT$. \qed
1135:
1136: This theorem makes it possible to apply the same lazy unfolding strategy as
1137: before to cyclical definitions. Such definitions are quite natural in a logic
1138: that supports inverse roles. For example, an orthopaedic procedure might be
1139: defined as a procedure performed by an orthopaedic surgeon, while an
1140: orthopaedic surgeon might be defined as a surgeon who performs only
1141: orthopaedic procedures:\footnote{This example is only intended for didactic
1142: purposes.}
1143: %
1144: \[
1145: \begin{array}{@{}r@{\;}c@{\;}l@{}}
1146: \Cname{o-procedure} & \doteq & \Cname{procedure} \sqcap (\Some{\Rname{performs}^-}{\Cname{o-surgeon}})\\
1147: \Cname{o-surgeon} & \doteq & \Cname{surgeon} \sqcap
1148: (\All{\Rname{performs}}{\Cname{o-procedure}})
1149: \end{array}
1150: \]
1151:
1152: The absorption algorithm described in Section~\ref{sec:application}
1153: would force the second of these definitions to be added to $\Tg$ as
1154: two general axioms and, although both axioms would subsequently be
1155: absorbed into $\Tu$, the procedure would result in a disjunctive term
1156: being added to one of the definitions in $\Tu$. Using
1157: Theorem~\ref{theo:monotone-tbox} to enhance the absorption algorithm
1158: so that these kinds of definition are directly added to $\Tu$ reduces
1159: the number of disjunctive terms in $\Tu$ and can lead to significant
1160: improvements in performance.
1161:
1162: \begin{figure*}[htb]
1163: \begin{center}
1164: \includegraphics[width=0.75\linewidth]{results.eps}
1165: \end{center}
1166: \caption{Classification times with and without enhanced absorption}
1167: \label{fig:graph2}
1168: \end{figure*}
1169:
1170:
1171: This can be demonstrated by a simple experiment with the new \Fact
1172: system, which implements the \shiq logic~\cite{Horrocks99j} and is
1173: thus able to deal with inverse roles. Figure~\ref{fig:graph2} shows the
1174: classification time in seconds using the normal and enhanced
1175: absorption algorithms for terminologies consisting of between 5 and 50
1176: pairs of cyclical definitions like those described above for
1177: \Cname{o-surgeon} and \Cname{o-procedure}. With
1178: only 10 pairs the gain in performance is already a factor of 30, while
1179: for 45 and 50 pairs it has reached several orders of magnitude: with
1180: the enhanced absorption the terminology is classified in 2--3
1181: seconds whereas with the original algorithm the time required exceeded
1182: the 10,000 second limit imposed in the experiment.
1183:
1184:
1185: It is worth pointing out that it is by no means trivially true that
1186: cyclical definitions can be dealt with by lazy unfolding. Even
1187: without inverse roles it is clear that definitions such as $A \doteq
1188: \Not A$ (or more subtle variants) force the domain to be empty and
1189: would lead to an incorrect absorption if dealt with by lazy unfolding.
1190: With converse roles it is, for example, possible to force the
1191: interpretation of a role $R$ to be empty with a definition such as $A
1192: \doteq \All{R}{(\All{R^-}{\Not A})}$, again leading to an incorrect
1193: absorption if dealt with by lazy unfolding.
1194:
1195:
1196:
1197:
1198:
1199:
1200:
1201:
1202: \section{OPTIMAL ABSORPTIONS}
1203:
1204: We have demonstrated that absorption is a highly effective and widely
1205: applicable technique, and by formally defining correctness criteria for
1206: absorptions we have proved that the procedure used by \Fact finds
1207: correct absorptions. Moreover, by establishing more precise correctness
1208: criteria we have demonstrated how the effectiveness of this procedure
1209: could be further enhanced.
1210:
1211: However, the absorption algorithm used by \Fact is clearly
1212: sub-optimal, in the sense that changes could be made that would, in
1213: general, allow more axioms to be absorbed (e.g., by also giving
1214: special consideration to axioms of the form $\Not A \sqsubseteq C$
1215: with $A \in \NC$). Moreover, the procedure is non-deterministic, and,
1216: while it is guaranteed to produce a correct absorption, its specific
1217: result depends on the order of the axioms in the original TBox \Tau.
1218: Since the semantics of a TBox \Tau does not depend on the order of its
1219: axioms, there is no reason to suppose that they will be arranged in a
1220: way that yields a ``good'' absorption. Given the
1221: effectiveness of absorption, it would be desirable to have an
1222: algorithm that was guaranteed to find the ``best'' absorption possible for
1223: any set of axioms, irrespective of their ordering in the TBox.
1224:
1225: Unfortunately, it is not even clear how to define a sensible
1226: optimality criterion for absorptions. It is obvious that simplistic
1227: approaches based on the number or size of axioms remaining in $\Tg$
1228: will not lead to a useful solution for this problem. Consider, for
1229: example, the cyclical TBox experiment from the previous section. Both the original
1230: \Fact absorption algorithm and the enhanced algorithm, which exploits
1231: Theorem~\ref{theo:monotone-tbox}, are able to compute a complete absorption of
1232: the axioms ( i.e., a correct absorption with $\Tg=\emptyset$), but
1233: the enhanced algorithm leads to much better performance, as
1234: shown in Figure~\ref{fig:graph2}.
1235:
1236: An important issue for future work is, therefore, the identification
1237: of a suitable optimality criterion for absorptions, and the
1238: development of an algorithm that is able to compute absorptions that
1239: are optimal with respect to this criterion.
1240:
1241:
1242: \subsubsection*{Acknowledgements}
1243:
1244: This work was partially supported by the DFG, Project No. GR 1324/3-1.
1245:
1246:
1247:
1248:
1249: \newcommand{\etalchar}[1]{$^{#1}$}
1250: \begin{thebibliography}{BHH{\etalchar{+}}91}
1251:
1252: \bibitem[Baa91]{Baader91c}
1253: F.~Baader.
1254: \newblock Augmenting concept languages by transitive closure of roles: An
1255: alternative to terminological cycles.
1256: \newblock In {\em Proceedings of the 12th International Joint Conference on
1257: Artificial Intelligence (IJCAI-91)}, pages 446--451, 1991.
1258:
1259: \bibitem[BBH96]{BaaderBuchheit+-AIJ-1996}
1260: F.~Baader, M.~Buchheit, and B.~Hollunder.
1261: \newblock Cardinality restrictions on concepts.
1262: \newblock {\em Artificial Intelligence}, 88(1--2):195--213, 1996.
1263:
1264: \bibitem[BDS93]{Buchheit93}
1265: M.~Buchheit, F.~M. Donini, and A.~Schaerf.
1266: \newblock Decidable reasoning in terminological knowledge representation
1267: systems.
1268: \newblock {\em J.\ of Artificial Intelligence Research}, 1:109--138, 1993.
1269:
1270: \bibitem[BFH{\etalchar{+}}94]{BFHNP94}
1271: F.~Baader, E.~Franconi, B.~Hollunder, B.~Nebel, and H.-J. Profitlich.
1272: \newblock An empirical analysis of optimization techniques for terminological
1273: representation systems, or: Making {KRIS} get a move on.
1274: \newblock {\em Applied Artificial Intelligence}, 4:109--132, 1994.
1275:
1276: \bibitem[BFH{\etalchar{+}}99]{Horrocks99i}
1277: A.~Borgida, E.~Franconi, I.~Horrocks, D.~McGuinness, and P.~F. Patel-Schneider.
1278: \newblock Explaining $\mathcal{ALC}$ subsumption.
1279: \newblock In P.~Lambrix, A.~Borgida, M.~Lenzerini, R.~M{\"o}ller, and
1280: P.~Patel-Schneider, editors, {\em Proceedings of the International Workshop
1281: on Description Logics (DL'99)}, pages 37--40, 1999.
1282:
1283: \bibitem[BH91]{Baader91e}
1284: F.~Baader and B.~Hollunder.
1285: \newblock A terminological knowledge representation system with complete
1286: inference algorithms.
1287: \newblock In {\em Processing declarative knowledge: International workshop
1288: PDK'91}, number 567 in Lecture Notes in Artificial Intelligence, pages
1289: 67--86, Berlin, 1991. Springer-Verlag.
1290:
1291: \bibitem[BHH{\etalchar{+}}91]{Baader91b}
1292: F.~Baader, H.-J. Heinsohn, B.~Hollunder, J.~Muller, B.~Nebel, W.~Nutt, and
1293: H.-J. Profitlich.
1294: \newblock Terminological knowledge representation: A proposal for a
1295: terminological logic.
1296: \newblock Technical Memo TM-90-04, Deutsches Forschungszentrum f{\"u}r
1297: K{\"u}nstliche Intelligenz GmbH (DFKI), 1991.
1298:
1299: \bibitem[Cal96]{Calvanese96a}
1300: D.~Calvanese.
1301: \newblock Reasoning with inclusion axioms in description logics: Algorithms and
1302: complexity.
1303: \newblock In Wolfgang Wahlster, editor, {\em Proceedings of the 12th European
1304: Conference on Artificial Intelligence (ECAI'96)}, pages 303--307. John Wiley
1305: \& Sons Ltd., 1996.
1306:
1307: \bibitem[CDL99]{CaDL99}
1308: D.~Calvanese, G.~{De Giacomo}, and M.~Lenzerini.
1309: \newblock Reasoning in expressive description logics with fixpoints based on
1310: automata on infinite trees.
1311: \newblock In {\em Proc.\ of the 16th Int.\ Joint Conf.\ on Artificial
1312: Intelligence (IJCAI'99)}, 1999.
1313:
1314: \bibitem[DDM96]{Donini96a}
1315: F.~Donini, G.~{De~Giacomo}, and F.~Massacci.
1316: \newblock {EXPTIME} tableaux for $\mathcal{ALC}$.
1317: \newblock In L.~Padgham, E.~Franconi, M.~Gehrke, D.~L. McGuinness, and P.~F.
1318: Patel-Schneider, editors, {\em Collected Papers from the International
1319: Description Logics Workshop (DL'96)}, number WS-96-05 in AAAI Technical
1320: Report, pages 107--110. AAAI Press, Menlo Park, California, 1996.
1321:
1322: \bibitem[DL94]{DeLe94}
1323: G.~{De Giacomo} and M.~Lenzerini.
1324: \newblock Boosting the correspondence between description logics and
1325: propositional dynamic logics.
1326: \newblock In {\em Proc.\ of the 12th Nat.\ Conf.\ on Artificial Intelligence
1327: (AAAI'94)}, pages 205--212. {AAAI} Press/The {MIT} Press, 1994.
1328:
1329: \bibitem[DL96]{DeLe96}
1330: G.~{De Giacomo} and M.~Lenzerini.
1331: \newblock {TBox} and {ABox} reasoning in expressive description logics.
1332: \newblock In Luigia~C. Aiello, John Doyle, and Stuart~C. Shapiro, editors, {\em
1333: Proc.\ of the 5th Int.\ Conf.\ on the Principles of Knowledge Representation
1334: and Reasoning (KR'96)}, pages 316--327. Morgan Kaufmann, Los Altos, 1996.
1335:
1336: \bibitem[DMar]{DeGiacomo98a}
1337: G.~{{De~Giacomo}} and F.~Massacci.
1338: \newblock Combining deduction and model checking into tableaux and algorithms
1339: for converse-{PDL}.
1340: \newblock {\em Information and Computation: special issue on the Federated
1341: Logic Conferences}, to appear.
1342:
1343: \bibitem[EH85]{Emerson85}
1344: E.~A. Emerson and J.~Y. Halpern.
1345: \newblock Decision procedures and expressiveness in the temporal logic of
1346: branching time.
1347: \newblock {\em J.\ of Computer and System Sciences}, 30:1--24, 1985.
1348:
1349: \bibitem[HN90]{Hollunder90b}
1350: B.~Hollunder and W.~Nutt.
1351: \newblock Subsumption algorithms for concept languages.
1352: \newblock In {\em Proceedings of the 9th European Conference on Artificial
1353: Intelligence (ECAI'90)}, pages 348--353. John Wiley \& Sons Ltd., 1990.
1354:
1355: \bibitem[HNS90]{HoNS90}
1356: B.~Hollunder, W.~Nutt, and M.~{Schmidt-\hskip0pt Schauss}.
1357: \newblock Subsumption algorithms for concept description languages.
1358: \newblock In {\em ECAI-90}, Pitman Publishing, London, 1990.
1359:
1360: \bibitem[Hor97]{Horrocks97b}
1361: I.~Horrocks.
1362: \newblock {\em Optimising Tableaux Decision Procedures for Description Logics}.
1363: \newblock PhD thesis, University of Manchester, 1997.
1364:
1365: \bibitem[Hor98]{Horrocks98c}
1366: I.~Horrocks.
1367: \newblock Using an expressive description logic: {FaCT} or fiction?
1368: \newblock In A.~G. Cohn, L.~Schubert, and S.~C. Shapiro, editors, {\em
1369: Principles of Knowledge Representation and Reasoning: Proceedings of the
1370: Sixth International Conference (KR'98)}, pages 636--647. Morgan Kaufmann
1371: Publishers, San Francisco, California, June 1998.
1372:
1373: \bibitem[HS99]{Hustadt99a}
1374: U.~Hustadt and R.~A. Schmidt.
1375: \newblock On the relation of resolution and tableaux proof systems for
1376: description logics.
1377: \newblock In {\em Proceedings of the 16th International Joint Conference on
1378: Artificial Intelligence (IJCAI-99)}, pages 110--115, 1999.
1379:
1380: \bibitem[HST99]{Horrocks99j}
1381: I.~Horrocks, U.~Sattler, and S.~Tobies.
1382: \newblock Practical reasoning for expressive description logics.
1383: \newblock In {\em Proceedings of the 6th International Conference on Logic for
1384: Programming and Automated Reasoning (LPAR'99)}, pages 161--180, 1999.
1385:
1386: \bibitem[RNG93]{Rector93a}
1387: A.~L. Rector, W~A Nowlan, and A~Glowinski.
1388: \newblock Goals for concept representation in the \textsc{Galen} project.
1389: \newblock In {\em Proceedings of the 17th Annual Symposium on Computer
1390: Applications in Medical Care (SCAMC'93)}, pages 414--418, Washington DC, USA,
1391: 1993.
1392:
1393: \bibitem[Sch91]{Schi91}
1394: K.~Schild.
1395: \newblock A correspondence theory for terminological logics: Preliminary
1396: report.
1397: \newblock In {\em Proc.\ of the 12th Int.\ Joint Conf.\ on Artificial
1398: Intelligence (IJCAI'91)}, pages 466--471, Sydney, 1991.
1399:
1400: \bibitem[SS91]{SSSm91}
1401: M.~{Schmidt-\hskip0pt Schau{\ss}} and G.~Smolka.
1402: \newblock Attributive concept descriptions with complements.
1403: \newblock {\em Acta Informatica}, 48(1):1--26, 1991.
1404:
1405: \bibitem[Tar55]{Tars55}
1406: A.~Tarski.
1407: \newblock A lattice-theoretical fixpoint theorem and its applications.
1408: \newblock {\em Pacific Journal of Mathematics}, 5:285--309, 1955.
1409:
1410: \bibitem[VW86]{VaWo86}
1411: M.~Y. Vardi and P.~Wolper.
1412: \newblock Automata-theoretic techniques for modal logics of programs.
1413: \newblock {\em J.\ of Computer and System Sciences}, 32:183--221, 1986.
1414: \newblock A preliminary version appeared in {\sl Proc.\ of the 16th ACM SIGACT
1415: Symp.\ on Theory of Computing (STOC'84)}.
1416:
1417: \bibitem[WS92]{Woods92}
1418: W.~A. Woods and J.~G. Schmolze.
1419: \newblock The \textsc{Kl-One} family.
1420: \newblock {\em Computers and Mathematics with Applications -- Special Issue on
1421: Artificial Intelligence}, 23(2--5):133--177, 1992.
1422:
1423: \end{thebibliography}
1424:
1425:
1426: \end{document}
1427:
1428:
1429: