Answer set programming (ASP) is an efficient problem-solving approach, which has been strongly supported both scientifically and technologically by several solvers, ongoing active research, and implementations in many different fields. However, although researchers acknowledged long ago the necessity of epistemic operators in the language of ASP for better introspective reasoning, this research venue did not attract much attention until recently. Moreover, the existing epistemic extensions of ASP in the literature are not widely approved either, due to the fact that some propose unintended results even for some simple acyclic epistemic programs, new unexpected results may possibly be found, and more importantly, researchers have different reasonings for some critical programs. To that end, Cabalar et al. have recently identified some structural properties of epistemic programs to formally support a possible semantics proposal of such programs and standardise their results. Nonetheless, the soundness of these properties is still under debate, and they are not widely accepted either by the ASP community. Thus, it seems that there is still time to really understand the paradigm, have a mature formalism, and determine the principles providing formal justification of their understandable models. In this paper, we mainly focus on the existing semantics approaches, the criteria that a satisfactory semantics is supposed to satisfy, and the ways to improve them. We also extend some well-known propositions of here-and-there logic (HT) into epistemic HT so as to reveal the real behaviour of programs. Finally, we propose a slightly novel semantics for epistemic ASP, which can be considered as a reflexive extension of Cabalar et al.'s recent formalism called autoepistemic ASP.

Defined by Gelfond in 1991 (G91), epistemic specifications (or programs) are an extension of logic programming under stable models semantics that introduces subjective literals. A subjective literal allows checking whether some regular literal is true in all (or in some of) the stable models of the program, being those models collected in a set called world view. One epistemic program may yield several world views but, under the original G91 semantics, some of them resulted from selfsupported derivations. During the last eight years, several alternative approaches have been proposed to get rid of these self-supported world views. Unfortunately, their success could only be measured by studying their behaviour on a set of common examples in the literature, since no formal property of "self-supportedness" had been defined. To fill this gap, we extend in this paper the idea of unfounded set from standard logic programming to the epistemic case. We define when a world view is founded with respect to some program and propose the foundedness property for any semantics whose world views are always founded. Using counterexamples, we explain that the previous approaches violate foundedness, and proceed to propose a new semantics based on a combination of Moore's Autoepistemic Logic and Pearce's Equilibrium Logic. The main result proves that this new semantics precisely captures the set of founded G91 world views.

We present a SAT-based approach for solving the modal logic S5-satisfiability problem. That problem being NP-complete, the translation into SAT is not a surprise. Our contribution is to greatly reduce the number of propositional variables and clauses required to encode the problem. We first present a syntactic property called diamond degree. We show that the size of an S5-model satisfying a formula phi can be bounded by its diamond degree. Such measure can thus be used as an upper bound for generating a SAT encoding for the S5-satisfiability of that formula. We also propose a lightweight caching system which allows us to further reduce the size of the propositional formula.We implemented a generic SAT-based approach within the modal logic S5 solver S52SAT. It allowed us to compare experimentally our new upper-bound against previously known one, i.e. the number of modalities of phi and to evaluate the effect of our caching technique. We also compared our solver againstexisting modal logic S5 solvers. The proposed approach outperforms previous ones on the benchmarks used. These promising results open interesting research directions for the practical resolution of others modal logics (e.g. K, KT, S4)