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

DOI10.1017/S1471068410000293MaRDI QIDQ3585169zbMATH OpenOpenAlexFDO

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)

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

zbMATH Keywords

fixpoint definitionsclassical logic extensionsfixpoint constructs

Mathematics Subject Classification ID

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

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

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

Cites work

• scientific article; zbMATH DE number 1936671 (Why is no real title available?)
• scientific article; zbMATH DE number 952378 (Why is no real title available?)
• A logic of nonmonotone inductive definitions
• Abductive Logic Programming
• Depth-First Search and Linear Graph Algorithms
• Stable models and difference logic
• The expressive powers of the logic programming semantics

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)