Research map / Learning theory and algorithms / Combinatorial and search optimization
Recursive Aggregates as Intensional Functions in Answer Set Programming: Semantics and Strong Equivalence
Read the paperCheck your idea against 108,967 papers
AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.
Characterizes clingo and dlv aggregate semantics as extended first-order formulas with intensional functions in the logic of Here-and-There, and reduces strong equivalence checking of programs with recursive aggregates to classical first-order logic.
Problem
Recursive aggregates in answer set programming (clingo and dlv semantics) are hard to analyze without grounding, and strong equivalence of programs with aggregates lacks a classical FO-based treatment that covers recursion.
Approach
Translate programs with aggregates into extended many-sorted FO sentences where set-valued aggregate elements are represented by intensional function symbols; a new double-negation connective captures dlv's FLP semantics, and a transformation gamma maps Here-and-There formulas to classical FO, giving a classical-logic criterion for strong equivalence.
Key results
- The fo-clingo answer sets coincide with clingo answer sets, and fo-dlv answer sets coincide with dlv answer sets (Theorems on correspondence).
- Strong equivalence for clingo and for dlv is characterized by equivalence of agg-ht-models of the translated theories, and a classical FO sentence (with HT and AGG axioms) decides strong equivalence.
- Example: two rules with aggregates are strongly equivalent under dlv but not under clingo, showing the semantics differ on recursive/non-positive aggregates.
Surprising findings
- Two programs with non-positive aggregates that are strongly equivalent under dlv are not strongly equivalent under clingo.
- Double negation of a regular atom under the ht-semantics is not equivalent to the standard negation-of-negation, matching the FLP-reduct treatment.
Limitations
- Work is theoretical; no implementation of the classical-logic verification tool is presented.
- Restricted to aggregates with count and sum operations in the illustrations, with other aggregates only mentioned as extensions.
Experimental setup
Builds on: Abstract Gringo FLP reduct Quantified Here-and-There logic SM operator
Closest papers by meaning
- Axiomatization of Aggregates in Answer Set Programming (AAAI 2022 · similarity 0.94)
- A Unified View on Forgetting and Strong Equivalence Notions in Answer Set Programming (AAAI 2024 · similarity 0.90)
- Boolean Functions with Ordered Domains in Answer Set Programming (AAAI 2016 · similarity 0.89)
- On Equivalence and Inconsistency of Answer Set Programs with External Sources (AAAI 2017 · similarity 0.88)
- Strong Equivalence for Epistemic Logic Programs Made Easy (AAAI 2019 · similarity 0.87)
- On the Structural Hardness of Answer Set Programming: Can Structure Efficiently Confine the Power of Disjunctions? (AAAI 2024 · similarity 0.86)
Writing a paper in this area? scime draft is a free LaTeX editor with AI included, real-time co-authors and a check of your references and venue rules before you submit. It also imports OpenAI Prism projects.