On the Trap Space Semantics of Normal Logic Programs

TL;DR

This work introduces trap space semantics as a unified framework for interpreting normal logic programs (NLPs), blending model-theoretic and dynamical perspectives. By generalizing trap-space concepts from finite Datalog-neg programs to arbitrary NLPs, it defines stable and supported trap spaces and shows how they relate to established semantics such as stable, supported, regular, and L-stable models, as well as to dynamical transition graphs. The authors prove foundational properties, establish existence results for stable/supported trap spaces and corresponding classes, and demonstrate how trap-space analysis yields precise correspondences and corrections to prior results. The framework provides a principled method to reason about fixed points and trajectory-based behaviors in NLPs, with potential benefits for verification, knowledge representation, and systems biology. Overall, trap space semantics unify disparate semantic approaches and offer a rigorous, axiomatic basis for deriving existence results and comparing NLP semantics across model-theoretic and dynamical viewpoints.

Abstract

The logical semantics of normal logic programs has traditionally been based on the notions of Clark's completion and two-valued or three-valued canonical models, including supported, stable, regular, and well-founded models. Two-valued interpretations can also be seen as states evolving under a program's update operator, producing a transition graph whose fixed points and cycles capture stable and oscillatory behaviors, respectively. We refer to this view as dynamical semantics since it characterizes the program's meaning in terms of state-space trajectories, as first introduced in the stable (supported) class semantics. Recently, we have established a formal connection between Datalog^\neg programs (i.e., normal logic programs without function symbols) and Boolean networks, leading to the introduction of the trap space concept for Datalog^\neg programs. In this paper, we generalize the trap space concept to arbitrary normal logic programs, introducing trap space semantics as a new approach to their interpretation. This new semantics admits both model-theoretic and dynamical characterizations, providing a comprehensive approach to understanding program behavior. We establish the foundational properties of the trap space semantics and systematically relate it to the established model-theoretic semantics, including the stable (supported), stable (supported) partial, regular, and L-stable model semantics, as well as to the dynamical stable (supported) class semantics. Our results demonstrate that the trap space semantics offers a unified and precise framework for proving the existence of supported classes, strict stable (supported) classes, and regular models, in addition to uncovering and formalizing deeper relationships among the existing semantics of normal logic programs.

Figures (2)

• Figure 1: Stable transition graph (a) and supported transition graph (b) of the NLP $P$ of Example \ref{['exam:NLP-all']}. Herein, $a_i$ denotes $p(s^i(0))$, $I_1(a) = 0, \forall a \in \mathsf{HB}_{P}$ ($I_1 = \emptyset$), $I_2(a) = 1, \forall a \in \mathsf{HB}_{P}$ ($I_2 = \mathsf{HB}_{P}$).
• Figure 2: Summary of the main relationships shown in Section \ref{['sec:TS-relationships']}. A full arc indicates a set-inclusion relation, whereas a dashed line along with a box indicate the relationship between the two end vertices.

Theorems & Definitions (38)

• Definition 2.1
• Example 2.1
• Example 2.2
• Lemma 2.1: Zorn's lemma Zorn1935
• Lemma 2.2: BS2014
• Lemma 2.3: Hartogs' lemma
• Definition 3.1
• Definition 3.2
• Definition 3.3
• Example 3.1