Recursive Aggregates as Intensional Functions in Answer Set Programming: Semantics and Strong Equivalence
This work addresses foundational semantics and equivalence issues in ASP, which is incremental as it builds on existing solver implementations to provide theoretical insights and automation tools.
The paper tackles the problem of characterizing the semantics of programs with aggregates in Answer Set Programming (ASP) solvers like clingo and dlv, showing they can be represented as extended First-Order formulas with intensional functions in the logic of Here-and-There, and uses this to study strong equivalence, reducing its checking to classical First-Order logic for automation.
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.