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, volume 3698 of Lecture Notes in Artificial Intelligence, pages 18–33. Springer-Verlag, 2005.
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.

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.

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.

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 Sat Feb 4 10:56:31 CET 2012.