Axiomatization of Aggregates: Extended Abstract

This paper presents semantics for logic programs with aggregates that refer to neither fixpoints nor grounding, relying instead on transformations into first and second-order theories. This characterization introduces new function symbols to represent aggregates, whose meaning can be fixed by adding appropriate axioms to the result of the proposed transformations. These semantics provide a foundation for reasoning formally about non-ground programs with aggregates in a direct manner. This is useful for the task of formally verifying logic programs, and represents a first step towards using first-order theorem provers to automatically verify properties of programs with aggregates. For programs without positive recursion through aggregates our semantics coincide with the semantics of the answer set solver Clingo.