Model-Guided Synthesis of Inductive Lemmas for FOL with Least Fixpoints

TL;DR

This paper introduces a novel method for synthesizing inductive lemmas in first-order logic with least fixpoints, using finite models as counterexamples to guide proof search, especially for heap data structures.

Contribution

It presents a new approach leveraging finite models as counterexamples to synthesize inductive hypotheses in FO+lfp logic, addressing its proof challenges.

Findings

Effective synthesis of inductive lemmas demonstrated on heap data structure theorems.

Method improves proof automation in FO+lfp logic.

Extensive evaluation shows high success rate in complex inductive proofs.

Abstract

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.