Agda 中的一阶自然演绎
逻辑
2021-04-12 v1 计算机科学中的逻辑
摘要
Agda 是一种依赖类型的函数式编程语言，基于直觉主义 Martin-Löf 类型论的扩展。我们在 Agda 中实现一阶自然演绎。我们利用 Agda 的类型检查器来验证自然演绎证明的正确性，并利用 Agda 的证明辅助功能证明自然演绎的性质。该实现对应于构造类型论中自然演绎的形式化，并且这些证明经 Agda 验证为正确（在假定 Agda 本身正确的前提下）。
引用
@article{arxiv.2104.04095,
title = {First-order natural deduction in Agda},
author = {Louis Warren},
journal= {arXiv preprint arXiv:2104.04095},
year = {2021}
}