ML Anthology

Recursive Aggregates as Intensional Functions in Answer Set Programming: Semantics and Strong Equivalence

Jorge Fandinno, Zachary Hansen
AAAI 2025 pp. 14893-14901
doi:10.1609/AAAI.V39I14.33633 /aaai/2025/fandinno2025aaai-recursive/

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.

PDF AAAI Semantic Scholar

Cite

Text

Fandinno and Hansen. "Recursive Aggregates as Intensional Functions in Answer Set Programming: Semantics and Strong Equivalence." AAAI Conference on Artificial Intelligence, 2025. doi:10.1609/AAAI.V39I14.33633

Markdown

[Fandinno and Hansen. "Recursive Aggregates as Intensional Functions in Answer Set Programming: Semantics and Strong Equivalence." AAAI Conference on Artificial Intelligence, 2025.](https://mlanthology.org/aaai/2025/fandinno2025aaai-recursive/) doi:10.1609/AAAI.V39I14.33633

BibTeX

@inproceedings{fandinno2025aaai-recursive,
  title     = {{Recursive Aggregates as Intensional Functions in Answer Set Programming: Semantics and Strong Equivalence}},
  author    = {Fandinno, Jorge and Hansen, Zachary},
  booktitle = {AAAI Conference on Artificial Intelligence},
  year      = {2025},
  pages     = {14893-14901},
  doi       = {10.1609/AAAI.V39I14.33633},
  url       = {https://mlanthology.org/aaai/2025/fandinno2025aaai-recursive/}
}