arXiv · 2412.10975
Recursive Aggregates as Intensional Functions in Answer Set Programming: Semantics and Strong Equivalence
Abstract
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.
Explore related subjects
Keep this discovery
Explore connections, maps & timelines
Jorge Fandinno, Zachary Hansen. 2024-12-14. Recursive Aggregates as Intensional Functions in Answer Set Programming: Semantics and Strong Equivalence. https://arxiv.org/abs/2412.10975
Cite the original work for its findings. Save a collection to share your selection of sources.