Verifying the unification algorithm in LCF
\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.
- A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction
- Formalization of the resolution calculus for first-order logic
- Completeness in PVS of a nominal unification algorithm
- Unification: A case-study in data refinement
- Unification via the s_e-style of explicit substitutions
- First-order unification by structural recursion
- Lessons learned from LCF: A Survey of Natural Deduction Proofs
- Verification of the Completeness of Unification Algorithms à la Robinson
- A comprehensible guide to a new unifier for CIC including universe polymorphism and overloading
- A certified implementation of ML with structural polymorphism and recursive types
- Automating the derivation of unification algorithms. A case study in deductive program synthesis
- Partial and nested recursive function definitions in higher-order logic
This page was built for publication: Verifying the unification algorithm in LCF
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1060023)
