KnowledgeBase » 
SEMINAR
» ID = 576
More on proof automation: Shostak's decision procedure and Nuprl
by Mark Bickford
2001-2002
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.