Formal verification of some potential contradictions in knowledge base using a high level net approach

摘要

With increasingly complex, sophisticated and changeable real-world domains, knowledge based systems have to cope with the problems of maintaining the consistency and the integrity of their knowledge bases. It is becoming increasingly important that knowledge base be formally verified. This article describes a formal technique based on the state transition model for verifying some potential contradictions in rule-based systems. The approach emphasizes the detection, and identification of different anomalies relevant to such problems that could occur in sequences of inferences. A description of the problems in terms of predicate formulae for verification is given. Formal analysis is provided which is based on reachability markings generated by transition firings in the Petri network. A discussion on the complexity of the methodology is given.