GRUNGE：一个大一统的 ATP 挑战
计算机科学中的逻辑
2019-11-20 v2
摘要
本文描述了一组通过将 HOL4 标准库中的定理翻译为多种逻辑形式而得到的大型相关定理证明问题集。这些形式涵盖高阶逻辑（含与不含类型变量）以及一阶逻辑（可能含多类型，且可能含类型变量）。所得问题集使我们能够在对应问题上运行支持不同逻辑格式的自动定理证明器（ATP），并比较其性能。这也产生了一个新的“大一统”大型理论基准，其模拟了 ITP/ATP hammer 环境，其中系统与元系统可以以互补方式使用多种 ATP 形式，并从积累的知识中联合学习。
引用
@article{arxiv.1903.02539,
title = {GRUNGE: A Grand Unified ATP Challenge},
author = {Chad E. Brown and Thibault Gauthier and Cezary Kaliszyk and Geoff Sutcliffe and Josef Urban},
journal= {arXiv preprint arXiv:1903.02539},
year = {2019}
}
备注
CADE 27 -- 27th International Conference on Automated Deduction