KJ3-a tool for proving formal specifications of rule-based expert systems

KJ3 is the first system which incorporates theorem proving techniques with the Petri Net description scheme for knowledge validation of rule based systems (RBSs). By converting the validation tasks of RBSs to reachability problems of Enhanced High-level Petri Net (EHLPN), KJ3 performs validation by proving if the hypothetical reachability problem is true. The establishment of the hypothesis corresponds to the achievement of the validation tasks. Since the properties of RBSs, such as refraction, conservation of facts, variables, closed world assumption, and negative information, can be properly represented and handled by EHLPN, different types of RBSs can be processed in KJ3. Since checking user specifications becomes investigating the reachability problems of EHLPN, all types of validation tasks can be handled by KJ3. The validation results can be directly extracted from the inference process to allow the users to explain the validation results. The inference process is mathematically traceable, sound, and complete, KJ3 guarantees that the validation outcome is reliable