The main focus of my research during the Graduiertenkolleg has been on
extending decision procedures, specially those used in Description Logics,
to allow for explanation and correction of unwanted consequences. Given a
consequence that one can deduce from a series of rules, or _axioms_, one
may be interested in finding the specific axioms that are responsible for
it. Furthermore, since there may be distinct combinations of axioms that
lead to the same consequences, one might be interested in finding all of
them. The approach used in my research consists on constructing a
so-called _pinpointing formula_. Informally, a pinpointing formula is a
compact representation of how the combination of axioms have an influence
on the presence or absense of the consequence being tested. In Description
Logics, the two main approaches for deciding a consequence are the
tableaux-based and the automata- based methods. I showed how one can
modify each of them in such a way that, instead of merely yield a yes/no
answer to the existence of the consequence, they give a pinpointing
formula for it. For the tableaux-based approach, I first needed to define
a general notion of a tableau algorithm, and then proceeded to describe
its _pinpointing extension_, showing that it actually computes the desired
formula. This technique brought out an inherent problem: the pinpointing
extension of a terminating tableaux-based algorithm may not terminate,
even for very special cases. It can be shown that it is actually
undecidable whether the pinpointing extension terminates. In trying to
solve this problem, a subclass of tableaux was defined, for which the
pinpointing extension is always terminating. For the automata-based
approach it was also necessary to define the correctness regarding
deciding properties. Once this was done, the automaton used was extended
to a weighted automaton whose behaviour was exactly the pinpointing
formula. Since the properties in DLs require infinite tree-models, it was
also necessary to develop an algorithm for computing the behaviour of
weighted automata on infinite trees using finite resources. The algorithm
found requires polynomial execution time, measured on the number of states
of the automaton. It was shown that this is optimal. I also analysed the
overhead in time and space resources associated with finding explanations,
in general, and a pinpointing formula in particular. For this, the
research focused on the tableaux-based algorithm for deciding subsumption
in EL, an inexpressive DL. The original decision algorithm requires
polynomial time and space, and hence any hardness results would yield
light on the additional resources required by explanation. It was shown
that finding one explanation (even the last-lexicographical one) has no
complexity overhead over deciding. Nonetheless, even deciding whether
there is an explanation of size smaller or equal to a given number n is
already NP-hard. Other kinds of complexity were also analysed. So, it was
shown that finding all the explanations requires time superpolynomial on
the size of the input and output combined (output complexity); that
counting the number of explanations is #P-hard (counting complexity), and
that the pinpointing formula can have length superpolynomial on the number
of axioms (monotone complexity), among others. Latest research has shown
that pinpointing can be useful for computing other kinds of values
depending on the axioms. Applications of this generalization include
rights management, fuzzy inferences, and weighted logics.
Penaloza, Rafael
Participated in the following conferences and workshops:
-The 2006 International Workshop on Description Logics (DL 2006). The Lake
District, UK. 2006. -The 2007 International Workshop on Description Logics
(DL 2007). Brixen/Bressanone, Italy. 2007. -The 30th German Conference on
Artificial Intelligence (KI 2007). Osnabrück, Germany. 2007. -The 16th
International Conference on Automated Reasoning with Analytic Tableaux and
Related Methods (TABLEAUX 2007). Aix-en-Provence, France. 2007. -The 2008
International Workshop on Description Logics (DL 2008). Dresden, Germany.
2008. -The 4th International Joint Conference on Automated Reasoning
(IJCAR 2008). Sydney, Australia. 2008.
Journal Publications:
-Axiom Pinpointing in General Tableaux (with Franz Baader)
Journal of Logic and Computation. 2008. To appear.
-Automata can Show PSpace Results for Description Logics (with Franz
Baader and Jan Hladik) Information and Computation, volume 206, Issue 9-10
(September 2008). pp 1045-1056.
Conference Proceedings Publications:
-Automata-Based Axiom Pinpointing (with Franz Baader)
Proceedings of IJCAR 2008. LNAI 5195. Springer, 2008.
-SI! Automata can Show PSpace Results for Description Logics (with Franz
Baader and Jan Hladik) Proceedings of LATA 2007. LNAI. Springer, 2007.
-Axiom Pinpointing in General Tableaux (with Franz Baader) Proceedings of
TABLEAUX 2007. LNAI. Springer, 2007. -Pinpointing in the Description Logic
EL+ (with Franz Baader and Boontawee Suntisrivaraporn) Proceedings of KI
2007. LNAI. Springer, 2007.
Workshop Proceedings Publications:
-Automata-based Pinpointing for DLs.
Proceedings of DL 2008. CEUR-WS, 2008.
-Blocking Automata for PSpace DLs (with Franz Baader and Jan Hladik)
Proceedings of DL 2007. CEUR-WS, 2007.
-Pinpointing in the Description Logic EL (with Franz Baader and Boontawee
Suntisrivaraporn) Proceedings of DL 2007. CEUR-WS, 2007. -PSpace Automata
for Description Logics (with Jan Hladik) Proceedings of DL 2006. CEUR-WS,
2006.