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

arXiv: https://arxiv.org/abs/2412.10975 · HTML: https://mlsanity.com/paper/2412.10975/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 6 of its 40 references that are in the map.
- First posted on arXiv 14 Dec 2024.

## Builds on (most cited first, 6 of 6)

- [Verifying Tight Logic Programs with anthem and Vampire](https://mlsanity.com/paper/2008.02025/) (2020)
- [Vicious Circle Principle and Logic Programs with Aggregates](https://mlsanity.com/paper/1808.07050/) (2018)
- [First-Order Stable Model Semantics with Intensional Functions](https://mlsanity.com/paper/2307.10225/) (2023)
- [Relating Two Dialects of Answer Set Programming](https://mlsanity.com/paper/1907.12139/) (2019)
- [Strong Equivalence of Logic Programs with Counting](https://mlsanity.com/paper/2205.07783/) (2022)
- [Functional ASP with Intensional Sets: Application to Gelfond-Zhang Aggregates](https://mlsanity.com/paper/1805.00660/) (2018)

## Built on by (most cited first, 1 of 1)

- [Deductive Systems for Logic Programs with Counting](https://mlsanity.com/paper/2511.19565/) (2025)

## Abstract (arXiv)

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.