Technical reports
Verifying the unification algorithm in LCF
March 1984, 28 pages
DOI: 10.48456/tr-50
Abstract
Manna and Waldinger’s theory of substitutions and unification has been verified using the Cambridge LCF theorem prover. A proof of the monotonicity of substitution is presented in detail, as an example of interaction with LCF. Translating the theory into LCF’s domain-theoretic logic is largely straightforward. Well-founded induction on a complex ordering is translated into nested structural inductions. Correctness of unification is expressed using predicates for such properties as idempotence and most-generality. The verification is presented as a series of lemmas. The LCF proofs are compared with the original ones, and with other approaches. It appears difficult to find a logic that is both simple and flexible, especially for proving termination.
Full text
BibTeX record
@TechReport{UCAM-CL-TR-50, author = {Paulson, Lawrence}, title = {{Verifying the unification algorithm in LCF}}, year = 1984, month = mar, url = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-50.pdf}, institution = {University of Cambridge, Computer Laboratory}, doi = {10.48456/tr-50}, number = {UCAM-CL-TR-50} }