Proving properties of rule-based systems

Abstract

A deductive method is applied to the validation of rule-based systems. A number of validation tasks, including the detection of errors or anomalies, the proof of termination, the verification of properties, and the generation of test cases, are all translated into conjectures. If the conjectures in an appropriate system theory are proved, the corresponding validation task is accomplished. The method applies to nonmonotonic rule systems, which may delete elements from working memory, as well as monotonic ones, which do not. Validation conjectures are proved or disproved in a new theorem-proving system, SNARK, which has facilities for reasoning in first-order theories with mathematical induction. The system has already been applied to establish properties of a number of simple rule-based systems.< <ETX xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">&gt;</ETX>