The Wayback Machine - https://web.archive.org/web/20120218092244/http://lat.inf.tu-dresden.de/research/papers-2001.html
Chair for Automata Theory of the Institute for Theoretical Computer Science, Faculty of Computer Science at TU Dresden

Publications

2001

 F. Baader, S. Brandt, and R. Küsters. Matching under Side Conditions in Description Logics. In B. Nebel, editor, Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence, IJCAI'01, pages 213–218, Seattle, Washington, 2001. Morgan Kaufmann.
Bibtex entry  Abstract

Abstract

Whereas matching in Description Logics is now relatively well-investigated, there are only very few formal results on matching under additional side conditions, though these side conditions were already present in the original paper by Borgida and McGuinness introducing matching in DLs. The present paper closes this gap for sublanguages of the DL ALN.

F. Baader, G. Brewka, and Th. Eiter, editors. KI 2001: Advances in Artificial Intelligence, Proceedings of the Joint German/Austrian Conference on AI (KI 2001), volume 2174 of Lecture Notes in Artificial Intelligence. Springer–Verlag, Vienna, Austria, 2001.
Bibtex entry

F. Baader and R. Küsters. Unification in a Description Logic with Transitive Closure of Roles. In R. Nieuwenhuis and A. Voronkov, editors, Proceedings of the 8th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2001), volume 2250 of Lecture Notes in Computer Science, pages 217–232, Havana, Cuba, 2001. Springer-Verlag.
Bibtex entry  Paper (PS)  ©Springer-Verlag

Abstract

Unification of concept descriptions was introduced by Baader and Narendran as a tool for detecting redundancies in knowledge bases. It was shown that unification in the small description logic FL0, which allows for conjunction, value restriction, and the top concept only, is already ExpTime-complete. The present paper shows that the complexity does not increase if one additionally allows for composition, union, and transitive closure of roles. It also shows that matching (which is polynomial in FL0) is PSpace-complete in the extended description logic. These results are proved via a reduction to linear equations over regular languages, which are then solved using automata. The obtained results are also of interest in formal language theory.

F. Baader and P. Narendran. Unification of Concepts Terms in Description Logics. J. Symbolic Computation, 31(3):277–305, 2001.
Bibtex entry  Free reprint

Abstract

Unification of concept terms is a new kind of inference problem for Description Logics, which extends the equivalence problem by allowing to replace certain concept names by concept terms before testing for equivalence. We show that this inference problem is of interest for applications, and present first decidability and complexity results for a small concept description language.

F. Baader and U. Sattler. An Overview of Tableau Algorithms for Description Logics. Studia Logica, 69:5–40, 2001.
Bibtex entry  Paper (PS)

Abstract

Description logics are a family of knowledge representation formalisms that are descended from semantic networks and frames via the system KL-ONE. During the last decade, it has been shown that the important reasoning problems (like subsumption and satisfiability) in a great variety of description logics can be decided using tableau-like algorithms. This is not very surprising since description logics have turned out to be closely related to propositional modal logics and logics of programs (such as propositional dynamic logic), for which tableau procedures have been quite successful.

Nevertheless, due to different underlying intuitions and applications, most description logics differ significantly from run-of-the-mill modal and program logics. Consequently, the research on tableau algorithms in description logics led to new techniques and results, which are, however, also of interest for modal logicians. In this article, we will focus on three features that play an important role in description logics (number restrictions, terminological axioms, and role constructors), and show how they can be taken into account by tableau algorithms.

F. Baader and K. Schulz. Combining Constraint Solving. In H. Comon, C. Marché, and R. Treinen, editors, Constraints in Computational Logics, volume 2002 of Lecture Notes in Computer Science. Springer–Verlag, 2001. See http://link.springer.de/link/service/series/0558/tocs/t2002.htm.
Bibtex entry  Paper (PS)

Abstract

In many areas of Logic, Computer Science, and Artificial Intelligence, there is a need for specialized formalisms and inference mechanisms to solve domain-specific tasks. For this reason, various methods and systems have been developed that allow for an efficient and adequate treatment of such restricted problems. In most realistic applications, however, one is faced with a complex combination of different problems, which means that a system tailored to solving a single problem can only be applied if it is possible to combine it both with other specialized systems and with general purpose systems.

F. Baader and W. Snyder. Unification Theory. In J.A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning, volume I, pages 447–533. Elsevier Science Publishers, 2001. See the handbook Web pages of Andrei Voronkov (http://www.cs.man.ac.uk/˜voronkov/handbook-ar/index.html) and Elsevier (http://www.elsevier.nl/locate/isbn/0444829490).
Bibtex entry  Paper (PS)  Free reprint

Abstract

This is the final version of a chapter on unification theory to appear in the Handbook of Automated Reasoning. The chapter is not intended to give a complete coverage of all the results. Instead we try to cover a number of significant topics in more detail. This should give a feeling for unification research and its methodology, provide the most important references, and enable the reader to study recent research papers on the topic.

F. Baader and S. Tobies. The Inverse Method Implements the Automata Approach for Modal Satisfiability. In Proceedings of the International Joint Conference on Automated Reasoning IJCAR'01, volume 2083 of Lecture Notes in Artificial Intelligence, pages 92–106. Springer-Verlag, 2001.
Bibtex entry  Paper (PS)  ©Springer-Verlag

Abstract

This paper ties together two distinct strands in automated reasoning: the tableau- and the automata-based approach. It shows that the inverse tableau method can be viewed as an implementation of the automata approach. This is of interest to automated deduction because Voronkov recently showed that the inverse method yields a viable decision procedure for the modal logic K.

F. Baader and A.-Y. Turhan. TBoxes do not yield a compact representation of least common subsumers. In Proceedings of the International Workshop in Description Logics 2001 (DL2001), Stanford, USA, August 2001.
Bibtex entry  Paper (PS)

Abstract

For Description Logics with existential restrictions, the size of the least common subsumer (lcs) of concept descriptions may grow exponentially in the size of the input descriptions. This paper investigates whether the possibly exponentially large concept description representing the lcs can always be represented in a more compact way when using an appropriate (acyclic) TBox for defining this description. This conjecture was supported by our experience in a chemical process engineering application. Nevertheless, it turns out that, in general, TBoxes cannot always be used to obtain a polynomial size representation of the lcs.

S. Brandt and A.-Y. Turhan. Using Non-standard Inferences in Description Logics — what does it buy me?. In Proceedings of the KI-2001 Workshop on Applications of Description Logics (KIDLWS'01), number 44 in CEUR-WS, Vienna, Austria, September 2001. RWTH Aachen. Proceedings online available from http://SunSITE.Informatik.RWTH-Aachen.DE/Publications/CEUR-WS/Vol-44/.
Bibtex entry  Paper (PS)

Abstract

In knowledge representation systems based on Description Logics, standard inference services such as consistency, subsumption, and instance are well-investigated. In contrast, non-standard inferences like most specific concept, least common subsumer, unification, and matching are missing in most systems---or exist only as ad-hoc implementations. We give an example of how these inferences can be applied successfully in the domain of process engineering. The benefit gained in our example, however, occurs in to many domains where knowledge bases are managed by persons with little expertise in knowledge engineering.

V. Haarslev, R. Möller, and A.-Y. Turhan. Exploiting Pseudo Models for TBox and ABox Reasoning in Expressive Description Logics. In Proceedings of the International Joint Conference on Automated Reasoning IJCAR'01, LNAI. Springer Verlag, 2001.
Bibtex entry  Paper (PS)  ©Springer-Verlag

Abstract

This paper investigates optimization techniques and data structures exploiting the use of so-called pseudo models. These techniques are applied to speed-up TBox and ABox reasoning for the description logics ALCNHR+ and ALC(D). The advances are demonstrated by an empirical analysis using the description logic system RACE that implements TBox and ABox reasoning for ALCNHR+.

U. Hatnik, T. Hinze, and M. Sturm. A Probabilistic Approach to Description of Molecular Biological Processes on DNA and Their Object Oriented Simulation. In V.V. Kluev and N.E. Mastorakis, editors, Proceedings WSES International Conference on Simulation (SIM2001), Malta, 2001.
Bibtex entry  Paper (PS)  Paper (PDF)

Abstract

Inspired by the potential of DNA based recombination techniques, we have analyzed processes used in DNA computing at the molecular level in laboratory studies with the aim to specify these processes as detailed as possible. Based on this knowledge, we have developed a simulation tool of real occurring molecular biological processes considering side effects. Side effects are described by appropriate statistical parameters. The comparison of simulation results with real observations in the laboratory shows a high degree of accordance. Using the simulation tool, prognoses about resulting DNA strands and influences of side effects to subsequent DNA operations can be obtained. The number of strand duplicates reflecting DNA concentrations is considered as an important factor for a detailed description of the DNA computing operations on the molecular level in the simulation. This property allows to evaluate the quantitative balance of DNA concentrations in a test tube. The simulation considers the DNA based reactions and processes synthesis, annealing, melting, union, ligation, digestion, labeling, polymerisation, affinity purification, and gel electrophoresis.

C. Hirsch and S. Tobies. A Tableau Algorithm for the Clique Guarded Fragment. In F. Wolter, H. Wansing, M. de Rijke, and M. Zakharyaschev, editors, Advances in Modal Logics Volume 3, Stanford, 2001. CSLI Publications.
Bibtex entry  Paper (PS)

Abstract

We describe a "modal style" tableau algorithm that decides satisfiability for the clique guarded fragment. As a corollary of constructions used to prove the correctness of the algorithm, we obtain a new proof for the generalised tree model property of the clique guarded fragment.

J. Hladik. Implementierung eines Entscheidungsverfahrens für das Bewachte Fragment der Prädikatenlogik. Diploma thesis, RWTH Aachen, Germany, 2001.
Bibtex entry  Paper (PS)

Abstract

In this thesis we present SAGA, an optimized implementation of a tableau algorithm for the Guarded Fragment of first order predicate logic. The empirical evaluation of this program with different sets of benchmark formulae shows that backjumping and semantic branching are crucial for most formulae, and blocking is efficient even when it is not required by the logic of the corresponding formula. Compared with other systems, the performance of SAGA is similar to that of tableau algorithms for logics in a lower complexity class.

I. Horrocks and U. Sattler. Ontology Reasoning in the SHOQ(D) Description Logic. In Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence, 2001.
Bibtex entry  Paper (PS)

Abstract

Ontologies are set to play a key role in the ``Semantic Web'' by providing a source of shared and precisely defined terms that can be used in descriptions of web resources. Reasoning over such descriptions will be essential if web resources are to be more accessible to automated processes. SHOQ(D) is an expressive description logic equipped with named individuals and concrete datatypes which has almost exactly the same expressive power as the latest web ontology languages (e.g., OIL and DAML). We present sound and complete reasoning services for this logic.

C. Lutz. Interval-based Temporal Reasoning with General TBoxes. In Bernhard Nebel, editor, Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence IJCAI-01, pages 89–94, Seattle, Washington, USA, 2001. Morgan-Kaufmann Publishers.
Bibtex entry  Paper (PS)

Abstract

Until now, interval-based temporal Description Logics (DLs) did---if at all---only admit TBoxes of a very restricted form, namely acyclic macro definitions. In this paper, we present a temporal DL that overcomes this deficieny and combines interval-based temporal reasoning with general TBoxes. We argue that this combination is very interesting for many application domains. An automata-based decision procedure is devised and a tight ExpTime-complexity bound is obtained. Since the presented logic can be viewed as being equipped with a concrete domain, our results can be seen from a different perspective: we show that there exist interesting concrete domains for which reasoning with general TBoxes is decidable.

C. Lutz. NExpTime-complete Description Logics with Concrete Domains. In Rajeev Goré, Alexander Leitsch, and Tobias Nipkow, editors, Proceedings of the International Joint Conference on Automated Reasoning, number 2083 in Lecture Notes in Artifical Intelligence, pages 45–60, Siena, Italy, 2001. Springer Verlag.
Bibtex entry  Paper (PS)

Abstract

Concrete domains are an extension of Description Logics (DLs) allowing to integrate reasoning about conceptual knowledge with reasoning about ``concrete properties'' of objects such as sizes, weights, and durations. It is known that reasoning with ALC(D), the basic DL admitting concrete domains, is PSpace-complete. In this paper, it is shown that the upper bound is not robust: we give three examples for seemingly harmless extensions of ALC(D)---namely acyclic TBoxes, inverse roles, and a role-forming concrete domain constructor---that make reasoning NExpTime-hard. As a corresponding upper bound, we show that reasoning with all three extensions together is in NExpTime.

C. Lutz and U. Sattler. The Complexity of Reasoning with Boolean Modal Logics. In Frank Wolter, Heinrich Wansing, Maarten de Rijke, and Michael Zakharyaschev, editors, Advances in Modal Logics Volume 3. CSLI Publications, Stanford, 2001.
Bibtex entry  Paper (PS)

Abstract

In this paper, we investigate the complexity of reasoning with various Boolean Modal Logics. The main results are that (i) adding negation of modal parameters to (multi-modal) K makes reasoning ExpTime-complete and (ii) adding atomic negation and conjunction to K even yields a NExpTime-complete logic. The last result is relativized by the fact that it depends on an infinite number of modal parameters to be available. If the number of modal parameters is bounded, full Boolean Modal Logic becomes ExpTime-complete.

C. Lutz, U. Sattler, and F. Wolter. Description Logics and the Two-Variable Fragment. In D.L. McGuiness, P.F. Pater-Schneider, C. Goble, and R. Möller, editors, Proceedings of the 2001 International Workshop in Description Logics (DL-2001), pages 66–75, Stanford, California, USA, 2001. Proceedings online available from http://SunSITE.Informatik.RWTH-Aachen.DE/Publications/CEUR-WS/.
Bibtex entry  Paper (PS)

Abstract

We present a description logic L that is as expressive as the two-variable fragment of first-order logic and differs from other logics with this property in that it encompasses solely standard role- and concept-forming operators. The description logic L is obtained from ALC by adding full Boolean operators on roles, the inverse operator on roles and an identity role. It is proved that L has the same expressive power as the two-variable fragment FO^2 of first-order logic by presenting a translation from FO^2-formulae into equivalent L-concepts (and back). Additionally, we discuss an interesting complexity phenomenon: both L and FO^2 are NExpTime-complete and so is the restriction of FO^2 to finitely many relation symbols; astonishingly, the restriction of L to a bounded number of role names is in ExpTime.

C. Lutz, U. Sattler, and F. Wolter. Modal Logics and the two-variable fragment. In Annual Conference of the European Association for Computer Science Logic CSL'01, LNCS, Paris, France, 2001. Springer Verlag.
Bibtex entry  Paper (PS)

Abstract

We introduce a modal language L which is obtained from standard modal logic by adding the Boolean operators on accessibility relations, the identity relation, and the converse of relations. It is proved that L has the same expressive power as the two-variable fragment FO2 of first-order logic, but speaks less succinctly about relational structures: if the number of relations is bounded, then L-satisfiability is ExpTime-complete but FO2 satisfiability is NExpTime-complete. We indicate that the relation between L and FO2 provides a general framework for comparing modal and temporal languages with first-order languages.

C. Lutz, H. Sturm, F. Wolter, and M. Zakharyaschev. Tableaux for Temporal Description Logic with Constant Domain. In Rajeev Goré, Alexander Leitsch, and Tobias Nipkow, editors, Proceedings of the International Joint Conference on Automated Reasoning, number 2083 in Lecture Notes in Artifical Intelligence, pages 121–136, Siena, Italy, 2001. Springer Verlag.
Bibtex entry  Paper (PS)

Abstract

We show how to combine the standard tableau system for the basic description logic ALC and Wolper's tableau calculus for propositional temporal logic PTL (with the temporal operators `next-time' and `until') in order to design a terminating sound and complete tableau-based satisfiability-checking algorithm for the temporal description logic PTL_ALC interpreted in models with constant domains. We use the method of quasimodels to represent models with infinite domains, and the technique of minimal types to maintain these domains constant. The combination is flexible and can be extended to more expressive description logics or even to decidable fragments of first-order temporal logics.

U. Sattler and M. Y. Vardi. The Hybrid mu-Calculus. In R. Goré, A. Leitsch, and T. Nipkow, editors, Proceedings of the International Joint Conference on Automated Reasoning, volume 2083 of LNAI, pages 76–91. Springer Verlag, 2001.
Bibtex entry  Paper (PS)

Abstract

In the last years, several decision procedures for ExpTime-complete modal/description/dynamic logics were implemented and proved to behave well in practice. Due to its high expressive power, the full mu-calculus (including converse programs) is one of the ``queens'' of ExpTime modal/description/dynamic logics. However, it lacks two features important in many applications: nominals to refer to named individuals, and a universal program for the internalisation of general axioms. We present an ExpTime decision procedure for the full mu-Calculus extended with nominals and a universal program, thus creating a new, more expressive ``queen'' logic. The decision procedure is based on tree automata, and makes explicit the problems caused by nominals and how to overcome them. Roughly speaking, we show how to reason in a logic lacking the tree model property using techniques for logics with the tree model property. Hence the contribution of the paper is two-fold: we extend the choice of ExpTime logics an implementer can choose from, and we present a technique to reason in the presence of nominals.

E.P. Stoschek, M. Sturm, and T. Hinze. DNA-Computing - ein funktionales Modell im laborpraktischen Experiment. Informatik Forschung und Entwicklung, 16(1):35–52, 2001.
Bibtex entry  Paper (PDF)  ©Springer-Verlag

Abstract

Im Zentrum der Betrachtungen zum DNA-Computing steht die Frage nach den Chancen und Grenzen dieses neuen Berechnungsmodells, nachdem in den letzten Jahren eine rasante Entwicklung auf das Thema aufmerksam machte. Neben beachtlichen theoretischen Untersuchungen zum "Rechnen im Reagenzglas" werden auch laborpraktische Implementierungen favorisiert. An der TU Dresden wurde in interdisziplinärer Arbeit ein Integer-Rucksackproblem mittels eines DNA-Algorithmus im Labor gelöst und dabei eine Vielzahl molekularbiologischer Operationen analysiert. Mithilfe dieses Satzes von Operationen gelang eine universelle und labornahe Modellierung des DNA-Computing. Hierbei angewandte Techniken und Methoden werden vorgestellt und bewertet. Die Beschreibung des DNA-Algorithmus zeigt, wie sich Einzeloperationen vorteilhaft zu Operationsfolgen zusammensetzen lassen und gemeinsam mit einer geeigneten DNA-Kodierung der Eingangsdaten zur Lösung des Problems im Labor führen. Erstmalig wurden hierbei natürliche Zahlen verarbeitet. Die Arbeitsgemeinschaft DNA-Computing Dresden konzentriert sich auf Aufgabenstellungen, die formale Modelle des DNA-Computing mit überzeugenden Laborimplementierungen verbinden.

M. Sturm and T. Hinze. Distributed Splicing of RE with 6 Test Tubes. Romanian Journal of Information Science and Technology, 4(1-2):211–234, 2001.
Bibtex entry  Paper (PS)  Paper (PDF)

Abstract

This paper introduces a functional approach to distributed splicing systems for generation of recursive enumerable languages with 6 test tubes. The specification of this system serves both, the formal mathematical and the lab-experimental aspect. The implementation of the splicing system using a functional description of laboratory operations supports particularly the last-mentioned aspect. Advantages of this approach consist in large experimental practicability as well as in the independence of certain Chomsky type 0 grammar parameters.

M. Sturm and T. Hinze. Verfahren zur Ausführung von mathematischen Operationen mittels eines DNA-Computers und DNA-Computer hierzu. Anmeldung als Deutsches Patent, Aktenzeichen 10159886.6, Deutsches Patentamt München, 2001.
Bibtex entry

Stephan Tobies. PSPACE Reasoning for Graded Modal Logics. Journal of Logic and Computation, 11(1):85–106, 2001.
Bibtex entry  Paper (PS)

Abstract

We present a PSPACE algorithm that decides satisfiability of the graded modal logic Gr(K_R) - a natural extension of propositional modal logic K_R by counting expressions - which plays an important role in the area of knowledge representation. The algorithm employs a tableaux approach and is the first known algorithm which meets the lower bound for the complexity of the problem. Thus, we exactly fix the complexity of the problem and refute a EXPTIME-hardness conjecture. We extend the results to the logic Gr(K_{R_\cap^{-1}}), which augments Gr(K_R) with inverse relations and intersection of accessibility relations. This establishes a kind of ``theoretical benchmark'' that all algorithmic approaches can be measured against.

A.-Y. Turhan and R. Molitor. Using lazy unfolding for the computation of least common subsumers. In Proceedings of the International Workshop in Description Logics 2001 (DL2001), Stanford, USA, August 2001.
Bibtex entry  Paper (PS)

Abstract

For description logics with existential restrictions, the size of the least common subsumer (lcs) of concept descriptions may grow exponentially in the size of the concept descriptions. To reduce the size of the output descriptions and the run-time of the lcs algorithm we present an optimized algorithm for computing the lcs in ALE using lazy unfolding. A first evaluation of the performance of the naive algorithm in comparison to the performance of the algorithm using lazy unfolding indicates a performance gain for both concept sizes as well as run-times.

home Back to the homepage of the Chair for Automata Theory.
Generated at Thu Feb 16 10:00:02 CET 2012.
close