The integration of linear constraints has significantly expanded the reach of Answer Set Programming (ASP), yet existing hybrid solvers often rely on disparate semantic underpinnings that lack a unified logical foundation. To address this gap, we introduce 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.
Blogger's Review: The introduction of a many-sorted Bound-founded Logic provides a new theoretical foundation for Answer Set Programming, particularly showcasing remarkable flexibility in handling linear constraints. This framework opens up possibilities for further research, especially in program simplification and semantic integration, holding significant academic value and application prospects.