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.

翻译：本文证明了由求解器clingo和dlv实现的聚合程序语义，可在"此时此地"逻辑中表征为带有内涵函数的一阶扩展公式。此外，该表征可用于研究两种语义下聚合程序的强等价性。我们还提出了一种将强等价性验证任务归约为经典一阶逻辑推理的转换方法，为自动化该过程奠定了理论基础。