ROSE F. GAMBLE
This research was supported in part by DOE contract# DEAC22–93B-C14894.
Department of Mathematical and Computer Sciences University of Tulsa, 600 South College Avenue Tulsa, OK 74104–3189, USA
TERESA M. SHAFT
Department of Quantitative Methods and Management Information Systems University of Tulsa, 600 South College Avenue Tulsa, OK 74104–3189, USA

Received 19 August 1994
Revised 16 February 1996
Accepted 1 June 1996

The reliability of knowledge-based systems (KBSs) has been the subject of a great deal of recent research. Much of this research focuses on the verification of KBSs, specifically to eliminate redundant rules, conflicting rules, and to ensure that the KBS is complete. Often, verification is approached by testing the structural properties of the KBS after the rules have been defined. In this paper we take a different approach and show how the process of formal program derivation from software engineering can be applied to KBSs. The use of these techniques eliminates the need for post-development verification because program derivation guarantees that the KBS will not contain redundant rules, conflicting rules, or be incomplete. As such, verification concerns are addressed during development.

Verification; program derivation; formal methods; rule-based systems