Skip to main content
PRL Project

More on proof automation: Shostak's decision procedure and Nuprl

by Mark Bickford

Shostak's algorithm has been around for twenty years. It is a decision procedure for the equations on terms where some function symbols are interpreted in a "canonizable and solvable" theory. Shostak is at the heart of PVS, SVC and other "west coast" theorem provers. Shankar and Ruess have written a paper called "Deconstructing Shostak" in which they present a variant of Shostak's original algorithm and they prove that it is sound and complete. This is the first proof of completeness for Shostak (apparently the original algorithm was not complete).
I'll describe the algorithm, give some examples, and sketch the proofs of soundness and completeness. Then I'll talk about how this algorithm can be implemented as a tactic in Nuprl.
Those interested in reflection could think about how the whole proof of soundness and completeness could be done in Nuprl + reflection.