SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
  SRI Logo

Deconstructing Shostak
 by Dr. Harald Rueß & Dr. Natarajan Shankar.


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.
BibTEX Entry
    AUTHOR = {Harald Rue\ss and {N.} Shankar},
    TITLE = {Deconstructing Shostak},
    NOTE = {To be presented at {LICS'2001}},
    YEAR = {2001},
    URL = {}


About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2024 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy