An abstract fixed-point theorem for Horn formula equations
Stefan Hetzl, Johannes Kloibhofer
TL;DR
This work proves an abstract fixed-point theorem for Horn formula equations in FO logic with a least fixed-point operator, leveraging model abstractions to unify standard and abstract semantics. It shows that every Horn formula equation has a least solution given by the lfp of an operator Φ_ψ, and that this framework yields corollaries for weakest preconditions, strongest postconditions, affine solvability, and verification conditions. The results bridge Horn clause solving, second-order quantifier elimination, and abstract interpretation, enabling applications to program verification and inductive theorem proving while providing a unifying theoretical lens. The approach also yields dual-Horn and linear-Horn variants, demonstrates decidability in the affine setting, and connects to a broad literature on fixed-point theorems and Horn clauses, offering a versatile toolkit for logical foundations and practical verification.
Abstract
We consider a class of formula equations in first-order logic, Horn formula equations, which are defined by a syntactic restriction on the occurrences of predicate variables. Horn formula equations play an important role in many applications in computer science. We state and prove a fixed-point theorem for Horn formula equations in first-order logic with a least fixed-point operator. Our fixed-point theorem is abstract in the sense that it applies to an abstract semantics which generalises standard semantics. We describe several corollaries of this fixed-point theorem in various areas of computational logic, ranging from the logical foundations of program verification to inductive theorem proving.