Verifying the unification algorithm in LCF (Q1060023)

\textit{Z. Manna} and \textit{R. Waldinger}'s [ibid. 1, 5-48 (1981; Zbl 0472.68054)] theory of substitutions and unification has been verified using the Cambridge LCF theorem prover. A proof of the monotonicity of substitution is presented as a detailed example of interaction with LCF. Translating the theory into LCF's domain-theoretic logic is largely straightforward. Correctness of unification is expressed using predicates for such properties as idempotence and most-generality. Well-founded induction on a complex ordering is translated into nested structural inductions. The inductions divide the verification into lemmas: a constant is unifiable with itself, a constant is not unifiable with a combination, etc. The LCF proofs are compared with the original ones. Most of the work is devoted to proving that unification terminates. LCF's approach to termination proofs is compared with that of Boyer and Moore and others.