An abstract fixed-point theorem for Horn formula equations

TL;DR

This paper establishes a fixed-point theorem for Horn formula equations in first-order logic, providing a general framework applicable to various areas like program verification and theorem proving.

Contribution

It introduces an abstract fixed-point theorem for Horn formula equations that generalizes standard semantics and applies broadly across computational logic.

Findings

The theorem applies to an abstract semantics, broadening its applicability.

Several corollaries demonstrate its relevance in program verification and inductive theorem proving.

The fixed-point theorem unifies various logical foundations in a general framework.

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.