Verifying the Unification Algorithm in LCF

Details Verifying the Unification Algorithm in LCF Verifying the Unification Algorithm in LCF

2000-09-29

arxiv.org/abs/cs/9301101v1

Science of Computer Programming 5 (1985), 143-170

Computer Science

Logic in Computer Science

Scientific paper

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.

Affiliated with

Also associated with

No associations

Rating

Verifying the Unification Algorithm in LCF does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Verifying the Unification Algorithm in LCF, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Verifying the Unification Algorithm in LCF will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-342997