Recursive Aggregates as Intensional Functions in Answer Set Programming: Semantics and Strong Equivalence
Artificial Intelligence
2024-12-17 v1 Logic in Computer Science
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.
Cite
@article{arxiv.2412.10975,
title = {Recursive Aggregates as Intensional Functions in Answer Set Programming: Semantics and Strong Equivalence},
author = {Jorge Fandinno and Zachary Hansen},
journal= {arXiv preprint arXiv:2412.10975},
year = {2024}
}
Comments
Accepted for publication in the Proceedings of the 39th Annual AAAI Conference on Artificial Intelligence