用一阶逻辑重新定义聚合函数语义，实现程序强等价自动验证。
Recursive Aggregates as Intensional Functions in Answer Set Programming: Semantics and Strong Equivalence
- 将聚合语义转化为带意向函数的命题逻辑
- 提出强等价判定的归约方法，可转换为经典一阶逻辑推理
- 适用于clingo、dlv等求解器，适合形式化验证研究者
本文证明，clingo和dlv求解器中实现的聚合程序语义，可在这里-那里逻辑中通过带意向函数的扩展一阶公式进行刻画。该刻画可用于研究在两种语义下的程序强等价性。我们还提出一种变换，将强等价性检查问题转化为经典一阶逻辑中的推理任务，为自动化该过程提供了基础。
原文摘要 · Abstract (English)
This paper shows that the semantics of programs with aggregates implemented by the solvers clingo and dlv can be characterized as extended First-Order formulas with intensional functions in the logic of Here-and-There. Furthermore, this characterization can be used to study the strong equivalence of programs with aggregates under either semantics. We also present a transformation that reduces the task of checking strong equivalence to reasoning in classical First-Order logic, which serves as a foundation for automating this procedure.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。