An abstract fixed-point theorem for Horn formula equations
Stefan Hetzl and Johannes Kloibhofer
我们考虑一阶逻辑中的一类公式方程,Horn公式方程,这是由对谓词变量发生的句法限制定义的。 角方程在计算机科学的许多应用中发挥着重要作用。 我们用最少的定点运算符在一阶逻辑中对 Horn 公式方程进行定点定理。 我们的定点定理是抽象的,因为它适用于概括标准语义的抽象语义。 我们描述了这个定点定理在计算逻辑的各个领域的几个推论,从程序验证的逻辑基础到归纳定理证明。
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 stand...