Verifying the unification algorithm in LCF
type: Item
instance of: scholarly article
title: Verifying the unification algorithm in LCF
zbMATH Open document ID: 0567.68054
DOI: 10.1016/0167-6423(85)90009-7
published in: Science of Computer Programming
publication date: 1985-01-01T00:00:00Z
review text: \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.
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 68Q60
zbMATH DE Number: 3905873
zbMATH Keywords: substitutions
zbMATH Keywords: Cambridge LCF theorem prover
zbMATH Keywords: termination
Wikidata QID: Q57382754
author: Lawrence C. Paulson
describes a project that uses: LCF
describes a project that uses: HOL
MaRDI profile type: Publication
full work available at URL: 0167-6423(85)90009-7
OpenAlex ID: W2019994514
description: scientific article; zbMATH DE number 3905873