A Fixed-point Theorem for Horn Formula Equations

TL;DR

This paper introduces a fixed-point theorem for Horn formula equations, providing a logical foundation for program verification and potential generalizations to abstract interpretations.

Contribution

It establishes a fixed-point theorem for Horn formula equations using first-order logic with a least fixed point operator, advancing theoretical understanding.

Findings

Fixed-point theorem for Horn formula equations proved.

Logical foundations for program verification clarified.

Framework for incorporating abstract interpretations sketched.

Abstract

We consider constrained Horn clause solving from the more general point of view of solving formula equations. Constrained Horn clauses correspond to the subclass of Horn formula equations. We state and prove a fixed-point theorem for Horn formula equations which is based on expressing the fixed-point computation of a minimal model of a set of Horn clauses on the object level as a formula in first-order logic with a least fixed point operator. We describe several corollaries of this fixed-point theorem, in particular concerning the logical foundations of program verification, and sketch how to generalise it to incorporate abstract interpretations.