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.