Formal description and verification of knowledge base redundancyand subsumption

摘要

With increasingly complex, sophisticated and changeable real-worldndomains, knowledge based systems have to cope with the problems of truthnmaintenance of their knowledge bases. This paper initiates a formalndescription technique for verifying the redundancy and subsumption ofnproduction rule-based systems. It has its foundation on high level Petrinnets. The approach emphasizes the detection, and identification ofndifferent anomalies relevant to such problems that could occur innsequences of inferences. A description of the problems in terms ofnpredicate formulae for verification is given. Formal analysis isnprovided which is based on reachability markings generated by thentransition firings in the Petri network