A Forward Inference Engine to Aid in Understanding Specifications

An important part of understanding a specification is recognizing the consequences of what is stated. We describe a program that can help a user acquire this understanding. It does this by deriving interesting, though not deep consequences of a set of input axioms, while avoiding (a typically much larger set of) uninteresting consequences. The heuristics for obtaining that effect are described and justified. The program has been used in a symbolic evaluator that helps a user to understand and debug specifications written in the Gist specification language.

Authors

• Donald Cohen

Keywords

No keywords are indexed for this paper.