Knowledge verification with an enhanced high-level Petri-Net model

We describe how to model rule-based systems using advanced Petri-net models in which variables and negation are exactly represented. We also explain how such models achieve knowledge verification. We explore the detection of improper knowledge, including redundancy, subsumption, conflicts, cycles, and unnecessary conditions, through reachability problems solved using an enhanced high-level Petri-net (Ehlpn) model. We assume that each rule describes an implication relation from a collection of conditions (left-hand side) to a collection of actions or conclusions (right hand side). Negative elements may appear in both the left- and right-hand sides. For convenience, we represent a variable in a rule by a string beginning with an uppercase letter, and a constant by a string beginning with a lowercase letter