FO(FD): Extending classical logic with rule-based fixpoint definitions

TL;DR

This paper introduces FO(FD), a logic extending classical logic with rule-based fixpoint definitions, enabling new ways to model and solve problems involving fixpoint constructs.

Contribution

It presents FO(FD), a novel logic combining fixpoint definitions with classical logic, and explores its relation to FO(ID) and satisfiability solving via difference logic.

Findings

Reduction of FO(FD) to difference logic enables practical satisfiability solving.

Application of FO(FD) to fairness conditions demonstrates its modeling capabilities.

Potential applications in knowledge representation and reasoning are discussed.

Abstract

We introduce fixpoint definitions, a rule-based reformulation of fixpoint constructs. The logic FO(FD), an extension of classical logic with fixpoint definitions, is defined. We illustrate the relation between FO(FD) and FO(ID), which is developed as an integration of two knowledge representation paradigms. The satisfiability problem for FO(FD) is investigated by first reducing FO(FD) to difference logic and then using solvers for difference logic. These reductions are evaluated in the computation of models for FO(FD) theories representing fairness conditions and we provide potential applications of FO(FD).