On the Foundations of Grounding in Answer Set Programming

TL;DR

This paper rigorously analyzes the theoretical underpinnings of grounding in Answer Set Programming, introducing formal models and algorithms for recursive aggregates, aligning with practical ASP grounders.

Contribution

It offers a formal characterization of grounding algorithms in ASP using fixed point operators and extends the framework to recursive aggregates.

Findings

Provides a formal semantics for grounding in ASP.

Introduces algorithms for grounding recursive aggregates.

Aligns theoretical models with practical ASP grounders like gringo.

Abstract

We provide a comprehensive elaboration of the theoretical foundations of variable instantiation, or grounding, in Answer Set Programming (ASP). Building on the semantics of ASP's modeling language, we introduce a formal characterization of grounding algorithms in terms of (fixed point) operators. A major role is played by dedicated well-founded operators whose associated models provide semantic guidance for delineating the result of grounding along with on-the-fly simplifications. We address an expressive class of logic programs that incorporates recursive aggregates and thus amounts to the scope of existing ASP modeling languages. This is accompanied with a plain algorithmic framework detailing the grounding of recursive aggregates. The given algorithms correspond essentially to the ones used in the ASP grounder gringo.