VERIFICATION OF KNOWLEDGE BASES BASED ON CONTAINMENT CHECKING

Building complex knowledge based applications requires encoding large amounts of domain knowledge. After acquiring knowledge from domain exp erts, much of the effort in building a knowledge base goes into verify ing that the knowledge is encoded correctly. A knowledge base is verif ied if it can be shown that certain constraints always hold between th e inputs and the outputs. We consider the knowledge base verification problem for Horn rule knowledge bases and for three kinds of constrain ts: I/O consistency constraints, I/O dependency constraints, and input completeness constraints. For the first two cases, we establish tight complexity results on the problem, and show in what cases it is decid able. In the third case, we show that the problem is, in general, unde cidable, and we identify two decidable cases. In our analysis we show how the properties of the problem vary depending on the presence of re cursion in the Horn rules, the presence of the interpreted predicates =, less than or equal to, < and =, and the presence of negation in the antecedents of the rules. Our approach to the verification problem is based on showing a close relationship to the problem of query contain ment, studied in the database literature. This connection also provide s novel algorithms for the knowledge base verification problem. Finall y, we provide the first algorithm for verifying hybrid knowledge bases that combine the expressive power of Horn rules and the description l ogic ALCNR. (C) 1998 Published by Elsevier B.V. All rights reserved.