Chair for Automata Theory of the Institute for Theoretical Computer Science, Faculty of Computer Science at TU Dresden

Publications

2007

 A. Artale, R. Kontchakov, C. Lutz, F. Wolter, and M. Zakharyaschev. Temporalising Tractable Description Logics. In Proceedings of the Fourteenth International Symposium on Temporal Representation and Reasoning. IEEE Computer Society Press, 2007.
Bibtex entry  Paper (PDF)

Abstract

It is known that for temporal languages, such as first-order LTL, reasoning about constant (time-independent) relations is almost always undecidable. This applies to temporal description logics as well: constant binary relations together with general concept subsumptions in combinations of LTL and the basic description logic ALC cause undecidability. In this paper, we explore temporal extensions of two recently introduced families of "weak" description logics known as DL-Lite and EL. Our results are twofold: temporalisations of even rather expressive variants of DL-Lite turn out to be decidable, while the temporalisation of EL with general concept subsumptions and constant relations is undecidable.

Alessandro Artale, Carsten Lutz, and David Toman. A Description Logic of Change. In Manuela Veloso, editor, Proceedings of the Twentieth International Joint Conference on Artificial Intelligence (IJCAI'07), pages 218–223. AAAI Press, 2007.
Bibtex entry  Paper (PDF)

Abstract

We combine the modal logic S5 with the description logic (DL) ALCQI. The resulting multi-dimensional DL S5-ALCQI supports reasoning about change by allowing to express that concepts and roles change over time. It cannot, however, discriminate between changes in the past and in the future. Our main technical result is that satisfiability of S5-ALCQI concepts with respect to general TBoxes (including GCIs) is decidable and 2-ExpTime-complete. In contrast, reasoning in temporal DLs that are able to discriminate between past and future is inherently undecidable. We argue that our logic is sufficient for reasoning about temporal conceptual models with time-stamping constraints.

F. Baader, editor. 18th International Conference on Rewriting Techniques and Applications (RTA 2007), volume 4533 of Lecture Notes in Computer Science. Springer-Verlag, 2007.
Bibtex entry  Abstract

Abstract

This volume contains the papers presented at the 18th International Conference on Rewriting Techniques and Applications (RTA'07), which was held on June 26--28, 2007, on the Paris campus of the Conservatoire National des Arts et Metiers (CNAM) in Paris, France.

F. Baader and S. Ghilardi. Connecting Many-Sorted Theories. The Journal of Symbolic Logic, 72(2):535–583, 2007. To appear.
Bibtex entry  Paper (PDF)

Abstract

Basically, the connection of two many-sorted theories is obtained by taking their disjoint union, and then connecting the two parts through connection functions that must behave like homomorphisms on the shared signature. We determine conditions under which decidability of the validity of universal formulae in the component theories transfers to their connection. In addition, we consider variants of the basic connection scheme. Our results can be seen as a generalization of the so-called E-connection approach for combining modal logics to an algebraic setting.

F. Baader, J. Hladik, and R. Peñaloza. Blocking Automata for PSPACE DLs. In D. Calvanese, E. Franconi, and S. Tessaris, editors, Proceedings of the 2007 International Workshop on Description Logics, CEUR-WS, 2007.
Bibtex entry  Paper (PDF)

Abstract

In Description Logics (DLs), both tableau-based and automata-based algorithms are frequently used to show decidability and complexity results for basic inference problems such as concept satisfiability. Whereas tableau-based algorithms usually yield worst-case optimal algorithms in the case of PSPACE-complete logics, it is often very hard to design optimal tableau-based algorithms for EXPTIME-complete DLs. In contrast, the automata-based approach is usually well-suited to prove EXPTIME upper-bounds, but its direct application will usually also yield an EXPTIME-algorithm for a PSPACE-complete logic since the (tree) automaton constructed for a given concept is usually exponentially large. In the present paper, we formulate conditions under which an on-the-fly construction of such an exponentially large automaton can be used to obtain a PSPACE-algorithm. We illustrate the usefulness of this approach by proving a new PSPACE upper-bound for satisfiability of concepts w.r.t. acyclic terminologies in the DL SI.

F. Baader, J. Hladik, and R. Peñaloza. SI! Automata Can Show PSPACE Results for Description Logics. In C. Martin-Vide, editor, Proceedings of the First International Conference on Language and Automata Theory and Applications (LATA'07), Lecture Notes in Computer Science, 2007. To appear.
Bibtex entry  Paper (PS)  Paper (PDF)  ©Springer-Verlag

Abstract

In Description Logics (DLs), both tableau-based and automata-based algorithms are frequently used to show decidability and complexity results for basic inference problems such as satisfiability of concepts. Whereas tableau-based algorithms usually yield worst-case optimal algorithms in the case of PSPACE-complete logics, it is often very hard to design optimal tableau-based algorithms for EXPTIME-complete DLs. In contrast, the automata-based approach is usually well-suited to prove EXPTIME upper-bounds, but its direct application will usually also yield an EXPTIME-algorithm for a PSPACE-complete logic since the (tree) automaton constructed for a given concept is usually exponentially large. In the present paper, we formulate conditions under which an on-the-fly construction of such an exponentially large automaton can be used to obtain a PSPACE-algorithm. We illustrate the usefulness of this approach by proving a new PSPACE upper-bound for satisfiability of concepts w.r.t. acyclic terminologies in the DL SI, which extends the basic DL ALC with transitive and inverse roles.

F. Baader, I. Horrocks, and U. Sattler. Description Logics. In Frank van Harmelen, Vladimir Lifschitz, and Bruce Porter, editors, Handbook of Knowledge Representation, pages 135–179. Elsevier, 2007.
Bibtex entry  Abstract

Abstract

In this chapter we will introduce description logics, a family of logic-based knowledge representation languages that can be used to represent the terminological knowledge of an application domain in a structured way. We will first review their provenance and history, and show how the field has developed. We will then introduce the basic description logic ALC in some detail, including definitions of syntax, semantics and basic reasoning services, and describe important extensions such as inverse roles, number restrictions, and concrete domains. Next, we will discuss the relationship between description logics and other formalisms, in particular first order and modal logics; the most commonly used reasoning techniques, in particular tableaux, resolution and automata based techniques; and the computational complexity of basic reasoning problems. After reviewing some of the most prominent applications of description logics, in particular ontology language applications, we will conclude with an overview of other aspects of description logic research, and with pointers to the relevant literature.

Franz Baader, Bernhard Ganter, Ulrike Sattler, and Baris Sertkaya. Completing Description Logic Knowledge Bases using Formal Concept Analysis. In Proceedings of the Twentieth International Joint Conference on Artificial Intelligence (IJCAI-07). AAAI Press, 2007.
Bibtex entry  Paper (PDF)

Abstract

We propose an approach for extending both the terminological and the assertional part of a Description Logic knowledge base by using information provided by the knowledge base and by a domain expert. The use of techniques from Formal Concept Analysis ensures that, on the one hand, the interaction with the expert is kept to a minimum, and, on the other hand, we can show that the extended knowledge base is complete in a certain, well-defined sense.

Franz Baader, Bernhard Ganter, Ulrike Sattler, and Baris Sertkaya. Completing Description Logic Knowledge Bases using Formal Concept Analysis. In Christine Golbreich, Aditya Kalyanpur, and Bijan Parsia, editors, Proceedings of the Third International Workshop OWL: Experiences and Directions (OWLED 2007), volume 258. CEUR-WS, 2007.
Bibtex entry  Paper (PDF)

Abstract

We propose an approach for extending both the terminological and the assertional part of a Description Logic knowledge base by using information provided by the knowledge base and by a domain expert. The use of techniques from Formal Concept Analysis ensures that, on the one hand, the interaction with the expert is kept to a minimum, and, on the other hand, we can show that the extended knowledge base is complete in a certain, well-defined sense.

Franz Baader, Carsten Lutz, and Boontawee Suntisrivaraporn. Is Tractable Reasoning in Extensions of the Description Logic EL Useful in Practice?. In Journal of Logic, Language and Information, Special Issue on Method for Modality (M4M), 2007. To appear.
Bibtex entry  Paper (PS)  Paper (PDF)

Abstract

Extensions of the description logic EL have recently been proposed as lightweight ontology languages. The most important feature of these extensions is that, despite including powerful expressive means such as general concept inclusion axioms, reasoning can be carried out in polynomial time. In this paper, we consider one of these extensions, EL+, and introduce a refinement of the known polynomial-time classification algorithm for this logic. This refined algorithm was implemented in our CEL reasoner. We describe the results of several experiments with CEL on large ontologies from practice, which show that even a relatively straightforward implementation of the described algorithm outperforms highly optimized, state-of-the-art tableau reasoners for expressive description logics.

Franz Baader and Rafael Peñaloza. Axiom Pinpointing in General Tableaux. In N. Olivetti, editor, Proceedings of the 16th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods TABLEAUX 2007, volume 4548 of Lecture Notes in Computer Science, pages 11–27, Aix-en-Provence, France, 2007. Springer-Verlag.
Bibtex entry  Paper (PDF)  ©Springer-Verlag

Abstract

Axiom pinpointing has been introduced in description logics to help the user to understand the reasons why consequences hold and to remove unwanted consequences by computing minimal (maximal) subsets of the knowledge base that have (do not have) the consequence in question. The pinpointing algorithms described in the DL literature are obtained as extensions of the standard tableau-based reasoning algorithms for computing consequences from DL knowledge bases. Although these extensions are based on similar ideas, they are all introduced for a particular tableau-based algorithm for a particular DL. The purpose of this paper is to develop a general approach for extending a tableau-based algorithm to a pinpointing algorithm. This approach is based on a general definition of "tableaux algorithms," which captures many of the known tableau-based algorithms employed in DLs, but also other kinds of reasoning procedures.

Franz Baader, Rafael Peñaloza, and Boontawee Suntisrivaraporn. Pinpointing in the Description Logic EL. In Proceedings of the 2007 International Workshop on Description Logics (DL2007), CEUR-WS, 2007.
Bibtex entry  Paper (PDF)

Abstract

Axiom pinpointing has been introduced in description logics (DLs) to help the user to understand the reasons why consequences hold by computing minimal subsets of the knowledge base that have the consequence in question. Until now, the pinpointing approach has only been applied to the DL ALC and some of its extensions. This paper considers axiom pinpointing in the DL EL, for which subsumption can be decided in polynomial time. We describe an extension of the subsumption algorithm for EL that can be used to compute all minimal subsets of a given TBox that imply a certain subsumption relationship. We also show that an EL TBox may have exponentially many such minimal subsets and that even finding out whether there is such a minimal subset within a given cardinality bound is an NP-complete problem. In contrast to these negative results, we also show that one such minimal set can be computed in polynomial time. Finally, we provide some encouraging experimental results regarding the performance of a practical algorithm that computes one (not necessarily minimal) set that has a given subsumption relation as consequence.

Franz Baader, Rafael Peñaloza, and Boontawee Suntisrivaraporn. Pinpointing in the Description Logic EL. In Proceedings of the 30th German Conference on Artificial Intelligence (KI2007), volume 4667 of Lecture Notes in Artificial Intelligence, pages 52–67, Osnabrück, Germany, 2007. Springer-Verlag.
Bibtex entry  Paper (PDF)  ©Springer-Verlag

Abstract

Axiom pinpointing has been introduced in description logics (DLs) to help the user understand the reasons why consequences hold by computing minimal subsets of the knowledge base that have the consequence in question. Until now, the pinpointing approach has only been applied to the DL ALC and some of its extensions. This paper considers axiom pinpointing in the less expressive DL EL+, for which subsumption can be decided in polynomial time. More precisely, we consider an extension of the pinpointing problem where the knowledge base is divided into a static part, which is always present, and a refutable part, of which subsets are taken. We describe an extension of the subsumption algorithm for EL+ that can be used to compute all minimal subsets of (the refutable part of) a given TBox that imply a certain subsumption relationship. The worst-case complexity of this algorithm turns out to be exponential. This is not surprising since we can show that a given TBox may have exponentially many such minimal subsets. However, we can also show that the problem is not even output polynomial, i.e., unless P=NP, there cannot be an algorithm computing all such minimal sets that is polynomial in the size of its input and output. In addition, we show that finding out whether there is such a minimal subset within a given cardinality bound is an NP-complete problem. In contrast to these negative results, we also show that one such minimal subset can be computed in polynomial time. Finally, we provide some encouraging experimental results regarding the performance of a practical algorithm that computes one (small, but not necessarily minimal) subset that has a given subsumption relation as consequence.

Franz Baader, Baris Sertkaya, and Anni-Yasmin Turhan. Computing the Least Common Subsumer w.r.t. a Background Terminology. Journal of Applied Logic, 5(3):392–420, 2007.
Bibtex entry  Paper (PS)  Paper (PDF)  ©Journal of Applied Logic

Abstract

Methods for computing the least common subsumer (lcs) are usually restricted to rather inexpressive Description Logics (DLs) whereas existing knowledge bases are written in very expressive DLs. In order to allow the user to re-use concepts defined in such terminologies and still support the definition of new concepts by computing the lcs, we extend the notion of the lcs of concept descriptions to the notion of the lcs w.r.t. a background terminology. We will show both theoretical results on the existence of the least common subsumer in this setting, and describe a practical approach—based on a method from formal concept analysis—for computing good common subsumers, which may, however, not be the least ones. We will also describe results obtained in a first evaluation of this practical approach.

Yusri Bong. Description Logic ABox updates revisited. Master thesis, TU Dresden, Germany, 2007.
Bibtex entry  Paper (PDF)

Abstract

A description logic ABox is a tool to represent a snapshot of the world. Since the world is dynamic, we need a mechanism to update Aboxes. In general, updates can be any kind of information about a change of the world. Here, we consider only basic updates, i.e., updates that are described using only simple ABoxes. There are several known results concerning this kind of update. One of the results is that the existence of nominals and @-constructor is needed to express the updated ABox. More precisely, the simplest DL that is propositionally closed that is able to express the updated ABox is ALCO@. We try to recover the existence of ABox updates in fragments of ALCO@ that are still propositionally closed, by weakening the definition of ABox updates from semantic updates to syntactic updates. It turns out that this weakening is not enough to recover the existence of ABox updates in these DLs. We then try again to further weaken the definition of ABox updates from syntactic updates to extended syntactic updates. With this additional weakening, we recover the existence of ABox updates in ALCO. Unfortunately, this is not the case for ALC. If we only allow ALC ABoxes as the result of updates, then, also this second weakening is still not enough to recover ABox updates in ALC. Then, we recover the existence of extended syntactic ABox updates in ALC by allowing a KB, i.e., a pair of a TBox and an ABox, as the result of the update.

Huang Changsheng. Non-standard inference for explaining subsumption in the description logic EL with general concept inclusions and complex role inclusions. Master thesis, TU Dresden, Germany, 2007.
Bibtex entry  Paper (PDF)

Abstract

Ontologies are now ubiquitous and many of them are currently being ported into logical formalisms, most notably description logic (DL). It is inevitable that such migration might introduces inconsistencies -- both in terms of logical and that of ontological -- which could be far from obvious. This motivates the recent research topic of explanation of DL-based ontologies. Explanation comes in two flavors: pinpointing which addresses the source of inconsistencies found in the ontology and debugging which recovers the ontology into a consistent state. Since the latter often requires information from the former, we consider axiom pinpointing as essential for both flavors of the explanation problem. Much of the research in this area is focusing on expressive DLs, in which standard reasoning alone is already highly intractable. In this paper, we investigate this problem in a tractable extension of EL which is useful in life science applications. We have discovered that pinpointing is inherently intractable -- despite the tractable logic considered -- if all information is required. This is due to the combinatorial blow-up of possible sets of axioms. We develop a labelled algorithm for axiom pinpointing based on the EL subsumption algorithm and the known labelling technique used in tableau algorithm. For implementation purposes, we restrict this algorithm to computation of only partial information, for which polynomial-time algorithm can be obtained. We have experimented this approach on Galen and found that even partial information can already help ease the way an ontology is being debugged.

Birte Glimm, Carsten Lutz, Ian Horrocks, and Ulrike Sattler. Answering conjunctive queries in the SHIQ description logic. In Manuela Veloso, editor, Proceedings of the Twentieth International Joint Conference on Artificial Intelligence (IJCAI'07), pages 299–404. AAAI Press, 2007.
Bibtex entry  Paper (PDF)

Abstract

Conjunctive queries play an important role as an expressive query language for Description Logics (DLs). Although modern DLs usually provide for transitive roles, it was an open problem whether conjunctive query answering over DL knowledge bases is decidable if transitive roles are admitted in the query. In this paper, we consider conjunctive queries over knowledge bases formulated in the popular DL SHIQ and allow transitive roles in both the query and the knowledge base. We show that query answering is decidable and establish the following complexity bounds: regarding combined complexity, we devise a deterministic algorithm for query answering that needs time single exponential in the size of the KB and double exponential in the size of the query. Regarding data complexity, we prove co-NP-completeness.

Stefan Göller, Markus Lohrey, and Carsten Lutz. PDL with Intersection and Converse is 2EXP-complete. In Helmut Seidl, editor, Proceedings of the Tenth International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'07), volume 4423 of Lecture Notes in Computer Science, pages 198–212. Springer-Verlag, 2007.
Bibtex entry  Paper (PDF)

Abstract

We study the complexity of satisfiability in the expressive extension ICPDL of PDL (Propositional Dynamic Logic), which admits intersection and converse as program operations. Our main result is containment in 2EXP, which improves the previously known non-elementary upper bound and implies 2EXP-completeness due to an existing lower bound for PDL with intersection. The proof proceeds by showing that every satisfiable ICPDL formula has a model of tree-width at most two and then giving a reduction to the (non)-emptiness problem for alternating two-way automata on infinite trees. In this way, we also reprove in an elegant way Danecki's difficult result that satisfiability for PDL with intersection is in 2EXP.

Christoph Haase. Complexity of Subsumption in Extensions of EL. Master thesis, TU Dresden, Germany, 2007.
Bibtex entry  Paper (PDF)

Abstract

During the last years, it has been shown that the description logic EL is well-suited for tractable reasoning. In particular, reasoning is even tractable w.r.t. general concept inclusion axioms, and various extensions of EL and their effects on the complexity of subsumption w.r.t. general concept inclusion axioms have been studied. In this thesis, we sharpen the border between tractability and intractability of subsumption in extensions of EL w.r.t. cyclic TBoxes. We provide two new extensions for which subsumption can be computed in polynomial time w.r.t. cyclic TBoxes. The first extends EL by role con- and disjunction in disjunctive normal form, primitive negation and p-admissible concrete domains, and the second by role con- and disjunction in disjunctive normal form and at-least restrictions. Moreover, we show that a combination of the two extensions leads to intractability of subsumption w.r.t. cyclic TBoxes, as well as EL extended by negation, disjunction, transitive closure over role names, functionality and concrete domains with abstract feature chains. This justifies the fact that--except for inverse roles which remain an open problem--both extensions are maximal in the sense that they cannot be further extended without losing tractability of subsumption w.r.t. cyclic TBoxes.

A. Krisnadhi and C. Lutz. Data Complexity in the EL family of DLs. In Proceedings of the 2007 International Workshop on Description Logics (DL2007), CEUR-WS, 2007. To appear.
Bibtex entry  Paper (PDF)

Abstract

We study the data complexity of instance checking and conjunctive query answering in the EL family of DLs, with a particular emphasis on the boundary of tractability. We identify a large number of intractable extensions of EL, but also show that in ELIf, the extension of EL with inverse roles and global functionality, conjunctive query answering is tractable regarding data complexity. In contrast, instance checking in EL extended with only inverse roles or global functionality is ExpTime-complete regarding combined complexity.

Adila Krisnadhi. Data Complexity of Instance Checking in the EL Family of Description Logics. Master thesis, TU Dresden, Germany, 2007.
Bibtex entry  Paper (PDF)

Abstract

Instance checking is the basic problem of querying a description logic knowledge base comprising a TBox and an ABox. Most existing complexity results for instance checking concern combined complexity, which is measured in the size of the whole input consisting of a TBox, an ABox, a query concept and an individual name. However, in many applications, the size of the ABox is much larger than the size of the other parts of the input. Hence, it is more realistic to analyze data complexit, which is measured only in the size of the ABox. This thesis maps out the data complexity of instance checking in the EL family of DLs, a for which the tractability boundary of subsumption has been previously clarified. We identify members of the EL family for which data complexity is coNP-hard (and thus intractable) and members of the EL family for which data complexity is tractable. As an interesting note, these results show that the tractability boundary regarding combined complexity does not coincide with that of data complexity.

Adila Krisnadhi and Carsten Lutz. Data Complexity in the EL family of Description Logics. In Nachum Dershowitz and Andrei Voronkov, editors, Proceedings of the 14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR2007), volume 4790 of Lecture Notes in Artificial Intelligence, pages 333–347. Springer-Verlag, 2007.
Bibtex entry  Paper (PDF)

Abstract

We study the data complexity of instance checking and conjunctive query answering in the EL family of description logics, with a particular emphasis on the boundary of tractability. We identify a large number of intractable extensions of EL, but also show that in ELI^f, the extension of EL with inverse roles and global functionality, conjunctive query answering is tractable regarding data complexity. In contrast, already instance checking in EL extended with only inverse roles or global functionality is ExpTime-complete regarding combined complexity.

C. Löding, C. Lutz, and O. Serre. Propositional Dynamic Logic with Recursive Programs. Journal of Logic and Algebraic Programming, 73:51–69, 2007.
Bibtex entry  Paper (PDF)

Abstract

We extend the propositional dynamic logic PDL of Fischer and Ladner with a restricted kind of recursive programs using the formalism of visibly pushdown automata (Alur, Madhusudan 2004). We show that the satisfiability problem for this extension remains decidable, generalising known decidability results for extensions of PDL by non-regular programs. Our decision procedure establishes a 2- ExpTime upper complexity bound, and we prove a matching lower bound that applies already to rather weak extensions of PDL with non-regular programs. Thus, we also show that such extensions tend to be more complex than standard PDL.

C. Lutz. Inverse Roles Make Conjunctive Queries Hard. In Proceedings of the 2007 International Workshop on Description Logics (DL2007), CEUR-WS, 2007. To appear.
Bibtex entry  Paper (PDF)

Abstract

Conjunctive query answering is an important DL reasoning task. Although this task is by now quite well-understood, tight complexity bounds for conjunctive query answering in expressive DLs have never been obtained: all known algorithms run in deterministic double exponential time, but the existing lower bound is only an ExpTime one. In this paper, we prove that conjunctive query answering in ALCI is 2-ExpTime-hard (and thus complete), and that it becomes NExpTime-complete under some reasonable assumptions.

C. Lutz and M. Milicic. A Tableau Algorithm for DLs with Concrete Domains and GCIs. Journal of Automated Reasoning, 38(1–3):227–259, 2007.
Bibtex entry  Paper (PDF)

Abstract

To use description logics (DLs) in an application, it is crucial to identify a DL that is sufficiently expressive to represent the relevant notions of the application domain, but for which reasoning is still decidable. Two means of expressivity that are required by many modern applications of DLs are concrete domains and general TBoxes. The former are used for decidablening concepts based on concrete qualities of their instances such as the weight, age, duration, and spatial extension. The purpose of the latter is to capture background knowledge by stating that the extension of a concept is included in the extension of another concept. Unfortunately, it is wellknown that combining concrete domains with general TBoxes often leads to DLs for which reasoning is undecidable. In this paper, we identify a general property of concrete domains that is sucient for proving decidability of DLs with both concrete domains and general TBoxes. We exhibit some useful concrete domains, most notably a spatial one based on the RCC-8 relations, which have this property. Then, we present a tableau algorithm for reasoning in DLs equipped with concrete domains and general TBoxes.

Carsten Lutz, Dirk Walther, and Frank Wolter. Conservative Extensions in Expressive Description Logics. In Manuela Veloso, editor, Proceedings of the Twentieth International Joint Conference on Artificial Intelligence (IJCAI'07), pages 453–458. AAAI Press, 2007.
Bibtex entry  Paper (PDF)

Abstract

The notion of a conservative extension plays a central role in ontology design and integration: it can be used to formalize ontology refinements, safe mergings of two ontologies, and independent modules inside an ontology. Regarding reasoning support, the most basic task is to decide whether one ontology is a conservative extension of another. It has recently been proved that this problem is decidable and 2ExpTime-complete if ontologies are formulated in the basic description logic ALC. We consider more expressive description logics and begin to map out the boundary between logics for which conservativity is decidable and those for which it is not. We prove that conservative extensions are 2ExpTime-complete in ALCQI, but undecidable in ALCQIO. We also show that if conservative extensions are defined model-theoretically rather than in terms of the consequence relation, they are undecidable already in ALC.

Carsten Lutz and Frank Wolter. Conservative Extensions in the Lightweight Description Logic EL. In Frank Pfenning, editor, Proceedings of the 21th Conference on Automated Deduction (CADE-21), volume 4603 of Lecture Notes in Artificial Intelligence, pages 84–99. Springer-Verlag, 2007.
Bibtex entry  Paper (PDF)  ©Springer-Verlag

Abstract

We bring together two recent trends in description logic (DL): lightweight DLs in which the subsumption problem is tractable and conservative extensions as a central tool for formalizing notions of ontology design such as refinement and modularity. Our aim is to investigate conservative extensions as an automated reasoning problem for the basic tractable DL EL. The main result is that deciding (deductive) conservative extensions is ExpTime-complete, thus more difficult than subsumption in EL, but not more difficult than subsumption in expressive DLs. We also show that if conservative extensions are defined model-theoretically, the associated decision problem for EL is undecidable.

Maja Milicic. Complexity of Planning in Action Formalisms Based on Description Logics. In Proceedings of the 14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2007), Lecture Notes in Artificial Intelligence. Springer-Verlag, 2007.
Bibtex entry  Paper (PDF)

Abstract

In this paper, we continue the recently started work on integrating action formalisms with description logics (DLs), by investigating planning in the context of DLs. We prove that the plan existence problem is decidable for actions described in fragments of ALCQIO. More precisely, we show that its computational complexity coincides with the one of projection for DLs between ALC and ALCQIO if operators contain only unconditional post-conditions. If we allow for conditional post-conditions, the plan existence problem is shown to be in 2-ExpSpace.

Maja Milicic. Planning in Action Formalisms based on DLs: First Results. In Proceedings of the 2007 International Workshop on Description Logics (DL2007), CEUR-WS, 2007.
Bibtex entry  Paper (PDF)

Abstract

In this paper, we continue the recently started work on integrating action formalisms with description logics (DLs), by investigating planning in the context of DLs. We prove that the plan existence problem is decidable for actions described in fragments of ALCQIO. More precisely, we show that, if post-conditions of operators are unconditional, its computational complexity coincides with the one of projection for DLs between ALC and ALCQIO.

Stefan Schulz, Boontawee Suntisrivaraporn, and Franz Baader. SNOMED CT's Problem List: Ontologists' and Logicians' Therapy Suggestions. In Proceedings of The Medinfo 2007 Congress, Studies in Health Technology and Informatics (SHTI-series). IOS Press, 2007.
Bibtex entry  Paper (PDF)

Abstract

After a critical review of the present architecture of SNOMED CT, addressing both logical and ontological issues, we present a roadmap towards an overall improvement of this terminology. In particular, we recommend the following actions: Upper level categories should be re-arranged according to a standard upper level ontology. Meta-class like concepts should be identified and removed from the taxonomy. SNOMED concepts denoting (non instantiable) individual entities (e.g. geographical regions) should be kept separate from those concepts that denote (instantiable) types. SNOMED binary relations should be reduced to a set of canonical ones, following existing recommendations. Taxonomies should be cleansed and split into disjoint partitions. The number of full definitions should be increased. Finally, we propose a new approach to modeling part-whole hierarchies, as well as the integration of qualifier relations into the description logic framework.

Boontawee Suntisrivaraporn, Franz Baader, Stefan Schulz, and Kent Spackman. Replacing SEP-Triplets in SNOMED CT using Tractable Description Logic Operators. In Jim Hunter Riccardo Bellazzi, Ameen Abu-Hanna, editor, Proceedings of the 11th Conference on Artificial Intelligence in Medicine (AIME'07), Lecture Notes in Computer Science. Springer-Verlag, 2007.
Bibtex entry  Paper (PS)  Paper (PDF)  ©Springer-Verlag

Abstract

Reification of parthood relations according to the SEP-triplet encoding pattern has been employed in the clinical terminology SNOMED CT to simulate transitivity of the part-of relation via transitivity of the is-a relation and to inherit properties along part-of links. In this paper we argue that using a more expressive representation language, which allows for a direct representation of the relevant properties of the part-of relation, makes modelling less error prone while having no adverse effect on the efficiency of reasoning.

Muhammad Tayyab. Analysis of Pinpointing Algorithms for the Description Logic ALC. Master thesis, TU Dresden, Germany, 2007.
Bibtex entry  Paper (PDF)

Abstract

Most commonly used Description Logic reasoning systems provide only limited support for debugging logically inconsistent knowledge bases. Attempts have been made to come up with algorithms that solve the debugging problem by suggesting possible resolutions. These algorithms use the method of pinpointing of the axioms in the knowledge bases that are the possible source of inconsistency. In this thesis, we analyze two of such pinpointing algorithms devised for the Description Logic ALC. These algorithms are extensions of the standard tableau-based reasoning algorithms for the consistency of the knowledge bases represented in ALC. These pinpointing algorithms calculate maximal satisfiable subsets of the original knowledge base by pinpointing minimal sets of the problematic axioms. We have shown in the thesis that although these algorithms appear to be working quite differently from each other but a close analysis reveals that they use the same idea of axiom pinpointing and execute it in a similar fashion. Both contain similar rules to expand the knowledge and the rule applications have similar results in both of the algorithms. But the two algorithms keep the information about the axioms, that generate a particular knowledge portion, in different ways.

Balder ten Cate and Carsten Lutz. Query Containment in Very Expressive XPath dialects. In Leonid Libkin, editor, 26th ACM Symposium on Principles of Database Systems (PODS'07), pages 73–82. ACM Press, 2007.
Bibtex entry  Paper (PDF)

Abstract

Query containment has been studied extensively for fragments of XPath 1.0. For instance, the problem is known to be EXPTIMEcomplete for CoreXPath, the navigational core of XPath 1.0. Much less is known about query containment in (fragments of) the richer language XPath 2.0. In this paper, we consider extensions of CoreXPath with the following operators, which are all part of XPath 2.0 (except the last): path intersection, path equality, path complementation, for-loops, and transitive closure. For each combination of these operators, we determine the complexity of query containment, both with and without DTDs. It turns out to range from EXPTIME (for extensions with path equality) and 2-EXPTIME (for extensions with path intersection) to non-elementary (for extensions with path complementation or for-loops). In almost all cases, adding transitive closure on top has no further impact on the complexity. We also investigate the effect of dropping the upward and/or sibling axes, and show that this sometimes leads to a reduction in complexity. Since the languages we study include negation and conjunction in filters, our complexity results can equivalently be stated in terms of satisfiability. We also analyze the above languages in terms of succinctness.

A.-Y. Turhan and Y. Bong. Speeding up Approximation with Nicer Concepts. In D. Calvanese, E. Franconi, V. Haarslev, D. Lembo, B. Motik, S. Tessaris, and A.-Y. Turhan, editors, Proc. of the 2007 Description Logic Workshop (DL 2007), 2007.
Bibtex entry  Paper (PS)  Paper (PDF)

Abstract

Concept approximation is an inference service for Description Logics that provides ``translations'' of concept descriptions from one DL to a less expressive DL. In [4] a method for optimizing the computation of ALC-ALE-approximations of ALC-concept descriptions was introduced. The idea is to characterize a certain class of concept descriptions for which conjuncts can be approximated independently. In this paper we provide relaxed conditions for this class of ALC-concept descriptions, extend this notion to number restrictions and report on a first implementation of this method for ALCN-ALEN-approximation.

home Back to the homepage of the Chair for Automata Theory.
Generated at Fri Mar 19 16:53:03 CET 2010.