等式约束列表的幂等 MGU 公理的机器检验模型
计算机科学中的逻辑
2010-12-23 v1
摘要
我们提出了形式化证明，验证了定义在可满足约束列表上的一阶合一算法能生成最一般合一子（MGU），且该合一子恰好是幂等的。我们所有的证明都在 Coq 定理证明器中进行了形式化。我们的证明表明，由合一算法生成的有限映射提供了刻画约束列表的幂等 MGU 公理的一个模型。作为我们验证基础的公理，是通过将标准公理集扩展到约束列表上而得到的。对我们而言，约束是简单类型语言中项之间的等式。替换使用 Coq 库 Coq.FSets.FMapInterface 形式化建模为有限映射。Coq 的函数归纳法是证明许多公理时使用的主要证明技术。
引用
@article{arxiv.1012.4892,
title = {A Machine Checked Model of Idempotent MGU Axioms For Lists of Equational Constraints},
author = {Sunil Kothari and James Caldwell},
journal= {arXiv preprint arXiv:1012.4892},
year = {2010}
}
备注
In Proceedings UNIF 2010, arXiv:1012.4554