Deconstructing Shostak

Accepted for publication at LICS'2001.

---

Authors

Harald Rueß and N. Shankar

Abstract

Shostak's decision procedure for equality in the combination of solvable and canonizable theories has been around for nearly two decades. Variations of this decision procedure have been implemented in a number of systems including STP, EHDM, PVS, STeP, and SVC. The algorithm is extremely subtle and a correctness argument for it has remained elusive. A previous paper by Cyrluk, Lincoln, and Shankar gave a rigorous presentation of the algorithm but only outlined its proof. Shostak's algorithm and all previously published variants of it are in fact incomplete. We describe a variation of Shostak's algorithm as a system of transformations on sets of equalities, along with straightforward proofs of soundness and completeness.

gzipped postscript or postscript

BibTeX Entry

@unpublished{RuessShankar:LICS2001,
	TITLE = {Deconstructing Shostak},
	AUTHOR = {Harald Rue{\ss} and N. Shankar},
	YEAR = 2001,
	NOTE = {To be presented at LICS'2001}
}

---

Harald Ruess: ruess@csl.sri.com