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

Publications

2005

F. Baader, S. Brandt, and C. Lutz. Pushing the EL Envelope. In Proceedings of the Nineteenth International Joint Conference on Artificial Intelligence IJCAI-05, Edinburgh, UK, 2005. Morgan-Kaufmann Publishers.
Bibtex entry Paper (PDF)

Abstract

Recently, it has been shown that the small description logic (DL) EL, which allows for conjunction and existential restrictions, has better algorithmic properties than its counterpart FL0, which allows for conjunction and value restrictions. Whereas the subsumption problem in FL0 becomes already intractable in the presence of acyclic TBoxes, it remains tractable in EL even with general concept inclusion axioms (GCIs). On the one hand, we extend the positive result for EL by identifying a set of expressive means that can be added to EL without sacrificing tractability. On the other hand, we show that basically all other additions of typical DL constructors to EL with GCIs make subsumption intractable, and in most cases even ExpTime-complete. In addition, we show that subsumption in FL0 with GCIs is ExpTime-complete.

F. Baader and S. Ghilardi. Connecting Many-Sorted Structures and Theories through Adjoint Functions. In Proceedings of the 5th International Workshop on Frontiers of Combining Systems (FroCoS'05), volume 3717 of Lecture Notes in Artificial Intelligence, Vienna (Austria), 2005. Springer-Verlag.
Bibtex entry Paper (PS) Paper (PDF) ©Springer-Verlag

Abstract

In a previous paper, we have introduced a general approach for connecting two many-sorted theories through connection functions that behave like homomorphisms on the shared signature, and have shown that, under appropriate algebraic conditions, decidability of the validity of universal formulae in the component theories transfers to their connection. This work generalizes decidability transfer results for so-called E-connections of modal logics. However, in this general algebraic setting, only the most basic type of E-connections could be handled. In the present paper, we overcome this restriction by looking at pairs of connection functions that are adjoint pairs for partial orders defined in the component theories.

F. Baader and S. Ghilardi. Connecting Many-Sorted Theories. In Proceedings of the 20th International Conference on Automated Deduction (CADE-05), volume 3632 of Lecture Notes in Artificial Intelligence, pages 278–294, Tallinn (Estonia), 2005. Springer-Verlag.
Bibtex entry Paper (PS) Paper (PDF) ©Springer-Verlag

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.

F. Baader, I. Horrocks, and U. Sattler. Description Logics as Ontology Languages for the Semantic Web. In D. Hutter and W. Stephan, editors, Mechanizing Mathematical Reasoning: Essays in Honor of Jörg H. Siekmann on the Occasion of His 60th Birthday, volume 2605 of Lecture Notes in Artificial Intelligence, pages 228–248. Springer-Verlag, 2005.
Bibtex entry Paper (PS) Paper (PDF) ©Springer-Verlag

Abstract

The vision of a Semantic Web has recently drawn considerable attention, both from academia and industry. Description logics are often named as one of the tools that can support the Semantic Web and thus help to make this vision reality. In this paper, we describe what description logics are and what they can do for the Semantic Web. Descriptions logics are very useful for defining, integrating, and maintaining ontologies, which provide the SemanticWeb with a common understanding of the basic semantic concepts used to annotate Web pages. We also argue that, without the last decade of basic research in this area, description logics could not play such an important role in this domain.

F. Baader, C. Lutz, M. Milicic, U. Sattler, and F. Wolter. A Description Logic Based Approach to Reasoning about Web Services. In Proceedings of the WWW 2005 Workshop on Web Service Semantics (WSS2005), Chiba City, Japan, 2005.
Bibtex entry Paper (PDF)

Abstract

Motivated by the need for semantically well-founded and algorithmically managable formalisms for describing the functionality of Web services, we introduce an action formalism that is based on description logics (DLs), but is also firmly grounded on research in the reasoning about action community. Our main contribution is an analysis of how the choice of the DL influences the complexity of standard reasoning tasks such as projection and executability, which are important for Web service discovery and composition.

F. Baader, C. Lutz, M. Milicic, U. Sattler, and F. Wolter. Integrating Description Logics and Action Formalisms: First Results. In Proceedings of the Twentieth National Conference on Artificial Intelligence (AAAI-05), Pittsburgh, PA, USA, 2005.
Bibtex entry Paper (PDF)

Abstract

We propose an action formalism that is based on description logics (DLs) and may be viewed as an instance of the Situation Calculus (SitCalc). In particular, description logic concepts can be used for describing the state of the world, and the pre- and post-conditions of actions. The main advantage of such a combination is that, on the one hand, the expressive power for describing world states and conditions is higher than in other decidable fragments of the SitCalc, which are usually propositional. On the other hand, in contrast to the full SitCalc, effective reasoning is still possible. In this paper, we perform a detailed investigation of how the choice of the DL influences the complexity of the standard reasoning tasks executability and projection in the corresponding action formalism. We also discuss semantic and computational problems in natural extensions of our framework.

F. Baader, C. Lutz, M. Milicic, U. Sattler, and F. Wolter. Integrating Description Logics and Action Formalisms: First Results. In Proceedings of the 2005 International Workshop on Description Logics (DL2005), number 147 in CEUR-WS, 2005.
Bibtex entry Paper (PDF)

Abstract

F. Baader, C. Lutz, and B. Suntisrivaraporn. Is Tractable Reasoning in Extensions of the Description Logic EL Useful in Practice?. In Proceedings of the Methods for Modalities Workshop (M4M-05), Berlin, Germany, 2005.
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, which 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.

F. Baader and A. Voronkonv, editors. 11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning LPAR 2004, volume 3452 of Lecture Notes in Artificial Intelligence. Springer-Verlag, Montevideo, Uruguay, 2005.
Bibtex entry Abstract

Abstract

This volume contains the papers presented at the 11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), held from March 14 to 18, 2005, in Montevideo, Uruguay, together with the 5th International Workshop on the Implementation of Logics (organised by Stephan Schulz and Boris Konev) and the Workshop on Analytic Proof Systems (organised by Matthias Baaz).

Franz Baader, Carsten Lutz, Eldar Karabaev, and Manfred Theißen. A New n-ary Existential Quantifier in Description Logics. In Proceedings of the 2005 International Workshop on Description Logics (DL2005), number 147 in CEUR-WS, 2005.
Bibtex entry Paper (PS) Paper (PDF)

Abstract

Motivated by a chemical process engineering application, we introduce a new concept constructor in Description Logics (DLs), an n-ary variant of the existential restriction constructor, which generalizes both the usual existential restrictions and so-called qualified number restrictions. We show that the new constructor can be expressed in ALCQ, the extension of the basic DL ALC by qualified number restrictions. However, this representation results in an exponential blow-up. By giving direct algorithms for ALC extended with the new constructor, we can show that the complexity of reasoning in this new DL is actually not harder than the one of reasoning in ALCQ. Moreover, in our chemical process engineering application, a restricted DL that provides only the new constructor together with conjunction, and satisfies an additional restriction on the occurrence of roles names, is sufficient. For this DL, the subsumption problem is polynomial.

Franz Baader, Carsten Lutz, Eldar Karabaev, and Manfred Theißen. A New n-ary Existential Quantifier in Description Logics. In Proceedings of the 28th Annual German Conference on Artificial Intelligence, KI 2005, Lecture Notes in Artificial Intelligence. Springer-Verlag, 2005. To appear.
Bibtex entry Paper (PS) Paper (PDF) ©Springer-Verlag

Abstract

Sebastian Brandt and Jörg Model. Subsumption in EL w.r.t. hybrid TBoxes. In Proceedings of the 28th Annual German Conference on Artificial Intelligence, KI 2005, Lecture Notes in Artificial Intelligence. Springer-Verlag, 2005.
Bibtex entry Paper (PDF) ©Springer-Verlag

Abstract

In the area of Description Logic (DL) based knowledge representation, two desirable features of DL systems have as yet been incompatible: firstly, the support of general TBoxes containing general concept inclusion (GCI) axioms, and secondly, non-standard inference services facilitating knowledge engineering tasks, such as build-up and maintenance of terminologies (TBoxes). In order to make non-standard inferences available without sacrificing the convenience of GCIs, the present paper proposes hybrid TBoxes consisting of a pair of a general TBox F interpreted by descriptive semantics, and a (possibly) cyclic TBox T interpreted by fixpoint semantics. F serves as a foundation of T in the sense that the GCIs in F define relationships between concepts used as atomic concept names in the definitions in T. % Our main technical result is a polynomial time subsumption algorithm for hybrid EL-TBoxes based on a polynomial reduction to subsumption w.r.t.\ cyclic EL-TBoxes with fixpoint semantics. By virtue of this reduction, all non-standard inferences already available for cyclic EL-TBoxes become available for hybrid ones.

J. Hladik. A Generator for Description Logic Formulas. In I. Horrocks, U. Sattler, and F. Wolter, editors, Proceedings of DL 2005. CEUR-WS, 2005. Available from ceur-ws.org.
Bibtex entry Paper (PDF)

Abstract

We introduce a schema for generating random formulas for different description logics, which extends an existing pattern for modal logics. Using the DL reasoners FaCT and RACER, we test the difficulty of these formulas, and it turns out that the properties that make a formula in an expressive DL hard are quite different from those known for ALC formulas.

E. Karabaev. Reasoning in the Description Logic EL extended with an n-ary existential quantifier. Master thesis, TU Dresden, Germany, 2005.
Bibtex entry Paper (PDF)

Abstract

Motivated by a chemical process engineering application, we introduce a new concept constructor, namely the n-ary variant of the existential restriction, into the Description Logic (DL) EL. We refer to the resulting logic as EL(n) and to its fragment that matches the needs of the real world application as restricted EL(n). Although the new constructor can be expressed in the DL ALCQ, its translation is exponential and introduces many expensive constructors, thus making the translation-based approach impractical. In the present work, we design direct algorithms for deciding the main inference problem, namely subsumption, in restricted EL(n). We show that reasoning in restricted EL(n) is polynomial when we allow for acyclic TBoxes. Additionally, we examine the complexity of reasoning in (unrestricted) EL(n) with general TBoxes. In particular, we show that subsumption in EL(n) with GCIs is ExpTime-complete. In order to test the practical efficiency of our approach, we implement the polynomial algorithm for restricted EL(n) with acyclic TBoxes in a system called Eln. Comparison between Eln and the state-of-the-art DL reasoner RACER demonstrate a considerable advantage of the direct algorithm over the translation-based approach.

M. Lange and C. Lutz. 2-ExpTime lower bounds for Propositional Dynamic Logics with intersection. Journal of Symbolic Logic, 70(5):1072–1086, 2005.
Bibtex entry Paper (PS)

Abstract

In 1984, Danecki proved that satisfiability in IPDL, i.e., Propositional Dynamic Logic (PDL) extended with an intersection operator on programs, is decidable in deterministic double exponential time. Since then, the exact complexity of IPDL has remained an open problem: the best known lower bound was the ExpTime one stemming from plain PDL until, in 2004, the first author established ExpSpace-hardness. In this paper, we finally close the gap and prove that IPDL is hard for 2-ExpTime, thus 2-ExpTime-complete. We then sharpen our lower bound, showing that it even applies to IPDL without the test operator interpreted on tree structures.

Hongkai Liu. Matching in Description Logics with Existential Restrictions and Terminological Cycles. Master's thesis, Dresden University of Technology, Germany, 2005.
Bibtex entry Paper (PS)

Abstract

Matching of concepts against patterns is a so-called non-standard inference problem in Description Logics. For the small description language EL, matching problems without terminological cycles have been investigated. In the present thesis we introduce EL-matching problems allowing terminological cycles. Among the three different semantics defined by Nebel for the interpretation of cyclic TBoxes we will argue that gfp-semantics is the appropriate one to define matching problems. Based on deciding subsumption and computing the least common subsumers, a matching algorithm is provided whose soundness and completeness is shown. Moreover, the matching algorithm is implemented and tested in the programming language LISP.

C. Lutz. PDL with Intersection and Converse is Decidable. In Annual Conference of the European Association for Computer Science Logic CSL'05, LNCS. Springer Verlag, 2005.
Bibtex entry Paper (PS)

Abstract

In its many guises and variations, propositional dynamic logic (PDL) plays an important role in various areas of computer science such as databases, artificial intelligence, and computer linguistics. One relevant and powerful variation is ICPDL, the extension of PDL with intersection and converse. Although ICPDL has several interesting applications, its computational properties have never been investigated. In this paper, we prove that ICPDL is decidable by developing a translation to the monadic second order logic of infinite trees. Our result has applications in information logic, description logic, and epistemic logic. In particular, we solve a long-standing open problem in information logic. Another virtue of our approach is that it provides a decidability proof that is more transparent than existing ones for PDL with intersection (but without converse).

C. Lutz, C. Areces, I. Horrocks, and U. Sattler. Keys, Nominals, and Concrete Domains. Journal of Artificial Intelligence Research, 23:667–726, 2005.
Bibtex entry Paper (PS)

Abstract

Many description logics (DLs) combine knowledge representation on an abstract, logical level with an interface to "concrete" domains like numbers and strings with built-in predicates such as <, +, and prefix-of. These hybrid DLs have turned out to be useful in several application areas, such as reasoning about conceptual database models. We propose to further extend such DLs with key constraints that allow the expression of statements like "US citizens are uniquely identified by their social security number". Based on this idea, we introduce a number of natural description logics and perform a detailed analysis of their decidability and computational complexity. It turns out that naive extensions with key constraints easily lead to undecidability, whereas more careful extensions yield NExpTime-complete DLs for a variety of useful concrete domains.

C. Lutz and M. Milicic. A Tableau Algorithm for Description Logics with Concrete Domains and GCIs. In Proceedings of the 14th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods TABLEAUX 2005, LNAI, Koblenz, Germany, 2005. Springer.
Bibtex entry Paper (PDF) ©Springer-Verlag

Abstract

In description logics (DLs), concrete domains are used for defining concepts based on concrete qualities of their instances such as the weight, age, duration, and spatial extension. So-called general concept inclusions (GCIs) play an important role for capturing background knowledge. It is well-known that, when combining concrete domains with GCIs, reasoning easily becomes undecidable. In this paper, we identify a general property of concrete domains that is sufficient for proving decidability of DLs with both concrete domains and GCIs. 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 GCIs.

C. Lutz and M. Milicic. A Tableau Algorithm for DLs with Concrete Domains and GCIs. In Proceedings of the 2005 International Workshop on Description Logics (DL2005), number 147 in CEUR-WS, 2005.
Bibtex entry Paper (PDF)

Abstract

We identify a general property of concrete domains that is sufficient for proving decidability of DLs equipped with them and GCIs. We show that some useful concrete domains, such as a temporal one based on the Allen relations and a spatial one based on the RCC-8 relations, have this property. Then, we present a tableau algorithm for reasoning in DLs equipped with such concrete domains.

C. Lutz, U. Sattler, and L. Tendera. The Complexity of Finite Model Reasoning in Description Logics. Information and Computation, 199:132–171, 2005.
Bibtex entry Paper (PS)

Abstract

We analyse the complexity of finite model reasoning in the description logic ALCQI, i.e. ALC augmented with qualifying number restrictions, inverse roles, and general TBoxes. It turns out that all relevant reasoning tasks such as concept satisfiability and ABox consistency are Exptime-complete, regardless of whether the numbers in number restrictions are coded unarily or binarily. Thus, finite model reasoning with ALCQI is not harder than standard reasoning with ALCQI.

C. Lutz and D. Walther. PDL with Negation of Atomic Programs. Journal of Applied Non-Classical Logic, 15(2):189–214, 2005.
Bibtex entry Paper (PS)

Abstract

Propositional dynamic logic (PDL) is one of the most successful variants of modal logic. To make it even more useful for applications, many extensions of PDL have been considered in the literature. A very natural and useful such extension is with negation of programs. Unfortunately, as long known, reasoning with the resulting logic is undecidable. In this paper, we consider the extension of PDL with negation of atomic programs, only. We argue that this logic is still useful, e.g. in the context of description logics, and prove that satisfiability is decidable and ExpTime-complete using an approach based on Buechi tree automata.

C. Lutz, D. Walther, and F. Wolter. Quantitative Temporal Logics: PSpace and below. In Proceedings of the Twelfth International Symposium on Temporal Representation and Reasoning, Burlington, VT, USA, 2005. IEEE Computer Society Press.
Bibtex entry Paper (PDF)

Abstract

Often, the addition of metric operators to qualitative temporal logics leads to an increase of the complexity of satisfiability by at least one exponential. In this paper, we exhibit a number of metric extensions of qualitative temporal logics of the real line that do not lead to an increase in computational complexity. We show that the language obtained by extending since/until logic of the real line with the operators `sometime within n time units', n coded in binary, is PSpace-complete even without the finite variability assumption. Without qualitative temporal operators the complexity of this language turns out to depend on whether binary or unary coding of parameters is assumed: it is still PSpace-hard under binary coding but in NP under unary coding.

J. Model. Subsumtion in EL bezüglich hybrider TBoxen. Diploma thesis, TU Dresden, Germany, 2005.
Bibtex entry Paper (PS)

Abstract

Für die Beschreibungslogik EL ist gezeigt worden, dass das Subsumtionsproblem für zyklische TBoxen in polynomieller Laufzeit entscheidbar ist, sowohl mit gfp-Semantik, als auch mit deskriptiver Semantik. Auch das 'kleinste gemeinsame Oberkonzept' (lcs) von zwei Konzepten aus einer zyklischen EL-TBbox existiert immer und kann in polynomieller Zeit berechnet werden, wenn man die gfp-Semantik zugrunde legt. Ebenso wurde auch für generelle EL-TBoxen mit GCIs bezüglich deskriptiver Semantik ein polynomieller Subsumtionsalgorithmus angegeben. Da es beim Vorkommen von GCIs nicht sinnvoll ist, TBoxen mit gfp-Semantik zu interpretieren, andererseits nur die gfp-Semantik für zyklische EL-TBoxen die wünschenswerte Eigenschaft garantiert, dass das lcs immer existiert und in polynomieller Zeit berechnet werden kann, wurde eine eine neue Art von TBoxen konzipiert, in der sowohl zyklische Definitionen vorkommen, die mit gfp-Semantik interpretiert werden, als auch GCIs, die mit deskriptiver Semantik interpretiert werden. Wir zeigen, dass das Subsumtionsproblem für diese hybriden EL-TBoxen in polynomieller Zeit auf das Subsumtionsproblem für zyklische TBoxen mit gfp-Semantik reduziert werden kann und geben ein Verfahren dafür an. Außerdem wird eine prototypische Implementierung in LISP vorgestellt, die auf bestehenden Implementierungen für das Subsumtionsproblem von generellen TBoxen und zyklischen EL-TBoxen mit gfp-Semantik aufbaut.

B. Suntisrivaraporn. Optimization and Implementation of Subsumption Algorithms for the Description Logic EL with cyclic TBoxes and General Concept Inclusion Axioms. Master thesis, TU Dresden, Germany, 2005.
Bibtex entry Paper (PDF)

Abstract

The subsumption problem in the description logic (DL) EL has been shown to be polynomial regardless of whether cyclic or acyclic TBoxes are used. Recently, it was shown that the problem remains tractable even when admitting general concept inclusion (GCI) axioms. Motivated by its nice complexity and sufficient expressiveness for some applications, we propose three decision procedures for computing subsumption in the DL EL whose run-time is bounded by a low-degree polynomial. The three decision procedures are for three terminological settings in EL: TBoxes with greatest fixpoint semantics (ELgfp), TBoxes with descriptive semantics (ELdes), and terminologies with GCIs (ELgci). For subsumption wrt TBoxes, i.e. ELgfp and ELdes, we use a characterization through simulations on so-called EL-description graphs---the syntactically normalized representation of EL-TBoxes. With an efficient algorithm for computing simulations on graphs, we show that ELgfp-subsumption can be decided in time cubic in the size of the input TBox. We decide ELdes-subsumption by reducing the simulation problem on graphs to the satisfiability problem of Horn formulae. Then, we apply a linear-time Horn-SAT algorithm to our Horn formulae. This approach yields a quartic-time decision procedure for ELdes-subsumption. Concerning terminologies with GCIs, we employ a different normalization and characterize subsumption through so-called implication sets. We show that ELgci-subsumption can be decided in time cubic in the size of the input terminology, by translating the implication sets into a Horn formula and exploiting the linear-time Horn-SAT algorithm similarly to ELdes. Besides, we implement these decision procedures in the Common LISP language and evaluate their efficiency using the Gene Ontology as a benchmark. The implementation can be used as terminological reasoners that classify ontologies represented in EL-TBoxes.

Anni-Yasmin Turhan. Pushing the SONIC border — SONIC 1.0. In Reinhold Letz, editor, FTP 2005 — Fifth International Workshop on First-Order Theorem Proving. Technical Report University of Koblenz, 2005. http://www.uni-koblenz.de/fb4/publikationen/gelbereihe/RR-13-2005.pdf.
Bibtex entry Paper (PS) Paper (PDF)

Abstract

This paper reports on extensions of the Description Logics non-standard inference system SONIC. The recent contributions to the system are two-fold. Firstly, SONIC is extended by two new of non-standard inferences, namely, implementations of the good common subsumer w.r.t. a background terminology and a heuristics for computing a minimal rewriting. Secondly, SONIC is available as a plugin for the well-known ontology editor Protege.

Back to the homepage of the Chair for Automata Theory.

Generated at Fri Mar 19 16:53:03 CET 2010.