大型形式化数学中的定理证明作为一个新兴的 AI 领域
人工智能
2012-12-18 v2 数字图书馆
摘要
近年来，我们将大型形式化数学语料库与自动定理证明 (ATP) 工具联系起来，并开始在此环境下开发组合式 AI/ATP 系统。在本文中，我们首先将此项目与 Quaife 使用 McCune 的 Otter 系统早期进行的大规模自动化开发，以及 QED 项目关于形式化大部分数学的讨论联系起来。然后，我们总结了迄今为止的历程，论证 QED 的愿景在预见一个非常有趣的语义 AI 领域的创建上是正确的，并讨论了其进一步的研究方向。
引用
@article{arxiv.1209.3914,
title = {Theorem Proving in Large Formal Mathematics as an Emerging AI Field},
author = {Josef Urban and Jiri Vyskocil},
journal= {arXiv preprint arXiv:1209.3914},
year = {2012}
}