Verification of Knowledge Bases: a Unifying Logical View.
Alon Y. Levy, Marie-Christine Rousset · 1997
: Notions of correctness and completeness of a KB are impossible to capture completely by a formal definition. However, when the knowledge base is represented in a declarative logical formalism, they can be approached by a logical analysis of its contents. A logical analysis of the knowledge base and constraints that are known to hold on the domain enables us to detect anomalies or discrepancies between the knowledge represented in the KB and the domain. This paper describes a unified logical framework for the verification problem of knowledge bases represented by logical rules (i.e., Horn rules and some extensions). We consider several instances of the verification problem, describe algorithms for verification, and establish the computational complexity of the verification problem. In particular, we consider the verification w.r.t. consistency constraints that are specified separately on the inputs and on the outputs. Next, we consider dependency constraints on the relations between i...