Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Jorge Fandinno, Zachary Hansen

TL;DR

This work develops a semantic foundation for recursively defined aggregates in Answer Set Programming by modeling aggregates as intensional set-valued functions within Here-and-There logic. It provides translations that map ASP programs with aggregates into three-sorted extended First-Order sentences, enabling equivalence and correctness results to be established via classical FO reasoning. The authors show equivalence between clingo and the FO-theoretic characterization, and between the various solver semantics, and they introduce a gamma transformation to reduce HT logic to classical logic for automated strong-equivalence checks. The framework bypasses grounding, supports automation, and yields a robust cross-solver understanding of aggregates, with potential applications in formal verification and tooling for ASP+aggregates.

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.

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

TL;DR

This work develops a semantic foundation for recursively defined aggregates in Answer Set Programming by modeling aggregates as intensional set-valued functions within Here-and-There logic. It provides translations that map ASP programs with aggregates into three-sorted extended First-Order sentences, enabling equivalence and correctness results to be established via classical FO reasoning. The authors show equivalence between clingo and the FO-theoretic characterization, and between the various solver semantics, and they introduce a gamma transformation to reduce HT logic to classical logic for automated strong-equivalence checks. The framework bypasses grounding, supports automation, and yields a robust cross-solver understanding of aggregates, with potential applications in formal verification and tooling for ASP+aggregates.

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.

Paper Structure

This paper contains 27 sections, 47 theorems, 55 equations.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Syntax of programs with aggregates.
  4. Many-sorted logic and extended FO formulas.
  5. Stable Model Semantics with Intensional Functions.
  6. Logic Programs With Aggregates as Extended Many-Sorted First-Order Sentences
  7. Target Signature.
  8. Translations.
  9. Standard interpretations.
  10. Correspondence with clingo and dlv
  11. Grounding.
  12. Standard formulas and minimal models.
  13. Clingo.
  14. The dlv semantics.
  15. Strong Equivalence
  16. ...and 12 more sections

Key Result

Proposition 1

Let $F$ be an infinitary propositional formula. Then, $I \models F$ iff $\mathcal{I} \models F$.

Theorems & Definitions (96)

  • Definition 1
  • Proposition 1
  • Proposition 2
  • Proposition 3
  • Proposition 4
  • Theorem 5
  • proof : Proof sketch
  • Theorem 6
  • proof : Proof sketch
  • Theorem 7
  • ...and 86 more