# Comparing the Reasoning Capabilities of Equilibrium Theories and Answer Set Programs
## 1 Introduction  
Answer Set Programming (ASP) is a popular environment for knowledge representation and problem solving in artificial intelligence. Thanks to efficient answer set solvers, there are now many applications of this technique in diverse domains. Equilibrium logic [1] provides a logical foundation for ASP and extends the stable model semantics to arbitrary propositional and first order theories. It has also proved instrumental in generating novel extensions for temporal and epistemic reasoning under answer set semantics. Answer set programs are typically employed to provide one or more representations of problem solutions in the form of models or answer sets. Unlike Prolog, ASP was not traditionally designed to be used as a query answering system. Accordingly, the study of logical relations between programs, beginning with [2], has focused mainly on a comparison of their answer sets. This is how the principle relations of strong and uniform equivalence as well as their relativised and projective versions are understood [2, 3, 4, 5]. Strong and uniform equivalence were first considered in the Datalog domain [6, 7]; since then, many nonmonotonic formalisms have been investigated in this regard, including default logic [8], causal logics [9], argumentation frameworks [10, 11], and preference-based formalisms [12, 13, 14], to mention just a few examples. Results on strong equivalence and related notions have proved to be useful in many different contexts, such as program simplification [15] or forgetting [16]. Nevertheless, query answering is important in a number of domains where ASP can be applied. In such cases, we are interested in comparing the logical consequences of differentprograms, to see, for example, under what conditions they agree in their answering of queries. This motivates the challenge of defining and analysing equivalence and entailment relations between programs that are formulated in terms of inference and query answering. Similar notions turn up in other logic-based reasoning systems. In Datalog, there is the well-known concept of _query containment_[17]. In description logics for reasoning over ontologies, there is the concept of _query inseparability_ (see e.g., [18]); similarly, in abstract argumentation, strong equivalence with respect to _argument acceptance_ has been investigated [11]. In ASP, two programs are said to be _equivalent_ if they have the same stable models and _strongly equivalent_ if they remain equivalent under the addition of any new set of rules [2]. If only new facts can be added, the relation is known as _uniform equivalence_. Furthermore, _relativised_ versions of strong and uniform equivalence can be defined to cover the case that the newly added rules or facts are in a specific language. _Projective_ equivalence is the appropriate concept in case we are interested in model equivalence with respect to a restricted sublanguage of the programs. All these relations have been studied and characterised in the literature (as cited above). In [19], weak and strong forms of _entailment_ between programs were also defined and analysed. In this case, we are concerned with the relative _strength_ of theories. In the rest of the article, we formulate new intertheory and inter-program relations based on inference and show that, in most cases, they coincide with their well-known model-theoretic counterparts. This means that they can be studied using familiar concepts and techniques. We work throughout in the non-classical logic **HT** of _here-and-there_, which provides a basis for equilibrium logic and hence for the stable model semantics of ASP. **HT** is of particular importance in this context due to the way in which **HT** models relate to theory equivalences. In Section 2, we recall the basic features of **HT** and equilibrium logic, and we define three types of consequence relations for equilibrium theories. Section 3 deals with strong and uniform equivalence relations, showing how the standard notions compare with their counterparts formulated in terms of inference.