Over the last decades the development of ASP has brought about an expressive modeling language powered by highly performant systems. At the same time, it gets more and more difficult to provide semantic underpinnings capturing the resulting constructs and inferences. This is even more severe when it comes to hybrid ASP languages and systems that are often needed to handle real-world applications. We address this challenge and introduce the concept of abstract and structured theories that allow us to formally elaborate upon their integration with ASP. We then use this concept to make precise the semantic characterization of CLINGO's theory-reasoning framework and establish its correspondence to the logic of Here-and-there with constraints. This provides us with a formal framework in which we can elaborate formal properties of existing hybridizations of CLINGO such as CLINGCON, CLINGOM[DL], and CLINGO[LP].
翻译:在过去几十年中,ASP的发展带来了一种由高度性能强的系统驱动的显性模型语言。与此同时,越来越难以提供能够捕捉由此产生的构造和推论的语义基础。当涉及到处理现实世界应用经常需要的混合的ASP语言和系统时,这甚至更为严重。我们应对这一挑战,并引入抽象和结构化理论的概念,使我们能够正式阐明这些语言与ASP的融合。然后我们利用这一概念来精确地描述CLINGO理论理论框架的语义特征,并确立其与“内外”逻辑的对应性。这为我们提供了一个正式的框架,我们可以在这个框架内阐述CLingCon、CLingOM[DL]和CLINGO[LP]等CLingO现有混合化的正式特性。