Alon Y. Levy , Marie-Christine Rousset , Verification of Knowledge Bases using Containment Checking Proceedings of the AAAI Thirteenth National Conference on Artificial Intelligence 1996
Abstract: Building complex knowledge based applications requires encoding large
amounts of domain knowledge. After acquiring knowledge from domain
experts, much of the effort in building a knowledge base goes into
verifying that the knowledge is encoded correctly.
A knowledge base is
verified if for any correct set of inputs (i.e., problem
instance), the knowledge base entails correct outputs. The
correctness of the inputs and outputs is defined w.r.t. constraints
that are known to hold in the domain.
We consider the problem of
verifying hybrid knowledge bases that contain both Horn rules and a
terminology in a description logic. Our approach to the verification
problem is based on showing a close relationship to the problem of
query containment. Our first contribution, based on this
relationship, is presenting a thorough analysis of the decidability
and complexity of the verification problem, for knowledge bases
containing recursive rules and the interpreted predicates $=$, $\leq$,
$<$ and $\not =$. Second, we show that important
new classes of constraints on correct inputs and outputs can be
expressed in a hybrid setting, in which a description logic class
hierarchy is also considered, and we present the first complete
algorithm for verifying such hybrid knowledge bases.