论文标题
谁找到了简短的证据？使用高阶自动定理掠夺的Boolos奇怪推理的变体的探索
Who Finds the Short Proof? An Exploration of Variants of Boolos' Curious Inference using Higher-order Automated Theorem Provers
论文作者
论文摘要
本文使用高阶自动定理抛弃（ATP）报告了Boolos奇怪的推断的探索。令人惊讶的是，只能手工提供合适的速记符号才能找到一个简短的证明。 ATPS自动发现构造简易证明所需的高阶引理。鉴于本文的观察和建议，现在对Boolos和相关示例的完整证明自动化似乎已触及高阶ATP。
This paper reports on an exploration of Boolos' Curious Inference, using higher-order automated theorem provers (ATPs). Surprisingly, only suitable shorthand notations had to be provided by hand for ATPs to find a short proof. The higher-order lemmas required for constructing a short proof are automatically discovered by the ATPs. Given the observations and suggestions in this paper, full proof automation of Boolos' and related examples now seems to be within reach of higher-order ATPs.
