On the Foundations of Grounding in Answer Set Programming
This work provides foundational theory for ASP grounding, which is incremental as it formalizes and extends existing methods for a specific domain.
The paper tackles the problem of formalizing grounding algorithms in Answer Set Programming (ASP) by introducing a theoretical framework based on fixed-point operators and well-founded models, specifically addressing recursive aggregates. It results in a detailed algorithmic framework that aligns with existing tools like gringo.
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.