带差异约束的回答集编程的有界语义：初步报告
Bound-Founded Semantics for Answer Set Programming with Difference Constraints: Preliminary Report
AI总结：
研究带差异约束的回答集编程中现有混合求解器语义基础缺乏统一逻辑基础的问题，引入HTb多类变体构建通用框架，应用于差异约束设置，揭示不同混合系统行为语义根源，形成统一框架便于相关研究。
AI中文摘要：
虽然线性约束的集成显著扩展了回答集编程（ASP）的范围，但现有的混合求解器通常依赖于缺乏统一逻辑基础的不同语义基础。我们通过引入“这里和那里”的有界逻辑（HTb）的多类变体来解决这一差距，提供了一个通用框架，能够刻画具有线性约束的ASP扩展的各种替代语义的平衡模型。我们将此框架应用于差异约束设置，重点是clingo[DL]的语义刻画。我们方法的核心是数值变量有界性的形式化。通过研究不同的混合系统，如clingo[DL]、clingcon和flingo如何证明约束原子，我们揭示了它们不同行为的语义根源。这一研究产生了一个单一、一致的框架，不仅形式化了当前系统（如clingo[DL]）的基础，还便于对程序简化进行严格研究以及未来对不同语义原则的整合。
英文摘要：
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.
