Aug, 2022
谁发现了短证明？使用高阶自动定理证明器探索Boolos的奇怪推理变体
Who Finds the Short Proof? An Exploration of variants of Boolos' Curious
Inference using Higher-order Automated Theorem Provers
TL;DR应用高阶自动推理证明器探索 Boolos' Curious 推论，通过提供适当的简写符号以发现短证明所需的高阶引理，并提出全证明自动化的可能性。