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

DOI10.1017/S1471068410000293zbMATH Open1209.68094arXiv1007.3819OpenAlexW2006396461MaRDI QIDQ3585169FDOQ3585169

Authors: Ping Hou, Broes de Cat, Marc Denecker 

Publication date: 19 August 2010

Published in: Theory and Practice of Logic Programming (Search for Journal in Brave)

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).

Full work available at URL: https://arxiv.org/abs/1007.3819

Recommendations

• A logic of fixpoint definitions
• Publication:3204028
• A Deductive System for FO(ID) Based on Least Fixpoint Logic
• Fixed-point extensions of first-order logic
• Fixed-point logics and computation

zbMATH Keywords

fixpoint definitionsclassical logic extensionsfixpoint constructs

Mathematics Subject Classification ID

Knowledge representation (68T30) Logic programming (68N17)

Cites Work

• Depth-First Search and Linear Graph Algorithms
• Abductive Logic Programming
• Title not available (Why is that?)
• Title not available (Why is that?)
• Stable models and difference logic
• The expressive powers of the logic programming semantics
• A logic of nonmonotone inductive definitions

Cited In (8)

• Embedding justification theory in approximation fixpoint theory
• A Deductive System for FO(ID) Based on Least Fixpoint Logic
• Recursive rules with aggregation: a simple unified semantics
• On Nested Justification Systems
• Tree-like justification systems are consistent
• A logic of fixpoint definitions
• Justifications and a reconstruction of parity game solving algorithms
• A formal theory of justifications

This page was built for publication: \(FO(FD)\): extending classical logic with rule-based fixpoint definitions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3585169)