Logic programs with propositional connectives and aggregates

TL;DR

This paper introduces a new, simple, and expressive semantics for aggregates in answer set programming by drawing an analogy with propositional connectives, extending answer set semantics to arbitrary propositional theories.

Contribution

It proposes a novel approach to defining aggregates in ASP based on propositional connectives, extending answer set semantics to arbitrary propositional theories.

Findings

Defines aggregates as primitive constructs and formulas

Inherits theorems about strong equivalence and splitting

Offers a semantics balancing expressiveness and simplicity

Abstract

Answer set programming (ASP) is a logic programming paradigm that can be used to solve complex combinatorial search problems. Aggregates are an ASP construct that plays an important role in many applications. Defining a satisfactory semantics of aggregates turned out to be a difficult problem, and in this paper we propose a new approach, based on an analogy between aggregates and propositional connectives. First, we extend the definition of an answer set/stable model to cover arbitrary propositional theories; then we define aggregates on top of them both as primitive constructs and as abbreviations for formulas. Our definition of an aggregate combines expressiveness and simplicity, and it inherits many theorems about programs with nested expressions, such as theorems about strong equivalence and splitting.