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

TL;DR

This paper characterizes the semantics of aggregate programs in answer set programming using extended First-Order logic with intensional functions, enabling analysis of strong equivalence and automating reasoning tasks.

Contribution

It provides a formal logical characterization of aggregate semantics and introduces a transformation for automating strong equivalence checking in answer set programming.

Findings

Semantics of aggregate programs can be expressed in extended First-Order logic.

Strong equivalence of programs with aggregates can be analyzed using this logical framework.

A transformation reduces strong equivalence checking to classical First-Order reasoning.

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.