Verifying the Unification Algorithm in LCF
Verifying the Unification Algorithm in LCF
复制标题
验证LCF中的统一算法
DOI：
10.1016/0167-6423(85)90009-7
复制
发表时间：
1985
期刊：
影响因子：
--
通讯作者：
Lawrence Charles Paulson
中科院分区：
文献类型：
--
作者：
Lawrence Charles Paulson
Manna和Waldinger的替换和统一理论已使用剑桥LCF定理证明器进行了验证。给出了代换单调性的详细证明。作为与LCF互动的一个例子。将该理论转换为LCF的域理论逻辑在很大程度上是简单的。将复序上的良基归纳转化为嵌套的结构归纳。统一的正确性是用谓词来表示的，这些谓词的性质如等元性和最一般性。验证被呈现为一系列引理。的LCF证明进行了比较，与原来的，并与其他方法。似乎很难找到一个既简单又灵活的逻辑，特别是对于进行困难的终止证明。
Manna and Waldinger's theory of substitutions and unification has been verified using the Cambridge LCF theorem prover. A proof of the monotonicity of substitutiion 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 conducting difficult proofs of termination.