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 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 it can be shown that certain constraints always hold between the inputs and the outputs. We consider the knowledge base verification problem for Horn rule knowledge bases and for three kinds of constraints: 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 decidable. In the third case, we show that the problem is, in general, undecidable, and we identify two decidable cases. In our analysis we show how the properties of the problem vary depending on the presence of recursion in the Horn rules, the presence of the interpreted predicates =, ⩽, < 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 containment, studied in the database literature. This connection also provides novel algorithms for the knowledge base verification problem. Finally, we provide the first algorithm for verifying hybrid knowledge bases that combine the expressive power of Horn rules and the description logicALCNR.