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.
翻译:我们在问答设置程序(ASP)中全面阐述了可变即时或基础的理论基础。在ASP模型语言的语义基础上,我们引入了正式的基底算法(固定点)操作员特征描述。一个主要作用是,有专门基础的操作员,其相关模型提供语义指导,用于分解地面和在空中简化的结果。我们处理的是一个表达式逻辑程序类别,它包含循环总合,因此相当于现有ASP模型语言的范围。同时,我们还有一个简单的算法框架,详细描述循环总合的基底。给定的算法基本上与ASP地面格朗戈所使用的算法相对应。