@inproceedings{Ganzinger-02-cade,
  AUTHOR =	 {Ganzinger, H.},
  TITLE =	 {Shostak Light},
  YEAR =	 2002,
  publisher =	 s,
  series =	 lncs,
  booktitle =	 {Automated Deduction --- CADE-18},
  volume =	 2392,
  pages =	 "332--346",
  Abstract =	 { We represent the essential ingredients of Shostak's
                  procedure at a high level of abstraction, and as a
                  refinement of the Nelson-Oppen procedure. We analyze
                  completeness issues of the method based on a general
                  notion of theories. We also formalize a notion of
                  sigma-models and show that on the basis of Shostak's
                  procedure we cannot distinguish a theory from its
                  approximation represented by the class of its
                  sigma-models. }
}