-
- Greg Nelson
- Artificial Intelligence Laboratory, Computer Science Department, Stanford University, Stanford, CA
-
- Derek C. Oppen
- Artificial Intelligence Laboratory, Computer Science Department, Stanford University, Stanford, CA
書誌事項
- 公開日
- 1979-10
- 権利情報
-
- https://www.acm.org/publications/policies/copyright_policy#Background
- DOI
-
- 10.1145/357073.357079
- 公開者
- Association for Computing Machinery (ACM)
この論文をさがす
説明
<jats:p>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.</jats:p>
収録刊行物
-
- ACM Transactions on Programming Languages and Systems
-
ACM Transactions on Programming Languages and Systems 1 (2), 245-257, 1979-10
Association for Computing Machinery (ACM)