Simplification by Cooperating Decision Procedures
- 1 October 1979
- journal article
- Published by Association for Computing Machinery (ACM) in ACM Transactions on Programming Languages and Systems
- Vol. 1 (2), 245-257
- https://doi.org/10.1145/357073.357079
Abstract
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.Keywords
This publication has 3 references indexed in Scilit:
- A Practical Decision Procedure for Arithmetic with Function SymbolsJournal of the ACM, 1979
- Assignment Commands with Array ReferencesJournal of the ACM, 1978
- Some Completeness Results in the Mathematical Theory of ComputationJournal of the ACM, 1968