带最小不动点的一阶逻辑中归纳引理的模型引导综合

嵌入于基于指针的堆中的递归定义链表数据结构及其性质，可自然地用带最小不动点定义（FO+lfp）及背景理论的一阶逻辑表达。此类逻辑与纯一阶逻辑不同，甚至不存在完备过程。本文提出一种综合归纳假设以证明该逻辑中有效性的新方法。其思路是利用多种有限一阶模型作为反例，捕捉公式的不可证性与无效性，以引导归纳假设的搜索。我们实现了所述过程，并在涉及需要归纳证明的堆数据结构定理上进行了广泛评估，展示了方法的有效性。