Automated Reasoning with Boolean ABoxes
Bernadette MartÃnez HernÃ¡ndez
Abstract:
Description Logics (DL) is a family of knowledge representation (KR)
formalisms tailored to represent the knowledge of an application
domain by first defining the basic and derived concepts of the domain,
and then using these concepts to specify properties of objects and
individuals in the domain. Therefore a DL knowledge base (KB) is made
up of two parts, the terminological part (TBox) where the definitions
of the basic and derived notions are stored, and the assertional part
(ABox), which records facts about individuals.
A common property of a group of individuals is described by a
concept. Concepts can be considered as unary predicates and
interpreted as sets of objects. Roles are interpreted as binary
relations between objects. Thus, an ABox resembles superficially a
relational database with only unary and binary relations. However a
database represents only one interpretation, while an ABox encodes a
set of interpretations, namely all its models. The ABox does not
assume its information to be complete, but in a database the absence
of information is regarded as negative information. The partial
knowledge of an ABox comes out not only from lack of information, but
also from disjunctive assertions like i:C |_| D.
Such possibility of partial knowledge is very restricted, it only
allows conjunction of assertions. A less restricted representation is
usually needed to deal with interesting problems as planning and
diagnosis. To be useful it would have to have good expressivity to
describe partial knowledge by means of disjunctions or boolean
constraints.
One way to tackle this problem is to use the Boolean ABoxes (BABoxes),
in which boolean combinations of ABox assertions are permitted. Given
a TBox T and a BABox B, to find whether (T;B) has a model we treat all
the assertions of the BABox as propositions. Then, all the
propositional models, which are ABoxes, can be obtained. If one of
these models A, together with T has a model; then (T;B) has a
model. This process may be expensive because of the exhaustive
search. Therefore, a suitable translation from BABox to a regular KB
could make it better.
In [ABM02] such translation has been proposed. However it is not clear
if this translation is really more effcient than an optimized method
which tries out all propositional models. The research reported in
this thesis was done in order to clarify this issue.
Our main results are that the translation approach is an adequate
option for BABoxes containing propositionally non trivial information,
specifically when the BABoxes are modally constrained. We give
examples of DL's in which the translation approach is always needed.
Our work has several important consequences. We created a number of
examples which turned out to be revealing. They showed several
mistakes in RACER. We developed several optimizations to both the
translation and the model generation approach. Furthermore we created
a random generator of test examples.
Chapter 2 is a short introduction to Description Logics. Boolean
ABoxes are defined here as well. The two main approaches to check the
consistency of Boolean ABoxes, their algorithms and their
optimizations are described in Chapter 3. The last chapter contains
the description of the implementations of these algorithms, the
testing and the description of the random generator of test sets. In
Appendix A we include the code of the algorithms and in Appendix B we
can find the formulation of some puzzles that were part of the
preliminary test of the implementations.