Verification of Knowledge-Based Reasoning Modules

摘要

A knowledge-based system is made up out of components, and with each componentgoes a world description (W). Verification of a knowledge-based system is verifying each component in turn. If all components check out then the knowledge-based system has been verified. The paper introduces a number of properties that can be attributed to a knowledge base (KB) in relation to W, and are interesting for verification. Some are familiar from the literature, such as correctness, consistency, and decisiveness, but others such as completeness, and well-informedness are not often described. The authors show that the usual approach to verification is to check for special cases of these more general notions. Besides what to verify, another important topic is how to discover these potential problems. For this, a tool has been developed within the formal specification language DESIRE (a framework for DEsign and Specification of Interacting REasoning modules) for compositional architectures of knowledge-based systems. This tool DES-CHECK performs some automatic verification and fixing of the errors that are described in this paper.