提出新语义框架,统一解释逻辑程序的稳定与振荡行为。
On the Trap Space Semantics of Normal Logic Programs
- 引入陷阱空间概念,从状态演化角度重构逻辑程序语义。
- 证明该框架可统一支持、稳定、规则等传统模型语义。
- 适合研究逻辑程序行为分析与形式化验证的学者使用。
正常逻辑程序的传统语义基于克拉克完成和二值/三值标准模型,包括支持、稳定、规则和良基模型。二值解释可视为程序更新算子下的状态演化,其转移图的固定点与环分别刻画稳定与振荡行为,称为动力学语义。我们曾建立无函数符号的Datalog^¬程序与布尔网络的联系,提出陷阱空间概念。本文将此概念推广至任意正常逻辑程序,引入陷阱空间语义作为新解释方法。该语义兼具模型论与动力学特征,提供全面理解程序行为的框架。我们建立了其基础性质,并系统关联到既有模型论语义(如支持、稳定、规则、L-稳定)及动力学语义。结果表明,陷阱空间语义为证明支持类、严格稳定类与规则模型的存在性提供了统一精确框架,并揭示了现有语义间的深层关系。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。