Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On the Boolean Network Theory of Datalog$^\neg$

Van-Giang Trinh, Belaid Benhamou, Sylvain Soliman, François Fages

TL;DR

This paper builds a formal bridge between Datalog$^\neg$ programs and Boolean network theory by mapping atom dependencies to influence graphs and linking stable, supported, and regular semantics to BN trap spaces. It establishes structural results: absence of odd cycles in the atom dependency graph implies that regular models coincide with stable models (ensuring existence), while absence of even cycles yields uniqueness of stable partial and regular models. It provides new upper bounds on the number of stable partial, regular, and stable models via a feedback vertex set, and develops a trap-space framework in which subset-minimal stable trap spaces correspond to regular models. The results extend to uni-rule Datalog$^\neg$ programs, where stronger graphical and complexity bounds hold, and illuminate deep connections between logic programming semantics and discrete dynamical systems with potential algorithmic benefits for model enumeration and analysis.

Abstract

Datalog$^\neg$ is a central formalism used in a variety of domains ranging from deductive databases and abstract argumentation frameworks to answer set programming. Its model theory is the finite counterpart of the logical semantics developed for normal logic programs, mainly based on the notions of Clark's completion and two-valued or three-valued canonical models including supported, stable, regular and well-founded models. In this paper we establish a formal link between Datalog$^\neg$ and Boolean network theory first introduced for gene regulatory networks. We show that in the absence of odd cycles in a Datalog$^\neg$ program, the regular models coincide with the stable models, which entails the existence of stable models, and in the absence of even cycles, we prove the uniqueness of stable partial models and regular models. This connection also gives new upper bounds on the numbers of stable partial, regular, and stable models of a Datalog$^\neg$ program using the cardinality of a feedback vertex set in its atom dependency graph. Interestingly, our connection to Boolean network theory also points us to the notion of trap spaces. In particular we show the equivalence between subset-minimal stable trap spaces and regular models.

On the Boolean Network Theory of Datalog$^\neg$

TL;DR

This paper builds a formal bridge between Datalog programs and Boolean network theory by mapping atom dependencies to influence graphs and linking stable, supported, and regular semantics to BN trap spaces. It establishes structural results: absence of odd cycles in the atom dependency graph implies that regular models coincide with stable models (ensuring existence), while absence of even cycles yields uniqueness of stable partial and regular models. It provides new upper bounds on the number of stable partial, regular, and stable models via a feedback vertex set, and develops a trap-space framework in which subset-minimal stable trap spaces correspond to regular models. The results extend to uni-rule Datalog programs, where stronger graphical and complexity bounds hold, and illuminate deep connections between logic programming semantics and discrete dynamical systems with potential algorithmic benefits for model enumeration and analysis.

Abstract

Datalog is a central formalism used in a variety of domains ranging from deductive databases and abstract argumentation frameworks to answer set programming. Its model theory is the finite counterpart of the logical semantics developed for normal logic programs, mainly based on the notions of Clark's completion and two-valued or three-valued canonical models including supported, stable, regular and well-founded models. In this paper we establish a formal link between Datalog and Boolean network theory first introduced for gene regulatory networks. We show that in the absence of odd cycles in a Datalog program, the regular models coincide with the stable models, which entails the existence of stable models, and in the absence of even cycles, we prove the uniqueness of stable partial models and regular models. This connection also gives new upper bounds on the numbers of stable partial, regular, and stable models of a Datalog program using the cardinality of a feedback vertex set in its atom dependency graph. Interestingly, our connection to Boolean network theory also points us to the notion of trap spaces. In particular we show the equivalence between subset-minimal stable trap spaces and regular models.

Paper Structure

This paper contains 37 sections, 72 theorems, 6 equations, 7 figures, 1 table.

Table of Contents

  1. Introduction
  2. Paper Structure.
  3. Preliminaries
  4. Normal Logic Programs
  5. Syntax
  6. Atom Dependency Graph
  7. Semantics of Negation
  8. Stable and Supported Partial Models.
  9. Stable and Supported Classes.
  10. Least Fixpoint
  11. Boolean Networks
  12. Definition
  13. Influence Graph
  14. Dynamics and Attractors
  15. Trap Spaces
  16. ...and 22 more sections

Key Result

Proposition 3.1

Consider a Datalog$^\neg$ program $P$. Let $f$ be the encoded BN of $P$. Then the influence graph of $f$ is a sub-graph of the atom dependency graph of $P$.

Figures (7)

  • Figure 1: (a) Atom dependency graph $\mathsf{adg}({P})$, (b) stable transition graph $\mathsf{tg}_{st}({P})$, and (c) supported transition graph $\mathsf{tg}_{sp}({P})$ of Datalog$^\neg$ program $P$ of \ref{['exam:Datalog-all']}.
  • Figure 2: (a) $\mathsf{G}({f})$, (b) $\mathsf{sstg}({f})$, and (c) $\mathsf{astg}({f})$. The BN $f$ is given in \ref{['exam:throughout-BN']}.
  • Figure 3: (a) Atom dependency graph $\mathsf{adg}({P})$ of the Datalog$^\neg$ program $P$, (b) influence graph $\mathsf{G}({f})$ of the BN $f$. The details of $P$ and $f$ are given in \ref{['exam:Datalog-2-BN-connection']}.
  • Figure 4: Atom dependency graph of the Datalog$^\neg$ program $P$ given in \ref{['exam:Datalog-one-SCC-two-stable-models']}.
  • Figure 5: Signed directed graph $G$ of \ref{['exam:AND-NOT-BN-del-triple']}.
  • ...and 2 more figures

Theorems & Definitions (168)

  • Definition 2.1
  • Definition 2.2
  • Definition 2.3
  • Definition 2.4
  • Definition 2.5
  • Definition 2.6: BS1992
  • Definition 2.7: IS2012
  • Example 2.1
  • Definition 2.8
  • Definition 2.9
  • ...and 158 more