Formal description and verification of knowledge base redundancy and subsumption

With increasingly complex, sophisticated and changeable real-world domains, knowledge based systems have to cope with the problems of truth maintenance of their knowledge bases. This paper initiates a formal description technique for verifying the redundancy and subsumption of production rule-based systems. It has its foundation on high level Petri nets. 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 the transition firings in the Petri network