  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.
