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 even admit complete procedures, let alone decidable ones. In this paper, we undertake a novel approach for synthesizing inductive hypotheses in order to prove validity in this logic. The key techniques rely on utilizing several kinds of finite first-order models as counterexamples that capture 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, demonstrating the effectiveness of our methodology.

翻译：这种逻辑与纯粹的第一阶逻辑不同,甚至没有接受完整的程序,更不用说可变程序了。在本文件中,我们采取了一种新的方法,将感应假设综合起来,以证明这一逻辑的有效性。关键技术依赖于使用几种有限的第一阶模型作为反比示例,这些模型可以捕捉公式的不可预见性和无效性,用以指导对感应假设的搜索。我们执行我们的程序,并广泛评价涉及需要感应证据的巨型数据结构的巨型数据结构,以证明我们的方法的有效性。