自动发现定理证明中反复出现的术语模式，提升证明效率。
Twitch: Learning Abstractions for Equational Theorem Proving
- 用已有证明失败或成功案例挖掘重复出现的术语模式
- 在TPTP的UEQ问题上解决12个评级1级问题并加速多数求解
- 适合对自动化定理证明感兴趣的研究人员
自动化推理中许多成功策略依赖人工指定哪些项或子句结构值得关注。本文旨在自动发现这些有趣项结构。具体而言，我们发现抽象：在相关证明中反复出现的项模式。我们提出工具Twitch，借助原用于程序合成中发现可复用函数的Stitch工具来发现抽象。Twitch可通过两种方式生成抽象：(1) 从一个部分失败的定理证明中；(2) 从同一领域其他定理的成功证明中。我们还扩展了等式定理证明器Twee以使用这些抽象。在TPTP的单位等式（UEQ）问题集上评估Twitch，结果表明其能证明12个评级为1的问题，并在多个其他问题上实现显著提速。
原文摘要 · Abstract (English)
Several successful strategies in automated reasoning rely on human-supplied guidance about which term or clause shapes are interesting. In this paper we aim to discover interesting term shapes automatically. Specifically, we discover abstractions : term patterns that occur over and over again in relevant proofs. We present our tool Twitch which discovers abstractions with the help of Stitch, a tool originally developed for discovering reusable library functions in program synthesis tasks. Twitch can produce abstractions in two ways: (1) from a partial, failed proof of a conjecture; (2) from successful proofs of other theorems in the same domain. We have also extended Twee, an equational theorem prover, to use these abstractions. We evaluate Twitch on a set of unit equality (UEQ) problems from TPTP, and show that it can prove 12 rating-1 problems as well as yielding significant speed-ups on many other problems.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。