BriefGPT.xyz
Mar, 2023
引理：生成、选择、应用
Lemmas: Generation, Selection, Application
HTML
PDF
Michael Rawson, Christoph Wernhard, Zsolt Zombori, Wolfgang Bibel
TL;DR
本研究中，我们探讨引理在自动定理证明中的重要作用，提出了一种结合学习技术的系统，该系统能够生成有用的引理来协助自动定理证明，并通过试验验证了该系统在几个代表性问题的解决方面的优越性，特别是成功解决了一系列难题，这些难题在过去20年间都未被任何系统解决。通过侧重简化附加问题的研究，我们得出了引理以及它们在证明搜索中的根本作用。
Abstract
Noting that
lemmas
are a key feature of mathematics, we engage in an investigation of the role of
lemmas
in
automated theorem proving
. The
→