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