Formal verification of some potential contradictions in hybrid expert systems

With increasingly complex, sophisticated and changing real-world situations, it has been recognized that expert systems which combine one or more techniques greatly increase the problem solving capability and help overcome some of the shortcomings associated with any single technique. The verification of these expert systems requires methods that could tackle the multiple knowledge representation paradigms and integrated inference mechanisms used. This paper describes a formal technique based on State Controlled Coloured Petri Nets (SCCPNs) for verifying some potential contradictions in Hybrid Expert Systems (HES) that emphasize an integration of object hierarchy, property inheritance and production rules. The main idea of our approach is to convert the HES into a State Controlled Coloured Petri Net where the object hierarchy, property inheritance and production rules are modelled as separated components in the same SCCPN. The detection and analysis of the potential contradictions in the system are done by constructing and examining the reachability tree spanned by the knowledge inference. Propositions are formulated to verify such potential contradictions, and their mathematical proofs are explained.