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.

翻译：我们研究一阶逻辑中的一类公式方程——Horn公式方程，其通过谓词变量出现位置的句法限制定义。Horn公式方程在计算机科学的诸多应用中具有重要作用。本文在配备最小不动点算子的一阶逻辑中，陈述并证明了Horn公式方程的不动点定理。该不动点定理具有抽象性，因其适用于概括标准语义的抽象语义框架。我们进一步阐述了该定理在计算逻辑多个领域的推论，涵盖从程序验证的逻辑基础到归纳定理证明的广泛范围。