提出约束下的答案集编程强等价判定方法
Strong Equivalence in Answer Set Programming with Constraints
- 用带约束的赫尔-托逻辑刻画强等价关系
- 实现clingo类求解器语言到该逻辑的精确转换
- 为规则系统等价性验证提供理论工具
我们研究扩展框架下约束答案集编程中的强等价概念。若两组规则在任意上下文中意义相同，则视为强等价。在特定假设下，该设定中规则集的强等价可被精确刻画为带约束的赫尔-托逻辑中的等价性。我们还提出了从支持约束的clingo类求解器语言到赫尔-托逻辑的翻译方法，使该逻辑可用于此类求解器中的强等价推理。此外，我们探讨了在此背景下判定强等价的计算复杂度。
原文摘要 · Abstract (English)
We investigate the concept of strong equivalence within the extended framework of Answer Set Programming with constraints. Two groups of rules are considered strongly equivalent if, informally speaking, they have the same meaning in any context. We demonstrate that, under certain assumptions, strong equivalence between rule sets in this extended setting can be precisely characterized by their equivalence in the logic of Here-and-There with constraints. Furthermore, we present a translation from the language of several clingo-based answer set solvers that handle constraints into the language of Here-and-There with constraints. This translation enables us to leverage the logic of Here-and-There to reason about strong equivalence within the context of these solvers. We also explore the computational complexity of determining strong equivalence in this context.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。