2021/09/10 by Stefan Hetzl, Johannes Kloibhofer
Computer Science · #cs.LO
paper · pdf · doi:10.4204/eptcs.344.5
published as EPTCS 344, 2021, pp. 65-78 · In Proceedings HCVS 2021, arXiv:2109.03988
arxiv created 2021/09/10 · arxiv updated 2021/09/13
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.