一句话：提出用有限一阶模型作为反例引导，合成带最小不动点一阶逻辑中的归纳引理以证明公式有效性。
递归定义的链式数据结构及其性质常可用带最小不动点定义的一阶逻辑（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.
@article{paperbot1437,
title = {Model-guided synthesis of inductive lemmas for FOL with least fixpoints},
author = {Adithya Murali and Lucas Peña and Eion Blanchard and Christof Löding and P. Madhusudan},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {OOPSLA2},
year = {2022},
doi = {10.1145/3563354}
}