2001.

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.

@unpublished{RuessShankar:LICS2001,
    AUTHOR = {Harald Rue\ss and {N.} Shankar},
    TITLE = {Deconstructing Shostak},
    NOTE = {To be presented at {LICS'2001}},
    YEAR = {2001},
    URL = {http://www.csl.sri.com/papers/lics01/}
}

• shostak2001.pdf
• shostak2001.ps