|
AuthorPatricia D. L. Machadopatricia@dsc.ufpb.br
DescriptionUnification, which plays a central hole in theorem-proving, is the process of finding a common instance of two expressions, and if such an instance exists, the algorithm produces a substitution that yields that instance. The unification specification presented here is modelled on the one presented by Manna and Waldinger and is used in the author's PhD thesis to produce a case study on generating test oracles from structured algebraic specifications (see unification.ps.)The specification has been parsed successfully with HOL-CASL v0.3 and CATS v0.54.
Specification |