Lemma Generation for Horn Clause Satisfiability: A Preliminary Study

TL;DR

This paper explores methods for generating lemmas during the transformation of constrained Horn clauses to improve satisfiability checking of inductively defined structures, enhancing verification techniques.

Contribution

It introduces a novel approach for lemma generation using difference predicates and auxiliary queries to facilitate clause transformation and satisfiability proofs.

Findings

Difference predicates can serve as lemmata during clause transformation.

Auxiliary queries can replace lemmata when difference predicates are infeasible.

The approach improves the handling of inductively defined data structures in CHC satisfiability.

Abstract

It is known that the verification of imperative, functional, and logic programs can be reduced to the satisfiability of constrained Horn clauses (CHCs), and this satisfiability check can be performed by using CHC solvers, such as Eldarica and Z3. These solvers perform well when they act on simple constraint theories, such as Linear Integer Arithmetic and the theory of Booleans, but their efficacy is very much reduced when the clauses refer to constraints on inductively defined structures, such as lists or trees. Recently, we have presented a transformation technique for eliminating those inductively defined data structures, and hence avoiding the need for incorporating induction principles into CHC solvers. However, this technique may fail when the transformation requires the use of lemmata whose generation needs ingenuity. In this paper we show, through an example, how during the process of transforming CHCs for eliminating inductively defined structures one can introduce suitable predicates, called difference predicates, whose definitions correspond to the lemmata to be introduced. Through a second example, we show that, whenever difference predicates cannot be introduced, we can introduce, instead, auxiliary queries which also correspond to lemmata, and the proof of these lemmata can be done by showing the satisfiability of those queries.