为带差分约束的答案集编程建立统一语义框架。
Bound-Founded Semantics for Answer Set Programming with Difference Constraints: Preliminary Report
- 提出多类型HTb逻辑，统一处理数值变量的定义性。
- 揭示clingo[DL]等系统在约束原子解释上的语义差异。
- 支持程序简化分析，适合逻辑编程与形式化验证研究者。
尽管线性约束的引入显著拓展了答案集编程（ASP）的应用范围，现有混合求解器常依赖彼此分离的语义基础，缺乏统一逻辑支撑。本文提出一种多类型边界奠基的这里-那里逻辑（HTb），构建了一个灵活框架，可刻画包含线性约束的ASP扩展在多种语义下的平衡模型。聚焦差分约束场景，该框架用于厘清clingo[DL]的语义特性。核心在于对数值变量的奠基性进行形式化。通过分析clingo[DL]、clingcon和flingo等系统如何解释约束原子，我们揭示了其行为差异的语义根源。这一研究形成一个一致的框架，不仅形式化了现有系统如clingo[DL]的基础，还支持程序简化形式化研究，并为未来整合多样语义原则奠定基础。
原文摘要 · Abstract (English)
While the integration of linear constraints has significantly expanded the reach of Answer Set Programming (ASP), existing hybrid solvers often rely on disparate semantic underpinnings that lack a unified logical foundation. We address this gap by introducing a many-sorted variant of the Bound-founded Logic of Here-and-There (HTb), providing a versatile framework capable of characterizing equilibrium models across a wide spectrum of alternative semantics for extensions of ASP with linear constraints. We apply this framework to the setting of difference constraints, focusing on the semantic characterization of clingo[DL]. Central to our approach is the formalization of foundedness for numeric variables. By investigating how different hybrid systems - such as clingo[DL], clingcon, and flingo - justify constraint atoms, we uncover the semantic roots of their varying behaviors. This investigation results in a single, consistent framework that not only formalizes the foundations of current systems like clingo[DL] but also facilitates the rigorous study of program simplifications and the future integration of diverse semantic principles.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。