Verifying the Unification Algorithm in LCF
| dc.creator | Paulson, Lawrence C. | |
| dc.date | 2000-09-29 | |
| dc.date.accessioned | 2026-07-07T09:12:15Z | |
| dc.date.available | 2026-07-07T09:12:15Z | |
| dc.description | 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. | |
| dc.identifier | https://arxiv.org/abs/cs/9301101 | |
| dc.identifier | http://arxiv.org/abs/cs/9301101 | |
| dc.identifier | Science of Computer Programming 5 (1985), 143-170 | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/151960 | |
| dc.subject | Logic in Computer Science | |
| dc.subject | D.2.4; F.3.1; F.4.1 | |
| dc.title | Verifying the Unification Algorithm in LCF | |
| dc.type | text |