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

2024/12/14 by Jorge Fandinno, Fandinno, Jorge, Zachary Hansen +1 · 1 citation
Computer Science · Social Sciences · #Access Control and Trust #Artificial Intelligence (cs.AI) #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Multi-Agent Systems and Negotiation

paper · pdf · doi:10.48550/arxiv.2412.10975

openalex publication_date 2024/12/14 · openalex created_date 2024/12/18 · openalex updated_date 2026/07/28

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.

Cited by

• Deductive Systems for Logic Programs with Counting

Related

• Functional ASP with Intensional Sets: Application to Gelfond-Zhang Aggregates
• Logic programs with propositional connectives and aggregates
• An Unfolding-Based Semantics for Logic Programming with Aggregates
• A Constructive Semantic Characterization of Aggregates in ASP
• Aggregate Semantics for Propositional Answer Set Programs