Lemma Generation for Horn Clause Satisfiability: A Preliminary Study

Emanuele De Angelis
(DEC, University "G. d'Annunzio" of Chieti-Pescara, Italy)
Fabio Fioravanti
(DEC, University "G. d'Annunzio" of Chieti-Pescara, Italy)
Alberto Pettorossi
(DICII, University of Roma Tor Vergata, Italy)
Maurizio Proietti
(CNR-IASI, Rome, Italy)

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.

In Alexei Lisitsa and Andrei Nemytykh: Proceedings Seventh International Workshop on Verification and Program Transformation (VPT 2019), Genova, Italy, 2nd April 2019, Electronic Proceedings in Theoretical Computer Science 299, pp. 4–18.
Published: 20th August 2019.

ArXived at: https://dx.doi.org/10.4204/EPTCS.299.4 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org