Chair for Automata Theory
of the Institute for Theoretical Computer Science,
Faculty of Computer Science at
TU Dresden
Technical Reports
2006
Franz Baader and Alexander Okhotin.
On Language Equations with One-sided Concatenation.
LTCS-Report 06-01, Chair for Automata Theory, Institute for Theoretical
Computer Science, Dresden University of Technology, Germany, 2006.
See http://lat.inf.tu-dresden.de/research/reports.html.
Bibtex entry Abstract
Paper (PS) Paper (PDF)
Abstract
Language equations are equations where both the constants occurring in the
equations and the solutions are formal languages. They have first
been introduced in formal language theory, but are now also considered in
other areas of computer science. In the present paper, we restrict the attention
to language equations with one-sided concatenation, but in contrast to previous
work on these equations, we allow not just union but all Boolean operations
to be used when formulating them. In addition, we are not just interested in deciding
solvability of such equations, but also in deciding other properties of the
set of solutions, like its cardinality (finite, infinite, uncountable)
and whether it contains least/greatest solutions. We show that all these
decision problems are ExpTime-complete.
Franz Baader, Bernhard Ganter, Ulrike Sattler, and Baris Sertkaya.
Completing Description Logic Knowledge Bases using Formal Concept
Analysis.
LTCS-Report 06-02, Chair for Automata Theory, Institute for Theoretical
Computer Science, Dresden University of Technology, Germany, 2006.
See http://lat.inf.tu-dresden.de/research/reports.html.
Bibtex entry Paper (PS) Paper (PDF)
Abstract
We propose an approach for extending both the terminological and the
assertional part of a Description Logic knowledge base by using information
provided by the assertional part and by a domain expert. The use of techniques from
Formal Concept Analysis ensures that, on the one hand, the interaction with the
expert is kept to a minimum, and, on the other hand, we can show
that the extended knowledge base is complete in a certain sense.
H. Liu, C. Lutz, M. Milicic, and F. Wolter.
Description Logic Actions with general TBoxes: a Pragmatic
Approach.
LTCS-Report 06-03, Chair for Automata Theory, Institute for Theoretical
Computer Science, Dresden University of Technology, Germany, 2006.
See http://lat.inf.tu-dresden.de/research/reports.html.
Bibtex entry Paper (PDF)
Abstract
Action formalisms based on description logics (DLs) have recently
been introduced as decidable fragments of well-established action
theories such as the Situation Calculus and the Fluent Calculus.
However, existing DL action formalisms fail to include general
TBoxes as provided by almost all state-of-the-art description
logics. We define a DL action formalism that admits general TBoxes,
propose a pragmatic approach to addressing the ramification problem
that is introduced in this way, show that our formalim is decidable
and perform a detailed investigation of its computational
complexity.
F. Baader, J. Hladik, and R. Penaloza.
PSPACE Automata with Blocking for Description Logics.
LTCS-Report 06-04, Chair for Automata Theory, Institute for Theoretical
Computer Science, Dresden University of Technology, Germany, 2006.
See http://lat.inf.tu-dresden.de/research/reports.html.
Bibtex entry Paper (PDF)
Abstract
In Description Logics (DLs), both tableau-based and automata-based
algorithms are frequently used to show decidability and complexity results
for basic inference problems such as satisfiability of concepts. Whereas
tableau-based algorithms usually yield worst-case optimal algorithms in the
case of PSPACE-complete logics, it is often very hard to design optimal
tableau-based algorithms for EXPTIME-complete DLs. In contrast, the
automata-based approach is usually well-suited to prove EXPTIME
upper-bounds, but its direct application will usually also yield an
EXPTIME-algorithm for a PSPACE-complete logic since the (tree) automaton
constructed for a given concept is usually exponentially large. In the
present paper, we formulate conditions under which an on-the-fly
construction of such an exponentially large automaton can be used to obtain
a PSPACE-algorithm. We illustrate the usefulness of this approach by
proving a new PSPACE upper-bound for satisfiability of concepts w.r.t.
acyclic terminologies in the DL SI, which extends the basic DL ALC with
transitive and inverse roles.
Rafael Penaloza.
Pinpointing in Tableaus.
LTCS-Report 06-05, Chair for Automata Theory, Institute for Theoretical
Computer Science, Dresden University of Technology, Germany, 2006.
See http://lat.inf.tu-dresden.de/research/reports.html.
Bibtex entry Paper (PS) Paper (PDF)
Abstract
Tableau-based decision procedures have been successfully used for solving a wide variety of problems. For some applications, nonetheless, it is desirable not only to obtain a Boolean answer, but also to detect the causes for such a result. In this report, a method for finding explanations on tableau-based procedures is explored, generalizing previous results on the field. The importance and use of the method is shown by means of examples.
There is also a complete overview of our technical reports.
Back to the homepage of the Chair for Automata Theory.
Generated at Fri Jun 12 11:21:13 CEST 2009.