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

Technical Reports

2003

 F. Baader. The Instance Problem and the Most Specific Concept in the Description Logic w.r.t. Terminological Cycles with Descriptive Semantics. LTCS-Report 03-01, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2003. See http://lat.inf.tu-dresden.de/research/reports.html.
Bibtex entry  Paper (PS)

Abstract

and non-standard inferences in the presence of terminological cycles for the description logic EL, which allows for conjunctions, existential restrictions, and the top concept. Regarding standard inference problems, it was shown there that the subsumption problem remains polynomial for all three types of semantics usually considered for cyclic definitions in description logics, and that the instance problem remains polynomial for greatest fixpoint semantics. Regarding non-standard inference problems, it was shown that, w.r.t. greatest fixpoint semantics, the least common subsumer and the most specific concept always exist and can be computed in polynomial time, and that, w.r.t. descriptive semantics, the least common subsumer need not exist. The present report is concerned with two problems left open by this previous work, namely the instance problem and the problem of computing most specific concepts w.r.t. descriptive semantics, which is the usual first-order semantics for description logics. We will show that the instance problem is polynomial also in this context. Similar to the case of the least common subsumer, the most specific concept w.r.t. descriptive semantics need not exist, but we are able to characterize the cases in which it exists and give a decidable sufficient condition for the existence of the most specific concept. Under this condition, it can be computed in polynomial time.

S. Brandt, A.-Y. Turhan, and R. Küsters. Foundations of non-standard Inferences for Description Logics with transitive Roles and Role Hierarchies. LTCS-Report 03-02, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2003.
Bibtex entry  Paper (PS)

Abstract

Description Logics (DLs) are a family of knowledge representation formalisms used for terminological reasoning. They have a wide range of applications such as medical knowledge-bases, or the semantic web. Research on DLs has been focused on the development of sound and complete inference algorithms to decide satisfiability and subsumption for increasingly expressive DLs. Non-standard inferences are a group of relatively new inference services which provide reasoning support for the building, maintaining, and deployment of DL knowledge-bases. So far, non-standard inferences are not available for very expressive DLs. In this paper we present first results on non-standard inferences for DLs with transitive roles. As a basis, we give a structural characterization of subsumption for DLs where existential and value restrictions can be imposed on transitive roles. We propose sound and complete algorithms to compute the least common subsumer (lcs).

B. Morawska. Completness of E-unification with eager Variable Elimination. LTCS-Report 03-03, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2003. See http://lat.inf.tu-dresden.de/research/reports.html.
Bibtex entry  Paper (PS)

Abstract

The report contains a proof of completeness of a goal-directed inference system for general $E$-unification with eager Variable Elimination. The proof is based on an analysis of a concept of ground, equational proof. The theory of equational proofs is developed in the first part. Solving variables in a goal is then shown to be reflected in defined transformations of an equational proof. The termination of these transformations proves termination of inferences with eager Variable Elimination.

C. Lutz and D. Walther. PDL with Negation of Atomic Programs. LTCS-Report 03-04, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2003. See http://lat.inf.tu-dresden.de/research/reports.html.
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, 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.

F. Baader, Silvio Ghilardi, and Cesare Tinelli. A New Combination Procedure for the Word Problem that Generalizes Fusion Decidability Results in Modal Logics. LTCS-Report 03-05, Chair for Automata Theory, Institute for Theoretical Computer Science, Dresden University of Technology, Germany, 2003. See http://lat.inf.tu-dresden.de/research/reports.html.
Bibtex entry  Paper (PS)

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.

There is also a complete overview of our technical reports.
home Back to the homepage of the Chair for Automata Theory.
Generated at Fri Jun 12 11:21:13 CEST 2009.