Key points are not available for this paper at this time.
A method for combining decision procedures for several theories into a single decision procedure for their combination is described, and a simplifier based on this method is discussed. The simplifier finds a normal form for any expression formed from individual variables, the usual Boolean connectives, the equality predicate =, the conditional function if-then-else, the integers, the arithmetic functions and predicates +, -, and ≤, the Lisp functions and predicates car, cdr, cons, and atom, the functions store and select for storing into and selecting from arrays, and uninterpreted function symbols. If the expression is a theorem it is simplified to the constant true, so the simplifier can be used as a decision procedure for the quantifier-free theory containing these functions and predicates. The simplifier is currently used in the Stanford Pascal Verifier.
Building similarity graph...
Analyzing shared references across papers
Loading...
ACM Transactions on Programming Languages and Systems
Stanford University
Add This Paper to Your Research Feed
Any time a new paper drops it will be there.
Nelson et al. (Mon,) studied this question.