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

Fuente: arXiv
Saved in:
Bibliographic Details
Main Authors: Fandinno, Jorge, Hansen, Zachary
Format: Preprint
Published: 2024
Subjects:
Online Access:
Tags: Add Tag
No Tags, Be the first to tag this record!
_version_ 1866916523664211968
author Fandinno, Jorge
Hansen, Zachary
author_facet Fandinno, Jorge
Hansen, Zachary
contents 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.
format Preprint
id arxiv_https___arxiv_org_abs_2412_10975
institution arXiv
publishDate 2024
record_format arxiv
spellingShingle Recursive Aggregates as Intensional Functions in Answer Set Programming: Semantics and Strong Equivalence
Fandinno, Jorge
Hansen, Zachary
Artificial Intelligence
Logic in Computer Science
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.
title Recursive Aggregates as Intensional Functions in Answer Set Programming: Semantics and Strong Equivalence
topic Artificial Intelligence
Logic in Computer Science
url https://arxiv.org/abs/2412.10975