PROVING PROPERTIES OF RULE-BASED SYSTEMS

Rule-based systems are being applied to tasks of increasing responsibility. Deductive methods are being applied to their validation, to detect flaws in these systems and to enable us to use them with more confidence. Each system of rules is encoded as a set of axioms that define the system theory. The operation of the rule language and information about the subject domain are also described in the system theory. Validation tasks, such as establishing termination, unreachability, or consistency, or verifying properties of the system, are all phrased as conjectures. If we succeed in establishing the validity of the conjecture in the system theory, we have carried out the corresponding validation task. If the proof is restricted to be sufficiently constructive, we may extract from it information other than a simple yes/no answer. For example, we may obtain a description of a situation in which an error or anomaly may occur. A method for the gradual formulation of specifications based on the attempted proof of a series of conjectures has been found to be suitable for rule-based systems. Such a specification can serve as the basis for a reengineering of the system using conventional software technology. Validation conjectures are proved or disproved by a new theorem-proving system, SNARK, which implements (nonclausal) resolution and paramodulation, an optional constructive restriction, and some facilities for proof by induction. The system has already been applied to prove properties of a number of simple rule-based systems.