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

Publications

2004

A. Artale and C. Lutz. A Correspondence between Temporal Description Logics. Journal of Applied Non-Classical Logic, 14(1–2):209–233, 2004.
Bibtex entry Paper (PS)

Abstract

In this paper, we investigate the relationship between two decidable interval-based temporal description logics that have been proposed in the literature, TL-ALCF and ALCF(A). Although many aspects of these two logics are quite similar, the two logics suggest two rather different paradigms for representing temporal conceptual knowledge. In this paper, we exhibit a reduction from TL-ALCF concepts to ALCF(A) concepts that serves two purposes: first, it nicely illustrates the relationship between the two knowledge representation paradigms; and second, it provides a tight PSpace upper bound for TL-ALCF concept satisfiabiliy, whose complexity was previously unknown.

F. Baader. A Graph-Theoretic Generalization of the Least Common Subsumer and the Most Specific Concept in the Description Logic EL. In J. Hromkovic and M. Nagl, editors, Proceedings of the 30th International Workshop on Graph-Theoretic Concepts in Computer Science (WG 2004), volume 3353 of Lecture Notes in Computer Science, pages 177–188, Bad Honnef, Germany, 2004. Springer-Verlag.
Bibtex entry Paper (PS) Paper (PDF) ©Springer-Verlag

Abstract

In two previous papers we have investigates the problem of computing the least common subsumer (lcs) and the most specific concept (msc) for the description logic EL in the presence of terminological cycles that are interpreted with descriptive semantics, which is the usual first-order semantics for description logics. In this setting, neither the lcs nor the msc needs to exist. We were able to characterize the cases in which the lcs/msc exists, but it was not clear whether this characterization yields decidability of the existence problem. In the present paper, we develop a common graph-theoretic generalization of these characterizations, and show that the resulting property is indeed decidable, thus yielding decidability of the existence of the lcs and the msc. This is achieved by expressing the property in monadic second-order logic on infinite trees. We also show that, if it exists, then the lcs/msc can be computed in polynomial time.

F. Baader, S. Ghilardi, and C. Tinelli. A New Combination Procedure for the Word Problem that Generalizes Fusion Decidability Results in Modal Logics. In D. Basin and M. Rusinowitch, editors, Proceedings of the 2nd International Joint Conference on Automated Reasoning (IJCAR'04), volume 3097 of Lecture Notes in Artificial Intelligence, pages 183–197. Springer-Verlag, 2004.
Bibtex entry Paper (PS) Paper (PDF) ©Springer-Verlag

Abstract

Previous results for combining decision procedures for the word problem in the non-disjoint case do not apply to equational theories induced by modal logics---whose combination is not disjoint since they share the theory of Boolean algebras. Conversely, decidability results for the fusion of modal logics are strongly tailored towards the special theories at hand, and thus do not generalize to other equational theories. In this paper, we present a new approach for combining decision procedures for the word problem in the non-disjoint case that applies to equational theories induced by modal logics, but is not restricted to them. The known fusion decidability results for modal logics are instances of our approach. However, even for equational theories induced by modal logics our results are more general since they are not restricted to so-called normal modal logics.

F. Baader, I. Horrocks, and U. Sattler. Description Logics. In S. Staab and R. Studer, editors, Handbook on Ontologies, International Handbooks in Information Systems, pages 3–28. Springer–Verlag, Berlin, Germany, 2004.
Bibtex entry Abstract

Abstract

In this chapter, we explain what description logics are and why they make good ontology languages. In particular, we introduce the description logic SHIQ, which has formed the basis of several well-known ontology languages, including OWL.We argue that, without the last decade of basic research in description logics, this family of knowledge representation languages could not have played such an important role in this context. Description logic reasoning can be used both during the design phase, in order to improve the quality of ontologies, and in the deployment phase, in order to exploit the rich structure of ontologies and ontology based information. We discuss the extensions to SHIQ that are required for languages such as OWL and, finally, we sketch how novel reasoning services can support building DL knowledge bases.

F. Baader and B. Sertkaya. Applying Formal Concept Analysis to Description Logics. In P. Eklund, editor, Proceedings of the 2nd International Conference on Formal Concept Analysis (ICFCA 2004), volume 2961 of Lecture Notes in Artificial Intelligence, pages 261–286. Springer, 2004.
Bibtex entry Paper (PS) Paper (PDF) ©Springer-Verlag

Abstract

Given a finite set S := {C1, ..., Cn} of description logic concepts, we are interested in computing the subsumption hierarchy of all least common subsumers of subsets of S as well as the hierarchy of all conjunctions of subsets of S. These hierarchies can be used to support the bottom-up construction of description logic knowledge bases. The point is to compute the first hierarchy without having to compute the least common subsumer for all subsets of S, and the second hierarchy without having to check all possible pairs of such conjunctions explicitly for subsumption. We will show that methods from formal concept analysis developed for computing concept lattices can be employed for this purpose.

F. Baader, B. Sertkaya, and A.-Y. Turhan. Computing the Least Common Subsumer w.r.t. a Background Terminology. In José Júlio Alferes and João Alexandre Leite, editors, Proceedings of the 9th European Conference on Logics in Artificial Intelligence (JELIA 2004), volume 3229 of Lecture Notes in Computer Science, pages 400–412, Lisbon, Portugal, 2004. Springer-Verlag.
Bibtex entry Paper (PS) Paper (PDF) ©Springer-Verlag

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 both show a theoretical result 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.

Franz Baader, Baris Sertkaya, and Anni-Yasmin Turhan. Computing the Least Common Subsumer w.r.t. a Background Terminology. In Proceedings of the 2004 International Workshop on Description Logics (DL2004), CEUR-WS, 2004.
Bibtex entry Paper (PS) Paper (PDF)

Abstract

Methods for computing the least common subsumer (lcs) are usually restricted to rather inexpressive 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.

Sebastian Brandt. On Subsumption and Instance Problem in ELH w.r.t. General TBoxes. In Proceedings of the 2004 International Workshop on Description Logics (DL2004), CEUR-WS, 2004.
Bibtex entry Paper (PDF)

Abstract

Recently, it was shown for the DL EL that subsumption and instance problem w.r.t. cyclic terminologies can be decided in polynomial time. In this paper, we show that both problems remain tractable even when admitting general concept inclusion axioms and simple role inclusion axioms.

Sebastian Brandt. Polynomial Time Reasoning in a Description Logic with Existential Restrictions, GCI Axioms, and—What Else?. In R. López de Mantáras and L. Saitta, editors, Proceedings of the 16th European Conference on Artificial Intelligence (ECAI-2004), pages 298–302. IOS Press, 2004.
Bibtex entry Paper (PDF)

Abstract

In the area of Description Logic (DL) based knowledge representation, research on reasoning w.r.t. general terminologies has mainly focused on very expressive DLs. Recently, though, it was shown for the DL EL, providing only the constructors conjunction and existential restriction, that the subsumption problem w.r.t.\ cyclic terminologies can be decided in polynomial time, a surprisingly low upper bound. In this paper, we show that even admitting general concept inclusion (GCI) axioms and role hierarchies in EL terminologies preserves the polynomial time upper bound for subsumption. We also show that subsumption becomes co-NP hard when adding one of the constructors number restriction, disjunction, and `allsome', an operator used in the DL K-Rep. An interesting implication of the first result is that reasoning over the widely used medical terminology SNOMED is possible in polynomial time.

Sebastian Brandt and Hongkai Liu. Implementing Matching in ALN. In Proceedings of the KI-2004 Workshop on Applications of Description Logics (KI-ADL'04), CEUR-WS, Ulm, Germany, September 2004.
Bibtex entry Paper (PDF)

Abstract

Although matching in Description Logics (DLs) is theoretically well-investigated, an implementation of a matching algorithm exists only for the DL ALE. The present paper presents an implementation of an existing polynomial time matching algorithm for the DL ALN. Benchmarks using randomly generated matching problems indicate a relatively good performance even on large matching problems. Nevertheless, striking differences are revealed by direct comparison between the ALN- and the ALE-algorithm w.r.t. FL(-)-matching problems.

Mitchell A. Harris and Edward R. Reingold. Line Drawing, Leap Years, and Euclid. ACM Computing Surveys, 36:68–80, 2004.
Bibtex entry Paper (PDF)

Abstract

Bresenham's algorithm minimizes error in drawing lines on integer grid points; leap year calculations, surprisingly, are a generalization. We compare the two calculations, explicate the pattern, and discuss the connection of the leap year/line pattern with integer division and Euclid's algorithm for computing the greatest common divisor.

T. Hinze and M. Sturm. Rechnen mit DNA - Eine Einführung in Theorie und Praxis. R. Oldenbourg Wissenschaftsverlag München, ISBN 3-486-27530-5, 2004.
Bibtex entry Paper (PDF)

Abstract

Das Buch bietet eine umfassende und systematische Einführung in das interdisziplinär geprägte Wissensgebiet des DNA-Computing einschließlich seiner mathematischen wie auch molekularbiologischen Grundlagen. Im Zentrum des DNA-Computing stehen biologische Rechner, bei denen organische Moleküle als Speichermedium dienen und Rechenoperationen durch geeignete molekularbiologische und biochemische Prozesse im Reagenzglas ausgeführt werden. Algorithmen, die DNA-basiert konstruiert sind, nutzen eine massive Datenparallelität, die es ermöglicht, mit DNA-Computern Leistungsparameter zu erreichen, die einen Vergleich zu bekannter elektronischer Rechentechnik herausfordern. Bereits heute existiert eine Vielzahl interessanter praktischer Anwendungsfelder, deren Kommerzialisierung schon begonnen hat. Neben der Vermittlung von Basiswissen zum DNA-Computing werden Modelle, Methoden und Techniken vorgestellt, die eine Realisierung im Labor vorbereiten. Einen Schwerpunkt bildet die labornahe Simulation von Prozessen des DNA-Computing.

J. Hladik. Spinoza's Ontology. In G. Büchel, B. Klein, and T. Roth-Berghofer, editors, Proceedings of the 1st Workshop on Philosophy and Informatics (WSPI 2004), number RR-04-02 in DFKI Research Reports. DFKI, 2004.
Bibtex entry Paper (PDF)

Abstract

We examine the possibility of applying knowledge representation and automated reasoning in the context of philosophical ontology. For this purpose, we use the axioms and propositions in the first book of Spinoza's Ethics as knowledge base and a tableau-based satisfiability tester as reasoner. We are able to reconstruct most of Spinoza's system with formal logic, but this requires additional axioms which are assumed implicitly by Spinoza. This study illustrates how tools developed in computer science can be of practical use for philosophy.

J. Hladik. A Tableau System for the Description Logic SHIO. In Ulrike Sattler, editor, Contributions to the Doctoral Programme of IJCAR 2004. CEUR, 2004. Available from ceur-ws.org.
Bibtex entry Paper (PS)

Abstract

Tableau systems are a framework for tableau algorithms which tries to combine the advantages of tableau and automata algorithms, in particular efficiency in practice and worst-case complexity. In this paper, we present a tableau system for the expressive description logic SHIO and prove that the satisfiability problem for SHIO concepts is EXPTIME-complete. The succinctness of the proofs illustrates the usefulness of the tableau system framework.

J. Hladik and J. Model. Tableau Systems for SHIO and SHIQ. In V. Haarslev and R. Möller, editors, Proceedings of the 2004 International Workshop on Description Logics (DL 2004). CEUR, 2004. Available from ceur-ws.org.
Bibtex entry Paper (PDF)

Abstract

Tableau systems are a framework for tableau algorithms which tries to combine the advantages of tableau and automata algorithms, in particular efficiency in practice and worst-case complexity. In this paper, we present tableau systems for two expressive description logics, firstly the well-known SHIQ, and secondly SHIO, which has not been examined so far. The succinctness of the proofs illustrates the usefulness of the tableau system framework. As a corollary, we obtain that satisfiability of SHIO concepts is EXPTIME-complete.

E. Karabaev and C. Lutz. Mona as a DL Reasoner. In Proceedings of the 2004 International Workshop on Description Logics (DL2004), CEUR-WS, 2004.
Bibtex entry Paper (PS)

Abstract

We show how the Mona tool for reasoning in the monadic second order theories WS1S and WS2S can be used to obtain decision procedures for description logics. The performance of this approach is evaluated and compared to the dedicated DL reasoners FaCT and RACER.

R. Kontchakov, C. Lutz, F. Wolter, and M. Zakharyaschev. Temporal Tableaux. Studia Logica, 76(1):91–134, 2004.
Bibtex entry Paper (PS)

Abstract

As a remedy for the bad computational behaviour of first-order temporal logic (FOTL), it has recently been proposed to restrict the application of temporal operators to formulas with at most one free variable thereby obtaining so-called monodic fragments of FOTL. In this paper, we are concerned with constructing tableau algorithms for monodic fragments based on decidable fragments of first-order logic like the two-variable fragment or the guarded fragment. We present a general framework that shows how existing decision procedures for first-order fragments can be used for constructing a tableau algorithm for the corresponding monodic fragment of FOTL. Some example instantiations of the framework are presented.

O. Kutz, C. Lutz, F. Wolter, and M. Zakharyaschev. E-Connections of Abstract Description Systems. Artificial Intelligence, 156(1):1–73, 2004.
Bibtex entry Paper (PS)

Abstract

Combining knowledge representation and reasoning formalisms is an important and challenging task. It is important because non-trivial AI applications often comprise different aspects of the world, thus requiring suitable combinations of available formalisms modeling each of these aspects. It is challenging because the computational behavior of the resulting hybrids is often much worse than the behavior of their components. In this paper, we propose a new combination method which is computationally robust in the sense that the combination of decidable formalisms is again decidable, and which, nonetheless, allows non-trivial interactions between the combined components. The new method, called E-connection, is defined in terms of abstract description systems (ADSs), a common generalization of description logics, many logics of time and space, as well as modal and epistemic logics. The basic idea of E-connections is that the interpretation domains of n combined systems are disjoint, and that these domains are connected by means of n-ary `link relations.' We define several natural variants of E-connections and study in-depth the transfer of decidability from the component systems to their E-connections.

C. Lutz. Combining Interval-based Temporal Reasoning with General TBoxes. Artificial Intelligence, 152(2):235–274, 2004.
Bibtex entry Paper (PS)

Abstract

While classical Description Logics (DLs) concentrate on the representation of static conceptual knowledge, recently there is a growing interest in DLs that, additionally, allow to capture the temporal aspects of conceptual knowledge. Such temporal DLs are based either on time points or on time intervals as the temporal primitive. Whereas point-based temporal DLs are well-investigated, this is not the case for interval-based temporal DLs: all known logics either suffer from rather limited expressive power or have undecidable reasoning problems. In particular, there exists no decidable interval-based temporal DL that provides for general TBoxes-one of the most important expressive means in modern description logics. In this paper, for the first time we define an interval-temporal DL that is equipped with general TBoxes and for which reasoning is decidable (and, more precisely, ExpTime-complete).

C. Lutz and M. Milicic. Description Logics with Concrete Domains and Functional Dependencies. In Proceedings of the 16th European Conference on Artificial Intelligence (ECAI-2004), 2004. To appear.
Bibtex entry Paper (PS)

Abstract

Description Logics (DLs) with concrete domains are a useful tool in many applications. To further enhance the expressive power of such DLs, it has been proposed to add database-style key constraints. Up to now, however, only uniqueness constraints have been considered in this context, thus neglecting the second fundamental family of key constraints: functional dependencies. In this paper, we consider the basic DL with concrete domains \alcd, extend it with functional dependencies, and analyze the impact of this extension on the decidability and complexity of reasoning. Though intuitively the expressivity of functional dependencies seems weaker than that of uniqueness constraints, we are able to show that the former have a similarly severe impact on the computational properties: reasoning is undecidable in the general case, and \NExpTime-complete in some slightly restricted variants of our logic.

C. Lutz and D. Walther. PDL with Negation of Atomic Programs. In Proceedings of the 2nd International Joint Conference on Automated Reasoning IJCAR'04, Lecture Notes in Artificial Intelligence. Springer Verlag, 2004. To appear.
Bibtex entry Paper (PS) ©Springer-Verlag

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, it is long known that 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 and F. Wolter. Modal Logics of Topological Relations. In Proceedings of Advances in Modal Logics 2004, 2004.
Bibtex entry Paper (PS)

Abstract

We introduce a family of modal logics that are interpreted in domains consisting of regions in topological spaces, in particular the real plane. The underlying modal language has 8 operators interpreted by the RCC8 (or Egenhofer-Franzosa)-relations between regions. The following results on the expressive power and computational complexity of the resulting modal systems are obtained: they are expressively complete for the two-variable fragment of first-order logic, and are usually undecidable and often not even recursively enumerable. This also holds if we interpret our language in the class of all (finite) substructures of full region spaces. If interpreted in region spaces consisting of intervals in the real line, our results significantly extend undecidability results of Halpern and Shoham in that we prove the undecidability of interval temporal logic over the class of all substructures of all full interval structures. We also analyze modal logics based on the set of RCC5-relations which are more coarse than the RCC8 relations.

Carsten Lutz. NExpTime-complete Description Logics with Concrete Domains. ACM Transactions on Computational Logic, 5(4):669–705, 2004.
Bibtex entry Abstract

Abstract

Concrete domains are an extension of Description Logics (DLs) that allows to integrate reasoning about conceptual knowledge with reasoning about ``concrete qualities'' of real-world entities such as their sizes, weights, and durations. In this paper, we are concerned with the complexity of Description Logics providing for concrete domains: starting from the complexity result established in [Lutz 2002b], which states that reasoning with the basic propositionally closed DL with concrete domains ALC(D) is PSpace-complete (provided that some weak conditions are satisfied), we perform an in-depth analysis of the complexity of extensions of this logic. More precisely, we consider five natural and seemingly ``harmless'' extensions of ALC(D) and prove that, for all five extensions, reasoning is NExpTime-complete (again if some weak conditions are satisfied). Thus, we show that the PSpace upper bound for reasoning with ALC(D) cannot be considered robust w.r.t. extensions of the language.

Baris Sertkaya and Halit Oguztuzun. Proof of the Basic Theorem on Concept Lattices in Isabelle/HOL. In C. Aykanat, T. Dayar, and I. Korpeoglu, editors, Proceedings of the 19th International Symposium on Computer and Information Sciences (ISCIS2004), volume 3280 of Lecture Notes in Computer Science, pages 976–985. Springer, 2004.
Bibtex entry Paper (PS) Paper (PDF) ©Springer-Verlag

Abstract

This paper presents a machine-checked proof of the Basic Theorem on Concept Lattices, which appears in the book "Formal Concept Analysis" by Ganter and Wille, in the Isabelle/HOL Proof Assistant. As a by-product, the underlying lattice theory by Kammueller has been extended.

Anni-Yasmin Turhan and Christian Kissig. Sonic—Non-standard Inferences go OilEd. In D. Basin and M. Rusinowitch, editors, Proceedings of the 2nd International Joint Conference on Automated Reasoning (IJCAR'04), volume 3097 of Lecture Notes in Artificial Intelligence. Springer-Verlag, 2004.
Bibtex entry Paper (PS) Paper (PDF) ©Springer-Verlag

Abstract

SONIC (``Simple OilEd Non-standard Inference Component'') is the first prototype implementation of non-standard inferences for Description Logics usable via a graphical user interface. The contribution of our implementation is twofold: it extends an earlier implementation of the least common subsumer and of the approximation inference to number restrictions, and it offers these reasoning services via an extension of the graphical ontology editor OilEd.

Anni-Yasmin Turhan and Christian Kissig. Sonic—System Description. In Proceedings of the 2004 International Workshop on Description Logics (DL2004), CEUR-WS, 2004.
Bibtex entry Paper (PS) Paper (PDF)

Abstract

Back to the homepage of the Chair for Automata Theory.

Generated at Sat Feb 4 10:56:31 CET 2012.