Knowledge Base Reduction for Verifying Rulebases Containing Equations

Contents

The use of Knowledge Base Reduction to verify rule bases was first developed for propositional rule bases, and then extended to handle quantified variables in rules. However, these techniques did not reason about equations. This paper gives a formal specification of KB-Reducer3, an analysis tool for rule bases containing equations. The algorithm for KB-Reducer3 is described, and a brief discussion on its use and limitations is provided.