A Generalization of Shostak's Method for Combining Decision Procedures

摘要

Consider the problem of determining whether a quantifier-free formula Φ is satisfiable in some first-order theory τ. Shostak's algorithm decides this problem for a certain class of theories with both interpreted and uninterpreted function symbols. We present two new algorithms based on Shostak's method. The first is a simple subset of Shostak's algorithm for the same class of theories but without uninterpreted function symbols. This simplified algorithm is easy to understand and prove correct, providing insight into how and why Shostak's algorithm works. The simplified algorithm is then used as the foundation for a generalization of Shostak's method based on a variation of the Nelson-Oppen method for combining theories.