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.
翻译:我们从解决公式方程的更普遍的角度考虑限制的合恩条款的解决。受约束的合恩条款与合恩公式方程的子类相对应。我们提出并证明合恩公式方程的固定点理论。 我们提出并证明合恩公式方程的固定点理论,该方程的基础是将一组合恩条款在目标水平上的最低模式的固定点计算作为一阶逻辑中的一种公式,并且有一个最不固定点操作员。我们描述了这一固定点方程的若干轮廓,特别是关于程序核查的逻辑基础,并勾画如何将其概括为包含抽象解释。