Chair for Automata Theory
of the Institute for Theoretical Computer Science,
Faculty of Computer Science at
TU Dresden
Technical Reports
2008
Franz Baader, Silvio Ghilardi, and Carsten Lutz.
LTL over Description Logic Axioms.
LTCS-Report 08-01, Chair for Automata Theory, Institute for Theoretical
Computer Science, Dresden University of Technology, Germany, 2008.
See http://lat.inf.tu-dresden.de/research/reports.html.
Bibtex entry Paper (PS) Paper (PDF)
Abstract
Most of the research on temporalized Description Logics (DLs)
has concentrated on the case where temporal operators can occur
within DL concept descriptions.
In this setting, reasoning usually becomes quite hard if rigid roles,
i.e., roles whose interpretation does not change over time, are available.
In this paper, we consider the case where temporal operators are
allowed to occur only in front of DL axioms (i.e., ABox assertions
and general concept inclusion axioms), but not inside of concepts descriptions.
As the temporal component, we use linear temporal logic (LTL) and in
the DL component we consider the basic DL ALC.
We show that reasoning in the presence of rigid roles becomes considerably
simpler in this setting.
Franz Baader and Rafael Peñaloza.
Blocking and Pinpointing in Forest Tableaux.
LTCS-Report 08-02, Chair for Automata Theory, Institute for Theoretical
Computer Science, Dresden University of Technology, Germany, 2008.
See http://lat.inf.tu-dresden.de/research/reports.html.
Bibtex entry Paper (PS) Paper (PDF)
Abstract
Axiom pinpointing has been introduced in Description Logics (DLs) to help the used understand the reasons why consequences hold by computing minimal subsets of the knowledge base that have the consequence in consideration.
Several pinpointing algorithms have been described as extensions of the standard tableau-based reasoning algorithms for deciding consequences from DL knowledge bases.
Although these extensions are based on similar ideas, they are all introduced for a particular tableau-based algorithm for a particular DL, using specific traits of them.
In the past, we have developed a general approach for extending tableau-based algorithms into pinpointing algorithms.
In this paper we explore some issues of termination of general tableaux and their pinpointing extensions.
We also define a subclass of tableaux that allows the use of so-called blocking conditions, which stop the execution of the algorithm once a pattern is found, and adapt the pinpointing extensions accordingly, guaranteeing its correctness and termination.
Franz Baader and Rafael Peñaloza.
Pinpointing in Terminating Forest Tableaux.
LTCS-Report 08-03, Chair for Automata Theory, Institute for Theoretical
Computer Science, Dresden University of Technology, Germany, 2008.
See http://lat.inf.tu-dresden.de/research/reports.html.
Bibtex entry Paper (PS) Paper (PDF)
Abstract
Axiom pinpointing has been introduced in description logics (DLs) to help
the user to understand the reasons why consequences hold and to
remove unwanted consequences by computing minimal (maximal) subsets of
the knowledge base that have (do not have) the consequence in question.
The pinpointing algorithms described in the DL literature are obtained as extensions
of the standard tableau-based reasoning algorithms for computing consequences from DL
knowledge bases. Although these extensions are based on similar ideas,
they are all introduced for a particular tableau-based algorithm for a
particular DL.
The purpose of this paper is to develop a general approach for
extending a tableau-based algorithm to a pinpointing algorithm. This approach
is based on a general definition of ``tableau algorithms,'' which captures
many of the known tableau-based algorithms employed in DLs, but also
other kinds of reasoning procedures.
Felix Distel.
Model-based Most Specific Concepts in Description Logics with Value
Restrictions.
LTCS-Report 08-04, Institute for theoretical computer science, TU Dresden,
Dresden, Germany, 2008.
http://lat.inf.tu-dresden.de/research/reports.html.
Bibtex
entry Abstract
Paper
(PS) Paper
(PDF)
Abstract
Non-standard inferences are particularly useful in the bottom-up construction of
ontologies in Description Logics. One of the more common non-standard reasoning
tasks is the most specific concept (msc) for an ABox-individual.
In this paper we present similar non-standard reasoning task: model-based
most specific concepts (model-mscs). We show that, although they
look similar to ABox-mscs their computational behaviour can be different.
We present constructions for model-mscs in the logics \ensuremath{\mathcal{FLO}}
and \ensuremath{\mathcal{FLE}}
with cyclic TBoxes and for \ensuremath{\mathcal{ALC}^{\cup\ast}} with acyclic
TBoxes. Since subsumption in \ensuremath{\mathcal{FLE}} with cyclic TBoxes has not been
examined previously, we present a characterization of subsumption
and give a construction for the least common subsumer in this setting.
Franz Baader and Felix Distel.
Exploring finite models in the Description Logic
EL_gfp.
LTCS-Report 08-05, Institute for Theoretical Computer Science, TU Dresden,
Dresden, 2008.
See http://lat.inf.tu-dresden.de/research/reports.html.
Bibtex entry Paper (PS) Paper (PDF)
Abstract
In a previous ICFCA paper we have shown that, in the Description
Logics EL and ELgfp, the set of general concept inclusions
holding in a finite model always has a finite basis. In this paper,
we address the problem of how to compute this basis efficiently,
by adapting methods from formal concept analysis.
Baris Sertkaya.
Some Computational Problems Related to Pseudo-intents.
LTCS-Report 08-06, Chair for Automata Theory, Institute for Theoretical
Computer Science, Dresden University of Technology, Germany, 2008.
See http://lat.inf.tu-dresden.de/research/reports.html.
Bibtex
entry Abstract
Paper (PS) Paper
(PDF)
Abstract
We investigate the computational complexity of several decision, enumeration
and counting problems related to pseudo-intents. We show that given a
formal context and a set of its pseudo-intents, checking
whether this context has an additional pseudo-intent
is in coNP and it is at least as hard as checking whether a given simple
hypergraph is saturated.
We also show that recognizing the set of pseudo-intents
is also in coNP and it is at least as hard as checking whether a given
hypergraph is the transversal hypergraph of another given hypergraph.
Moreover, we show that if any of these two problems turns out to be coNP-hard,
then unless P = NP, pseudo-intents cannot be enumerated in output
polynomial time.
We also investigate the complexity of finding
subsets of a given Duquenne-Guigues Base from which a given implication follows.
We show that checking the existence of such a subset within a specified
cardinality bound is NP-complete, and counting all such minimal subsets is
#P-complete.
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.