论文标题
具有最小固定点的FOL的诱导引理的模型引导合成
Model-Guided Synthesis of Inductive Lemmas for FOL with Least Fixpoints
论文作者
论文摘要
递归定义的链接的数据结构嵌入了基于指针的堆中，它们的属性自然而然地以纯的一阶逻辑表达，具有最小的fixpoint定义（FO+LFP），并具有背景理论。与纯的一阶逻辑不同，这种逻辑甚至不承认完整的过程。在本文中，我们采用了一种新的方法来合成归纳假设，以证明该逻辑有效性。这个想法是利用几种有限的一阶模型作为捕获公式的不可估量和无效性的反例来指导搜索归纳假设。我们实施我们的程序，并对涉及需要归纳证明的堆数据结构的定理进行广泛评估，并证明我们方法的有效性。
Recursively defined linked data structures embedded in a pointer-based heap and their properties are naturally expressed in pure first-order logic with least fixpoint definitions (FO+lfp) with background theories. Such logics, unlike pure first-order logic, do not admit even complete procedures. In this paper, we undertake a novel approach for synthesizing inductive hypotheses to prove validity in this logic. The idea is to utilize several kinds of finite first-order models as counterexamples that capture the non-provability and invalidity of formulas to guide the search for inductive hypotheses. We implement our procedures and evaluate them extensively over theorems involving heap data structures that require inductive proofs and demonstrate the effectiveness of our methodology.
