将 HOL 翻译到 Dedukti
计算机科学中的逻辑
2015-08-03 v1
摘要
Dedukti 是一个基于 lambda-Pi-calculus modulo 重写的逻辑框架，其通过重写规则扩展了 lambda-Pi-calculus。在本文中，我们展示如何将一族 HOL 证明助手的证明翻译到 Dedukti。该翻译保持绑定、类型与归约。我们在一自动化工具中实现了此翻译，并用它成功翻译了 OpenTheory 标准库。
引用
@article{arxiv.1507.08720,
title = {Translating HOL to Dedukti},
author = {Ali Assaf and Guillaume Burel},
journal= {arXiv preprint arXiv:1507.08720},
year = {2015}
}
备注
In Proceedings PxTP 2015, arXiv:1507.08375