An abstract fixed-point theorem for Horn formula equations
Logic in Computer Science
2025-11-12 v1 Logic
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.
Cite
@article{arxiv.2511.08162,
title = {An abstract fixed-point theorem for Horn formula equations},
author = {Stefan Hetzl and Johannes Kloibhofer},
journal= {arXiv preprint arXiv:2511.08162},
year = {2025}
}