Synthesizing Lemmas for Inductive Reasoning
Synthesizing Lemmas for Inductive Reasoning
复制标题
综合引理进行归纳推理
DOI：
--
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
P. Madhusudan
中科院分区：
文献类型：
--
作者：
Adithya Murali;Lucas Peña;Christof Löding;P. Madhusudan
递归定义的结构和它们的属性自然地用一阶逻辑表示，具有最小不动点定义（FO+lfp），但这种逻辑的自动推理尚未取得太大进展。与纯粹的自由自由不同，这种逻辑甚至不承认完整的程序，更不用说可确定的程序了。在本文中，我们进行了一个基础的研究，寻找证明，使用归纳法推理这些逻辑。通过将证明视为纯粹的FO证明，并加上归纳引理的声明，我们将证明分别分为演绎推理的组件（可以自动完成）和需要推断的引理陈述。当人类凭直觉推断出这些引理时，我们提出了一种反例驱动技术来指导这些引理的合成，其中反例是有限模型，它见证了无法证明定理以及其他提出的引理。我们开发了相对完整的程序，使用程序/表达式合成的技术和工具来合成这些引理，用于强大的FO+lfp逻辑，这些逻辑具有受自然理论（如算术和集合论）约束的背景排序。我们评估了我们的程序，并证明了在一类需要找到归纳证明的定理上，我们的自动综合程序在证明它们时是有效的。
Recursively defined structures and properties about them are naturally expressed in first-order logic with least fixpoint definitions (FO+lfp), but automated reasoning for such logics has not seen much progress. Such logics, unlike pure FOL, do not even admit complete procedures, let alone decidable ones. In this paper, we undertake a foundational study of finding proofs that use induction to reason with these logics. By treating proofs as purely FO proofs punctuated by declarations of induction lemmas, we separate proofs into deductively reasoned components that can be automated and statements of lemmas that need to be divined, respectively. While humans divine such lemmas with intuition, we propose a counterexample driven technique that guides the synthesis of such lemmas, where counterexamples are finite models that witness inability of proving the theorem as well as other proposed lemmas. We develop relatively complete procedures for synthesizing such lemmas using techniques and tools from program/expression synthesis, for powerful FO+lfp logics that have background sorts constrained by natural theories such as arithmetic and set theory. We evaluate our procedures and show that over a class of theorems that require finding inductive proofs, our automatic synthesis procedure is effective in proving them.