Combining Shostak Theories

---

Authors

N. Shankar and Harald Rueß

Abstract

Ground decision procedures for combinations of theories are used in many systems for automated deduction. There are two basic paradigms for combining decision procedures. The Nelson--Oppen method combines decision procedures for disjoint theories by exchanging equality information on the shared variables. In Shostak's method, the combination of the theory of pure equality with canonizable and solvable theories is decided through an extension of congruence closure that yields a canonizer for the combined theory. Shostak's original presentation, and others that followed it, contained serious errors which were corrected for the basic procedure by the present authors. Shostak also claimed that it was possible to combine canonizers and solvers for disjoint theories. This claim is easily verifiable for canonizers, but is unsubstantiated for the case of solvers. We show how our earlier procedure can be extended to combine multiple disjoint canonizable, solvable theories within the Shostak framework.

gzipped postscript or postscript

BibTeX Entry

@Unpublished{ShankarRuess:RTA02,
  author =       {N. Shankar and Harald Rue{\ss}},
  title =        {Combining Shostak Theories},
  year =         {2002},
  note =         {Invited paper for Floc'02/RTA'02}
}

---

Harald Ruess: ruess@csl.sri.com