Towards a Semantics for Hybrid ASP systems

TL;DR

This paper develops a formal semantic framework for hybrid Answer Set Programming (ASP) systems, addressing the challenge of capturing complex constructs and inferences in real-world applications.

Contribution

It introduces abstract and structured theories to formally characterize the semantics of hybrid ASP systems and applies this to CLINGO's framework.

Findings

Semantic characterization of CLINGO's theory-reasoning framework

Formal correspondence to the logic of Here-and-there with constraints

Elaboration of properties of hybridizations like CLINGCON, CLINGOM[DL], CLINGO[LP]

Abstract

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].