| Abstract: | We are investigating the problem of establishing computational rather than syntactic properties of forward-chaining rule-based expert systems. We model an expert system as a computation on working memory, define its execution semantics, and present proof techniques suitable for those semantics. Specifically, we model execution as a Dijkstra guarded-do construct, and use Dijkstra's Invariance Theorem and weakest precondition predicate transformers to establish invariants (safety properties) and postconditions (liveness properties). Our approach is an application of well-developed methods developed by Dijkstra and others for the verification of procedural programs. This paper introduces the approach, reports some initial results, and discusses future work. |
