Top-down Splitting Property for Epistemic Logic Programs Stefania Costantini1 1 DISIM - Università dell’Aquila, Italy Abstract In this paper we consider Epistemic Logic Programs (ELPs), which extend Answer Set Programming (ASP) with “epistemic operators”. There are several approaches to the semantics of such programs in terms of World Views, which are sets of belief sets. Recent work has proposed an analysis of the structure of ELPs in terms of a concept of “splitting”, in order to be able to modularly compute their semantics in a bottom-up fashion, analogously to ‘traditional’ ASP. The proposal is brilliant but the problem is, that few of the semantics that have been proposed so far enjoy this new “Epistemic Splitting Property”. Thus, the notion of modular computation of world views does not work for most of the cases. We analyse the possibility to change the perspective about how to exploit a splitting, shifting from a bottom-up to a top-down approach. Our new definition: (i) copes with concerns regarding, e.g. “unfoundedness” of world views and “subjective constraint monotonicity”; (ii) is applicable to many of the existing semantics; (iii) coincides with the bottom-up notion of splitting on a significant class of programs. Keywords Answer Set Programming, Epistemic Logic Programs, Epistemic Splitting 1. Introduction In this paper we discuss Epistemic Logic Programs (first introduced in [1, 2]), that extend Answer Set Programs with introspective capabilities, where Answer Set Programming (ASP) [3] is a successful logic programming paradigm under the answer set semantics (AS) [4, 5]. As it can be found in the wide corpus of existing literature concerning ASP (cf., among many, [6, 7, 8, 9] and the references therein), this programming paradigm has encountered a remarkable success, and has been applied in many fields, e.g., information integration, constraint satisfaction, routing, planning, diagnosis, configuration, computer-aided verification, biology/biomedicine, knowledge management, etc. The approach to problem-solving proper of ASP consists in the following conceptually distinct steps: (i) encoding of the given problem via an ASP program; (ii) computing the “answer sets” of such a program via an inference engine, or “ASP solver” (many solvers are freely available, cf. [10]); (iii) extracting the problem solutions from the answer sets. Epistemic Logic programs (ELPs, in the following just ‘programs’ if not explicitly stated differently), extend ASP with epistemic operators that are able to introspectively “look inside” a program’s own semantics, which is defined in terms of its answer sets. In fact, K𝐴 means 14th Workshop on Answer Set Programming and Other Computing Paradigms " stefania.costantini@univaq.it (S. Costantini)  0000-0002-5686-6124 (S. Costantini) © 2021 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). CEUR Workshop Proceedings http://ceur-ws.org ISSN 1613-0073 CEUR Workshop Proceedings (CEUR-WS.org) that (ground) atom 𝐴 is true in every answer set of the very program Π where K𝐴 occurs, whereas M𝐴 means that 𝐴 is true in some of the answer sets of Π. The epistemic negation operator not 𝐴 expresses that 𝐴 is not provably true, meaning that 𝐴 is false in at least one answer set of Π. Epistemic operators, that form subjective literals, are interchangeable, in fact K𝐴 and M𝐴 can be rephrased as 𝑛𝑜𝑡 not 𝐴 and not 𝑛𝑜𝑡 𝐴, respectively (where 𝑛𝑜𝑡 is ASP standard ‘default negation’) while not 𝐴 can be rephrased as 𝑛𝑜𝑡 K𝐴. Consequently, in discussing the semantics of ELPs, many approaches consider explicitly only the operator K (as it is done here), while some approaches, primarily [11], consider explicitly only the operator not. Semantics of ELPs is provided in terms of World Views: instead of a unique set of answer sets like in ASP, there is now a set of such sets. Each world view consistently satisfies (according to a given semantics) the epistemic expressions that appear in a given program. Many semantic approaches/characterizations for ELPs have been introduced beyond the seminal one of [1, 2], among which [12, 13, 14, 11, 15, 16, 17, 18, 19]. Their aim is essentially to avoid world views which are ‘unintended’ with respect to a given program, and to compute the world views that appear ‘intuitively adequate’. Some approaches also propose extensions to the basic paradigm. ELP solving systems (for some specific semantics) have been defined and implemented [20, 21, 22, 23, 24] on top of state-of-the-art ASP solvers, that are invoked (more than once) to generate and check potential world views. Recent work presented in [18, 19, 25, 26, 27] has been aimed to extend to Epistemic Logic Programming notions which have been previously defined for ASP. Primarily, they consider splitting (introduced for ASP by [28]), which allows a program to be divided into parts in a principled way, so that the answer sets can be computed incrementally, starting from the answer sets of the bottom part, used to simplify the top part w.r.t. them, and then compute the answer sets of the simplified top part (such procedure can be iterated for as many levels as the program has been divided into, i.e., the top and the bottom could be split recursively). So, these works try first of all to extend the concept of splitting and the method of incremental calculation of the semantics (here, it is the world views that must be calculated). They thus define a notion of Epistemic Splitting, where top and bottom are defined w.r.t. the occurrence of subjective literals, and a corresponding property, which is respected by a semantics if it allows the world views to be computed bottom up (a precise definition is seen below). They then adapt to ELPs other properties of ASP, namely the fact that adding constraints leads to reduce the number of answer sets (Constraint Monotonicity, implied by the Epistemic Splitting Property), and Foundedness, meaning that atoms composing answer sets cannot have been derived through cyclic positive dependencies. They also define the class of Epistemically Stratified Programs, that admit a unique world view. The aim of this line of work is to extend to ELPs such properties because they have turned out to be convenient for ASP, where many useful results have stemmed from them. So, the authors believe that they might prove useful in ELPs as well. The problem is, virtually none of the semantics existing in the literature obeys these properties, except the original one of [2], and the authors’ own one, first presented in [25], called FAEEL, which has however been developed with these properties in mind. We believe that the approach of [18, 19, 25, 26, 27] is the correct one to examine ELPs: rather than defining ‘yet-another-semantics’, they establish properties that a semantics should fulfil, and then they compare the existing semantics with respect to these properties (and the same can be done for possible future new semantics). The introduction of a notion of epistemic splitting is brilliant, and highly useful. So, we have no intention whatsoever to argue against the work of Cabalar et al., which we found inspiring. Only, in our opinion it cannot be said that, apart from those in [2, 25], all the other semantics presented in the literature deliver unreasonable results. Without denying the potential practical utility of the properties proposed therein, we only tried to take a different stance, on the basis of the notion of epistemic splitting. Our Contributions: 1. We considered the original splitting property in ASP, defined by Lifschitz and Turner in [28] (say, L&T splitting); it is not by its very nature an operational notion, yet it has been procedurally adopted for iterative answer sets computation (cf., e.g., [29, 30, 31, 32]). We noticed that L&T splitting can be exploited to this aim both bottom-up (as commonly done) but also in a top-down way: in fact, a splitting set 𝑈 for program Π defines a ‘bottom’ program, composed solely of atoms of 𝑈 , and a ‘top’ program, where atoms from 𝑈 can occur only on the body of rules. (Note that, the top part can be in turn split, over a number of layers). In a bottom-up fashion, basically, any layer can compute its answer sets given the answer sets of the lower layer(s), that allow truth values to be assigned to literals referring the that layer (literals involving “lower atoms”). In a top-down fashion, every layer could make all possible hypotheses about truth values of the set of lower atoms; it would calculate its own answer sets according to each hypothesis, and then discard answer sets deriving from those hypotheses not matching the actual answer sets of the lower layer, when they become known. This method is clearly somehow impractical, yet feasible; it is potentially useful in forms of modular programming, where a top part defining general (e.g., ontological) useful properties might be combined ‘on demand’ with any bottom part. It is easy to see that the bottom-up and top-down processes provide identical results. 2. We observed that every occurrence of a subjective literal is an act of introspection aimed to inspect, but also potentially to influence, the set of consequences which are derivable, and we considered that such influence, in order to be “global”, should spread bottom-up. 3. We take as granted the notion of Epistemic Splitting to subdivide the program into layers, but we then define an alternative process of incremental computation of world views, which operates top-down instead of bottom-up. 4. Our results: we prove that the proposed method of Top-Down Epistemic Splitting returns the world views that are computed by some of the most significant semantics proposed in the literature, and makes the problem of unfoundedness immaterial. The method is orthogonal to bottom-up Epistemic Splitting, and provides coincident results on the class of Epistemically Stratified Programs. 5. Our conclusions: we show that not only FAEEL but also other semantics produce their results in a principled way, and obey useful properties; both methods (bottom-up and top-down) for exploiting the splitting of ELPs may have their merits, that will have to be evaluated on practical applications. Such evaluation will be the subject of future work. The paper is organized as follows. In Sections 2–3 we recall Answer Set Programming and Epistemic Logic Programs (we assume a basic knowledge on logic programming and its declarative and procedural semantics as illustrated in standard textbooks, e.g., [33]). In Section 4 we provide background on the proposal by [18, 19, 25, 26, 27]. In Section 5 we introduce some observations on ELPs that will lead to formulate our proposal, that we discuss in Section 6. Finally, in Section 7 we conclude. 2. Answer Set Programming (ASP) and Answer Set semantics In ASP, one can see an answer set program (for short ‘ASP program’) as a set of statements that specify a problem, where each answer set represents a solution compatible with this specification. Whenever an ASP program has no answer sets (no solution can be found), it is said to be inconsistent, otherwise it is said to be consistent. Several well-developed freely available answer set solvers exist [6], that compute the answer sets of a given program. Syntactically, an ASP program Π is a collection of rules of the form 𝐴1 | . . . |𝐴𝑔 ← 𝐿1 , . . . , 𝐿𝑚 , 𝑛𝑜𝑡 𝐴𝑚+1 , . . . , 𝑛𝑜𝑡 𝐴𝑛 . where each 𝐴𝑖 , 𝑖 ≤ 𝑔, is an atom and | indicates disjunction (that can be alternatively indicated as ∨), and the 𝐿𝑖 s, 𝑖 ≥ 𝑛, 𝑚, 𝑛 ⩾ 0, are literals (i.e., atoms or negated atoms). The left-hand side and the right-hand side of the rule are called head and body, respectively. A rule with empty body is called a fact. Notation 𝐴 | 𝐵 indicates disjunction, usable only in rule heads and, so, in facts. A rule with empty head (or, equivalently, with head ⊥), of the form ‘← 𝐿1 , ..., 𝐿𝑛 .’ or ‘⊥ ← 𝐿1 , ..., 𝐿𝑛 .’, is a constraint, stating that literals 𝐿1 , . . . , 𝐿𝑛 are not allowed to be simultaneously true in any answer set; the impossibility to fulfil such requirement is one of the reasons that make a program inconsistent. All features of ASP not explicitly mentioned above are, for the sake of simplicity, not considered in this paper. As it is customary in the ASP literature, we implicitly refer to the “ground” version of Π, which is obtained by replacing in all possible ways the variables occurring in Π with the constants occurring in Π itself, and is thus composed of ground atoms, i.e., atoms which contain no variables. The answer set (or “stable model”) semantics (AS) can be defined in several ways (see, for instance, [34] or also [35]). However, answer sets of a program Π, if any exists, are the supported minimal classical models of the program interpreted as a first-order theory in the obvious way. The original definition by [4], introduced for programs where rule heads were limited to be single atoms, was in terms of the ‘GL-Operator’ Γ. Given set of atoms 𝐼 and program Π, ΓΠ (𝐼) is defined as the least Herbrand model of Π𝐼 , called the (Gelfond-Lifschitz) ‘reduct’ of Π w.r.t. 𝐼; Π𝐼 is positive program, so, its least Herbrand model can be computed via the standard immediate consequence operator (cf. [33]). Π𝐼 is obtained from Π by: 1. removing all rules which contain a negative literal 𝑛𝑜𝑡 𝐴 such that 𝐴 ∈ 𝐼; and 2. removing all negative literals from the remaining rules. Then, 𝐼 is an answer set whenever ΓΠ (𝐼) = 𝐼. 3. Epistemic Logic Programs Epistemic Logic Programs (ELPs), introduced in [1], allow one to express within ASP programs so-called subjective literals (in addition to objective literals, that are those that can occur in ‘plain’ ASP programs, plus the truth constants ⊤ and ⊥). Such new literals are constructed via the epistemic operator K (disregarding without loss of generality the other epistemic operators): K𝐴 means that (ground) atom 𝐴 is true in every answer set of given program Π (it is a so-called cautious consequence of Π). The syntax of rules is analogous to ASP, save that literals can now be either objective or subjective, where subjective literals are allowed to appear (only) in the body of rules. Nesting of subjective literals is not considered here. An ELP program is called objective if no subjective literals occur therein, i.e., it is an ASP program. A constraint involving (also) subjective literals is called a subjective constraint, where one involving objective literals only is an objective constraint. Let 𝐴𝑡 be the set of atoms occurring (within either objective or subjective literals) in a given program Π, and Atoms(𝑟) be the set of atoms occurring in rule 𝑟 in Π. Let Head(𝑟) be the head of rule 𝑟, Body_obj(𝑟) be the (possibly empty) set of objective literals occurring in the body of rule 𝑟, and Body_subj(𝑟) be the (possibly empty) set of subjective literals occurring in the body of rule 𝑟. We call subjective rules those rules whose body is composed of subjective literals only. The semantics of ELPs is based on the notion of World Views: for a given program, instead of a set of answer sets like in ASP, there is now a set of such sets. Each one, called “world view”, consistently satisfies all subjective literals occurring in the program. Take for instance program {𝑎 ← 𝑛𝑜𝑡 𝑏, 𝑏 ← 𝑛𝑜𝑡 𝑎, 𝑒 ← 𝑛𝑜𝑡 K𝑓, 𝑓 ← 𝑛𝑜𝑡 K𝑒}. Under every semantics, there are two world views: {{𝑎, 𝑒}, {𝑏, 𝑒}}, where K𝑒 is true and K𝑓 false, and {{𝑎, 𝑓 }, {𝑏, 𝑓 }} where K𝑓 is true and K𝑒 false. Notice that the presence of two answer sets in each world view is due to the cycle on objective atoms, whereas the presence of two world views is due instead to the cycle on subjective atoms (c.f. [36] for a discussion). 4. Epistemic Logic Programs: useful Properties As argued in [25] and [26], it would be useful if ELPs would enjoy (‘mutatis mutandis’) properties similar to those of ASP programs. So, in these works such useful properties are outlined and adapted, as we report (almost literally) below. To begin with, since several semantics for ELPs have been proposed, it is useful to abstract away from the specific semantic definition. Definition 4.1. [Slightly modified version of Definition 1 in [26] (Abstract semantics)] An (ab- stract) semantics 𝒮 is a function mapping each program into sets of ‘belief views’, i.e., sets of sets of objective literals, where if Π is an objective program, then 𝒮(Π) is the set of stable models of Π. Given a program Π, each belief view in 𝒮(Π) is called a 𝒮-world view of Π. Drawing inspiration from the Splitting Theorem introduced in [28], which defines a subdivision of ASP programs into layers so as to be able compute the answer sets incrementally, an analogous properties is defined for ELPs. Definition 4.2. [Reported from Definition 2 in [26] (Epistemic splitting set)] A set of atoms 𝑈 ⊆ 𝐴𝑡 is said to be an epistemic splitting set of given program Π if for any rule 𝑟 in Π one of the following conditions hold: (i) Atoms(𝑟) ⊆ 𝑈 , (ii) (Body_obj(𝑟) ∪ Head(𝑟)) ∩ 𝑈 = ∅. An epistemic splitting of Π is a pair ⟨𝐵𝑈 (Π), 𝑇𝑈 (Π)⟩ satisfying 𝐵𝑈 (Π) ∩ 𝑇𝑈 (Π) = ∅ (meaning that they have no rules in common), 𝐵𝑈 (Π) ∪ 𝑇𝑈 (Π) = Π, and also that all rules in 𝐵𝑈 (Π) satisfy (i) and all rules in 𝑇𝑈 (Π) satisfy (ii). Intuitively, the second condition means that the top program may refer to atoms 𝑈 which occur as heads of rules in the bottom, only through epistemic operators. Epistemic splitting can be used, similarly to ‘traditional’ L&T splitting, for iterative computa- tion of world views. In the case of ELPs, [25] proposes to compute first the world views of the bottom program 𝐵𝑈 (Π) and, for each one of them, simplify the corresponding subjective literals in the top part. Given an epistemic splitting set 𝑈 for a program Π and a set of interpretations 𝑊 , they define the subjective reduct of the top with respect to 𝑊 and signature 𝑈 , called 𝐸𝑈 (Π, 𝑊 ). This operator, according to [25], considers all subjective literals 𝐿 occurring in 𝑇𝑈 (Π), such that the atoms occurring in them belong to 𝐵𝑈 (Π). In particular, 𝐿 will be substituted by ⊤ in 𝐸𝑈 (Π, 𝑊 ) if 𝑊 |= 𝐿, and by ⊥ otherwise. So, 𝐸𝑈 (Π, 𝑊 ) is a version of 𝑇𝑈 (Π) where some subjective literal, namely those referring to the bottom part of the program, have been simplified as illustrated. Definition 4.3 (Reported from Definition 3 in [26]). Given a semantics 𝒮, a pair ⟨𝑊𝑏 , 𝑊𝑡 ⟩ is said to be an 𝒮-solution of Π with respect to an epistemic splitting set 𝑈 if 𝑊𝑏 is a 𝒮-world view of 𝐵𝑈 (Π) and 𝑊𝑡 is a 𝒮-world view of 𝐸𝑈 (Π, 𝑊𝑏 ). The definition is parametric w.r.t. 𝒮, as each different semantics 𝒮 will define in its own way the 𝒮-solutions for a given 𝑈 and Π, . So, world views of the entire program will be obtainable by suitably combining some world view of the bottom with some world view of the top, i.e., the world views of the entire program should be obtained as (where 𝐼𝑏 and 𝐼𝑡 are answer sets occurring respectively in 𝑊𝑏 and 𝑊𝑡 ): 𝑊𝑏 ⊔ 𝑊𝑡 = {𝐼𝑏 ∪ 𝐼𝑡 |𝐼𝑏 ∈ 𝑊𝑏 ∧ 𝐼𝑡 ∈ 𝑊𝑡 } Therefore, Property 4.1. [Property 1 in [26] (Epistemic Splitting Property)] A semantics 𝒮 satisfies epis- temic splitting if, for any epistemic splitting set 𝑈 of any given program Π: 𝑊 is an 𝒮-world view of Π iff there is an 𝒮-solution ⟨𝑊𝑏 , 𝑊𝑡 ⟩ of Π with respect to 𝑈 such that 𝑊 = 𝑊𝑏 ⊔ 𝑊𝑡 . As discussed at length in [25], some semantics satisfy epistemic splitting, and some others do not. Actually, most semantics do not satisfy this property, which is satisfied only in: the very first semantics of ELPs, proposed in [1] (and in some of its generalizations), and in Founded Autoepistemic Equilibrium Logic (FAEEL), introduced in [18]. The property of epistemic splitting implies subjective constraint monotonicity [19, 26]. I.e., if a semantics 𝒮 satisfies epistemic splitting then for any epistemic program Π and any subjective constraint 𝑟, 𝑊 is a world view of Π ∪ {𝑟} iff both 𝑊 is a world view of Π and 𝑊 satisfies 𝑟. Another property considered in [27] is foundedness, again extended from objective programs. A set 𝑋 of atoms is unfounded w.r.t. program Π and interpretation 𝐼, if for every 𝐴 ∈ 𝑋 there is no rule of 𝑟 by which 𝐴 might be derived, without incurring in positive circularities and without forcing the derivation of more than one atom from the head of a disjunctive rule. For ELPs, [27] adds the condition that positive dependencies are also those on positive subjective literals, like, e.g., in program 𝐴 ← K𝐴. Then, a world view for ELP Π will be founded if there is no composing interpretations 𝐼ˆ which contains an unfounded set w.r.t. Π and 𝐼ˆ. It turns out that, among existing semantics, only FAEEL satisfy foundedness. 5. Our Observations and Proposal The subdivision of an ELP into layers as defined in [25, 26, 27] suggests that, in the upper layer, epistemic literals referring to the lower layer may be aimed to perform some kind of meta-reasoning about that layer. In the aforementioned approach however, meta-level reasoning is in practice prevented, as it is the lower layer that decides the truth value of the subjective literals that connect the two layers. In fact, according to the epistemic splitting property as defined in [26], through the simplification w.r.t. the answer sets of the lower layer, the upper layer is strongly (maybe sometimes too strongly) constrained. We can see that for instance, for program Π0 𝑎 ∨ 𝑏, 𝑐 ← K𝑎, ← 𝑛𝑜𝑡 𝑐, that once one has computed the unique world view of the lower level 𝑎 ∨ 𝑏 considered as a program ‘per se’, i.e., {{𝑎}, {𝑏}}, then the overall program has no world views: in fact, under this world view K𝑎 does not hold and so 𝑐 is false, violating the constraint. The world view {{𝑎, 𝑐}}, returned instead by semantics such as [12, 11], does not fulfil the epistemic splitting property. This world view may however be seen as corresponding to an approach where the upper layer, in order to retain consistency, ‘requires’ the lower layer to entail 𝑎, which is absolutely feasible by choosing 𝑎 over 𝑏 in the disjunction. We follow (since a long time) the line, amply represented in the literature, in which meta- reasoning is aimed in general not only at ‘observing’ the lower layers, but also at trying to influence them (cf., e.g., [37] for a survey on the subject). So, we tried to look at the matter from another point of view, to understand whether the concept of splitting might be applied top-down, and how the existing semantics would behave in the new perspective. In our approach, the notion of splitting set remains the same, save for one detail. As noticed in [25], subjective constraints, and rules without objective literals in their body, according to the definition might be placed at either level. For convenience concerning definitions that will be introduced later, we impose the additional condition: Definition 5.1 (Subjective rules and Constraints in Epistemic Splitting). Given an epistemic splitting ⟨𝐵𝑈 (Π), 𝑇𝑈 (Π)⟩ of a given program Π, subjective rules satisfying condition (ii) of the definition above, and subjective constraints, are put in 𝑇𝑈 (Π). Let us proceed step by step to the new definition of Top-down Epistemic Splitting Property (TDESP for short). As in the aforementioned previous work, we consider only the epistemic operator K. Let us consider an epistemic splitting of given program Π as a pair ⟨𝐵𝑈 (Π), 𝑇𝑈 (Π)⟩ according to Definition 4.2. Let us, also, consider a semantics 𝒮 as given. Definition 5.2 (Epistemic top-down Constraint set and Requirement set). The Epistemic top- down subjective constraint set and the Requirement set concerning the world views of 𝑇𝑈 (Π) (obtained according to 𝒮) are obtained as follows. • Build from 𝑇𝑈 (Π) the new program 𝑇𝑈′ (Π) in the following way: – take the subjective literals K𝐿1 , . . . , K𝐿𝑧 occurring in 𝑇𝑈 (Π) but referring to 𝐵𝑈 (Π), in the sense that atoms involved therein occur in 𝐵𝑈 (Π) but not in 𝑇𝑈 (Π); – transform such literals into fresh atoms, 𝑘𝑙1 , . . . , 𝑘𝑙𝑧 (keeping track of the correspon- dence); – for each of the 𝑘𝑙𝑖 s, add new fact 𝑘𝑙𝑖 | 𝑛𝑜𝑡 𝑘𝑙𝑖 to 𝑇𝑈 (Π). • Given the world views 𝑊1′ , . . . , 𝑊𝑘′ of 𝑇𝑈′ (Π), for each such world view 𝑊 ′ , identify the sets 𝑆1 = {𝑘𝑙1 , . . . , 𝑘𝑙𝑟 }, 𝑆2 = {𝑘𝑙𝑟+1 , . . . , 𝑘𝑙𝑠 } where: all elements of both 𝑆1 and 𝑆2 are true in all sets composing the world view (i.e., they are cautious consequences), and all elements of 𝑆1 are also directly or indirectly involved in a constraint in 𝑇𝑈′ (Π) (cf. [38] for a formal definition of direct and indirect dependencies). • Given the world views 𝑊1′ , . . . , 𝑊𝑘′ of 𝑇𝑈′ (Π), cancel the 𝑘𝑙𝑖 ’s and 𝑛𝑜𝑡 𝑘𝑙𝑗 ’s from their composing sets, thus obtaining world views 𝑊1 , . . . , 𝑊𝑘 for 𝑇𝑈 (Π) (after removing any empty set that might result, except if it is the only set composing the world view). • Given each of the world views 𝑊1 , . . . , 𝑊𝑘 of 𝑇𝑈 (Π), say 𝑊𝑖 , the (possibly empty) set {K𝐿1 , . . . , K𝐿𝑟 } i.e., {K𝐿𝑖 | 1 ≤ 𝑖 ≤ 𝑟 ∧ 𝑘𝑙𝑖 ∈ 𝑆1 } is called Epistemic top-down Constraint set, indicated as 𝐸𝐶𝑇𝑈 (Π) (𝑊𝑖 ). • Given each of the world views 𝑊1 , . . . , 𝑊𝑘 of 𝑇𝑈 (Π), say 𝑊𝑖 , the (possibly empty) set {K𝐿𝑟+1 , . . . , K𝐿𝑠 } i.e., {K𝐿𝑗 | 𝑟 + 1 ≤ 𝑗 ≤ 𝑠 ∧ 𝑘𝑙𝑗 ∈ 𝑆2 } is called Requirement set, indicated as 𝑅𝑄𝑇𝑈 (Π) (𝑊𝑖 ). The overall set 𝐸𝐶𝑅𝑄𝑇𝑈 (Π) (𝑊𝑖 ) = 𝐸𝐶𝑇𝑈 (Π) (𝑊𝑖 ) ∪ 𝑅𝑄𝑇𝑈 (Π)(𝑊𝑖 ) is called Requisite Set, as it expresses prerequisites, about which epistemic literals must be entailed in some world view of 𝐵𝑈 (Π), so that such world view can be merged with 𝑊𝑖 in order to obtain a world view of the overall program Π. We keep the two sets separate because, from a knowledge engineering point of view, it can be useful to distinguish literals in 𝐸𝐶𝑇𝑈 (Π) (𝑊𝑖 ), that if not entailed lead to a constraint violation and so to non-existence of a world view of Π containing 𝑊𝑖 , from literals in 𝑅𝑄𝑇𝑈 (Π) (𝑊𝑖 ), that instead correspond to mere assumptions. In case, given world view 𝑊 of 𝑇𝑈 (Π), literals belonging to 𝐸𝐶𝑅𝑄𝑇𝑈 (Π) (𝑊 ) occur in the bodies of rules in 𝐵𝑈 (Π), our approach enforces the ‘required’ truth value of such literals by means of the following simplification. Definition 5.3 (Top-down Influence). Given world view 𝑊 of 𝑇𝑈 (Π), and its corresponding requisite set 𝐸𝐶𝑅𝑄𝑇𝑈 (Π) (𝑊 ), the 𝑊 -tailored version 𝐵𝑈𝑊 (Π) of 𝐵𝑈 (Π) is obtained by substi- tuting in 𝐵𝑈 (Π) all literals K𝐴 ∈ 𝐸𝐶𝑅𝑄𝑇𝑈 (Π) (𝑊 ) by 𝐴. World views of given program Π will be obtained, similarly to what done for the bottom-up approach, from world views of the top and the bottom, but with two important differences (i) Top-down Influence; (ii) a subset of a world view of the bottom (i.e., some of the answer sets occurring therein) can be cut out, so as to be combined with a ‘compatible’ world view of the top. Definition 5.4 (Candidate World Views (CWWs)). A Candidate World View (CWW) 𝑊 for given program Π (w.r.t. a semantics 𝒮) is obtained as follows. Take a world view 𝑊𝑇 of 𝑇𝑈 (Π) and a subset 𝑊𝐵 of a world view of 𝐵𝑈𝑊𝑇 (Π) such that ∀ K𝐿 ∈ 𝐸𝐶𝑅𝑄𝑇𝑈 (Π) (𝑊𝑇 ), 𝑊𝐵 |= 𝐾𝐿. Then, from 𝑊𝑇 and 𝑊𝐵 , we have: 𝑊 = 𝑊𝐵 ⊔ 𝑊𝑇 = {𝐼𝑏 ∪ 𝐼𝑡 |𝐼𝑏 ∈ 𝑊𝐵 ∧ 𝐼𝑡 ∈ 𝑊𝑇 } Notice that, CWWs are computed after applying Top-down Influence. There can be the case that no subset of any world view of the bottom complies with the conditions posed by world views of the top; in this situation, Π has no candidate world views. Notice that the process can be iterated, in the sense that both 𝐵𝑈 (Π) and 𝑇𝑈 (Π) can in turn be split into a top and a bottom. Definition 5.5 (Top-down Epistemic Splitting Property (TDESP)). A semantics 𝒮 satisfies Top- down Epistemic Splitting if any candidate world view of Π according to Definition 5.4 is indeed a world view of Π under 𝒮. Let us experiment this methodology on some of the examples proposed in recent literature. Consider program Π1 , reported in [39]. 𝑝|𝑞 (𝑟1) ⊥ ← 𝑛𝑜𝑡 K𝑝 (𝐶) Here, 𝐵𝑈 (Π1 ) consists of rule (r1), and 𝑇𝑈 (Π1 ) of constraint (C). So, 𝑇𝑈′ (Π1 ) is (where 𝑘𝑝 is a fresh atom): 𝑘𝑝 | 𝑛𝑜𝑡 𝑘𝑝 ⊥ ← 𝑛𝑜𝑡 𝑘𝑝 (𝐶) whose unique world view is {{𝑘𝑝}}. After cancelling 𝑘𝑝, we obtain world view 𝑊𝑇 = {∅} for 𝑇𝑈 (Π1 ), where 𝐸𝐶𝑇𝑈 (Π1 ) (𝑊𝑇 ) = {K𝑝} and 𝑅𝑄𝑇𝑈 (Π1 ) (𝑊𝑇 ) = ∅. Regardless of 𝒮, as no subjective literals occur therein, the unique world view of 𝐵𝑈 (Π1 ) is 𝑊 ˆ = {{𝑝}, {𝑞}}. Since 𝑊𝐵 = {{𝑝}} is only subset of 𝑊 ˆ fulfilling 𝐸𝐶𝑇 (Π ) (𝑊𝑇 ), then it is the one selected by our 𝑈 1 method. It is also a world view for the overall program, as the unique world view of the top part is empty. This world view violates subjective constraint monotonicity, still it is the one delivered by the semantics of [11] and, as noticed in [39], by several other semantics among which [16, 17]. Consider now the following program Π2 . 𝑝|𝑞 (𝑟1) 𝑝 ← K𝑞 (𝑟2) 𝑞 ← K𝑝 (𝑟3) ⊥ ← 𝑛𝑜𝑡 K𝑝 (𝐶) Here, 𝐵𝑈 (Π2 ) consists of rules (r1-r3), and 𝑇𝑈 (Π2 ) of constraint (C). So, 𝑇𝑈′ (Π2 ) is (where 𝑘𝑝 is a fresh atom): 𝑘𝑝 | 𝑛𝑜𝑡 𝑘𝑝 ⊥ ← 𝑛𝑜𝑡 𝑘𝑝 (𝐶) whose unique world view is {{𝑘𝑝}}. After cancelling 𝑘𝑝, we obtain world view 𝑊𝑇 = {∅} for 𝑇𝑈 (Π2 ) where 𝐸𝐶𝑇𝑈 (Π2 ) (𝑊𝑇 ) = {K𝑝} and set 𝑅𝑄 is empty. Regardless of 𝒮, the potential world views of 𝐵𝑈 (Π2 ) are 𝑊1 = {{𝑝}}, 𝑊2 = {{𝑞}}, 𝑊3 = {{𝑝}, {𝑞}}, 𝑊4 = {{𝑝, 𝑞}}. 𝑊4 is the only one fulfilling 𝐸𝐶𝑇𝑈 (Π2 ) (𝑊𝑇 ); 𝑊1 has the problem that, having 𝑝 and fulfilling K𝑝, (r3) might be applied thus getting 𝑞. 𝑊4 is in fact the world view returned by semantics such as [24, 11]. However, it is easy to see that 𝑊4 violates foundedness as defined in [25]. Notice that, in our approach 𝑞 is not derived via the positive cycle (extended to subjective literals), but from the K𝑝 “forced” by the upper layer via Top-down Influence, which substitutes K𝑝 with 𝑝 in rule (r3) of 𝐵𝑈 (Π2 ). This actually guarantees foundedness. Given that the unique world view of the top is empty, then the unique world view of the overal program is indeed, according to our method, 𝑊 = 𝑊4 = {{𝑝, 𝑞}}. Notice that, there is still the problem of unfoundeness of world view {{𝑝, 𝑞}} for the program consisting of rules (r1-r3) only. The example suggests that adding an upper-level constraint involving negated subjective literal(s) might be an empirical method to solve this problem. Let us go back to program Π0 that was the first one that we mentioned before: 𝑎|𝑏 (𝑟1) 𝑐 ← K𝑎 (𝑟2) ← 𝑛𝑜𝑡 𝑐 (𝐶) Here, 𝐵𝑈 (Π0 ) consists of rule (r1), and 𝑇𝑈 (Π0 ) of rule (r2) and constraint (C). So, 𝑇𝑈′ (Π0 ) is (where 𝑘𝑎 is a fresh atom): 𝑘𝑎 | 𝑛𝑜𝑡 𝑘𝑎 𝑐 ← 𝑘𝑎 (𝑟2′ ) ← 𝑛𝑜𝑡 𝑐 (𝐶) whose unique world view is {{𝑘𝑎, 𝑐}}. After cancelling 𝑘𝑎, we obtain world view 𝑊𝑇 = {{𝑐}} for 𝑇𝑈 (Π0 ). And, 𝐸𝐶𝑇𝑈 (Π0 ) (𝑊𝑇 ) = {K𝑎} with empty 𝑅𝑄. So, given the unique world view {{𝑎}, {𝑏}} of 𝐵𝑈 (Π0 ), its subset {{𝑎}} fulfils the condition in Definition 5.4 so it will be selected to form the overall candidate world view 𝑊 = {{𝑎, 𝑐}}. As said, 𝑊 does not satisfy the epistemic splitting property, but in our opinion it captures the ‘intended meaning’ of the program, where the top layer “asks” the bottom layer to support, if possible, K𝐴 (in order not to make the overall program inconsistent). Let us now consider Π3 to be the seminal example introduced in [1], that motivated the introduction of ELPs and, later, the introduction of the notion of epistemic splitting. The specific formulation (variations have appeared over time) is the one seen in [26]. eligible(X ) ← high(X ) (𝑟1) eligible(X ) ← minority(X ), fair (X ) (𝑟2) noeligible(X ) ← 𝑛𝑜𝑡 fair (X ), 𝑛𝑜𝑡 high(X ) (𝑟3) fair (mike) | high(mike) (𝑓 1) interview (X ) ← 𝑛𝑜𝑡 K eligible(X ), 𝑛𝑜𝑡 K noeligible(X ) (𝑟4) appointment(X ) ← K interview (X ) (𝑟5) Since in this version of the program we have only mike as an individual, we may obtain the following ground abbreviated version: 𝑒←ℎ (𝑟1) 𝑒 ← 𝑚, 𝑓 (𝑟2) 𝑛𝑒 ← 𝑛𝑜𝑡 𝑓, 𝑛𝑜𝑡 ℎ (𝑟3) 𝑓 |ℎ (𝑓 1) 𝑖𝑛 ← 𝑛𝑜𝑡 K𝑒, 𝑛𝑜𝑡 K𝑛𝑒 (𝑟4) 𝑎 ← K𝑖𝑛 (𝑟5) Here, we consider (r5) as the top 𝑇𝑈 (Π3 ), and (r1-r4) plus (f1) as the bottom, which can be however in turn divided into the top 𝑇 1𝑈 (Π3 ) including (r4), and the bottom 𝐵𝑈 (Π3 ), composed of (r1-r3) plus (f1). So, 𝑇𝑈′ (Π3 ) is (where 𝑘𝑖𝑛 is a fresh atom): 𝑘𝑖𝑛 | 𝑛𝑜𝑡 𝑘𝑖𝑛 𝑎 ← 𝑘𝑖𝑛 (𝑟5′ ) with world view {{𝑎, 𝑘𝑖𝑛}, ∅}. After cancelling 𝑘𝑖𝑛 and the empty set, we obtain for 𝑇𝑈 (Π3 ) world view 𝑊11 = {{𝑎}} with 𝑅𝑄𝑇𝑈 (Π3 ) (𝑊11 ) = {K𝑖𝑛}. Set 𝐸𝐶 is empty. Then, 𝑇 1′𝑈 (Π3 ) is (where 𝑘𝑒 and 𝑘𝑛𝑒 are fresh atoms), 𝑘𝑒 | 𝑛𝑜𝑡 𝑘𝑒 𝑘𝑛𝑒 | 𝑛𝑜𝑡 𝑘𝑛𝑒 𝑖𝑛 ← 𝑛𝑜𝑡 𝑘𝑒, 𝑛𝑜𝑡 𝑘𝑛𝑒 (𝑟4′ ) So, 𝑇 1𝑈 (Π3 ) has the unique world view (after cancelling fresh atoms and empty sets) 𝑊2 = {{𝑖𝑛}}. Here, both sets 𝐸𝐶 and 𝑅𝑄 are empty. Finally, 𝐵𝑈 (Π3 ) is 𝑒←ℎ (𝑟1) 𝑒 ← 𝑚, 𝑓 (𝑟2) 𝑛𝑒 ← 𝑛𝑜𝑡 𝑓, 𝑛𝑜𝑡 ℎ (𝑟3) 𝑓 |ℎ (𝑓 1) with world view 𝑊3 = {{ℎ, 𝑒}, {𝑓 }}. Since no constraints or requirements are given, we can obtain a Candidate World View 𝑊 Π3 = {{ℎ, 𝑒, 𝑖𝑛, 𝑎}, {𝑓, 𝑖𝑛, 𝑎}} for the part of the program including (r1-r4) plus (f1) by performing the union {ℎ, 𝑒} ∪ 𝑊2 = {ℎ, 𝑒, 𝑖𝑛} and {𝑓 } ∪ 𝑊2 = {𝑓, 𝑖𝑛}, since both sets are compliant with 𝑅𝑄𝑇𝑈 (Π3 ) (𝑊11 ) = {K𝑖𝑛}. It is easily seen that 𝑊 Π3 is the unique the world view of the overall program. Notice that the above program is Epistemically Stratified in the sense of [25, 26], according to which a program is epistemically stratified if there exists a mapping of atoms to levels, where: all the objective atoms occurring in a rule are at the same level; instead, atoms occurring in subjective literals in the body of rules are at a strictly lower level. They prove that, for any semantics obeying epistemic splitting, an epistemically stratified program has a unique world view. Actually, according to the result stated in [36], epistemically stratified programs have a unique world view under any semantics, as it is shown there that multiple world views can arise only in consequence of negative cycles involving epistemic literals: these cycles are obviously impossible for epistemically stratified programs. In [25, 26] it is shown how to compute the unique world view bottom-up. We have just seen how to compute it top-down. So, on this class of programs the two methods coincide. 6. Discussion It is at this point interesting to try to assess formally which semantics (if any) satisfy top-down epistemic splitting. Observation. We can see that the “generate and test” style of programming which is commonly used in traditional ASP, where the bottom part of the program generates a search space and constraints in the top prune it, does not immediately generalize to epistemic logic programming. Subjective constraints in fact (or, more generally, constraints involving directly or indirectly some subjective literal) do indeed reduce the number of world views of the overall program, w.r.t. the number of world views of the bottom part. But, they concur to determine the contents of the remaining world views. So, we might in perspective define a notion of Epistemic Subjective Constraint Monotonicity, different however from the one of [18]. For testing compliance with the Top-down Epistemic Splitting Property TDESP, we examine the case of the semantics introduced in [24], that, following [27], we call K15 for short. Definition 6.1 (K15-world views, as reported in [27]). Given a logic program Π, its K15-reduct with respect to a non-empty set of interpretations 𝑊 is obtained by: 1. replacing by ⊥ every subjective literal 𝐿 ∈ 𝐵𝑜𝑑𝑦𝑠𝑢𝑏 (𝑟) such that 𝑊 ̸|= 𝐿, and 2. replacing all other occurrences of subjective literals of the form K𝐴 by 𝐴. A non-empty set of interpretations 𝑊 is a K15-world view of Π iff 𝑊 is the set of all stable models of the K15-reduct of Π with respect to 𝑊 . In [27] it is in fact noticed that K15 slightly generalizes the semantics proposed in [12] (called G11 for short) and can be seen as a basis for the semantics of [11] (called S16 for short). In particular, S16 treats K15 world views as candidate solutions, to be pruned in a second step, to allow some unwanted world view to be removed; this because S16 considers the operator not𝐴 which means 𝑛𝑜𝑡 𝐾𝐴, so they need to maximize what is not known. Thus, should K15 satisfy top-down Epistemic Splitting, also G11 and S16 would do as well. Theorem 6.1 (K15 TDESP). The K15 semantics satisfies the Top-down Epistemic Splitting Property. I.e., given an ELP Π, and set of sets 𝑊 , where each set is composed of atoms occurring in Π, 𝑊 is a K15 world view for Π if and only if it is a Candidate world view for Π according to Definition 5.4. Proof Assume that there are two layers, top 𝑇𝑈 (Π) and bottom 𝐵𝑈 (Π). The reasoning below can be iterated over a subdivision into an arbitrary number of levels. Notice that, given a K15 world view 𝑊 , since each atom 𝐴 that occurs in the sets composing 𝑊 is derived in the part of the program including rules with head 𝐴, then 𝑊 can be divided into two parts, 𝑊𝑇 which is a world view of the top 𝑇𝑈 (Π) and 𝑊𝐵 which is a world view of the bottom 𝐵𝑈 (Π), each one composed of stable models of the K15-reduct of that part of the program. If part. Given a K15 world view 𝑊 , let 𝑆𝑙𝑇 be the subjective literals occurring in 𝑇𝑈 (Π) for which 𝑊𝐵 |= 𝐾𝐴, i.e., which are entailed by the bottom. So, the subset of 𝑆𝑙𝑇 that consists of literals involved in constraints in 𝑇𝑈 (Π) will form set 𝐸𝐶𝑇𝑈 (Π) (𝑊𝑇 ), and the remaining ones will form set 𝑅𝑄𝑇𝑈 (Π) (𝑊𝑇 ). Therefore, we can conclude that 𝑊 , which is a K15 world view, is indeed a Candidate World Wiew according to Definition 5.4. Only if part. Consider a Candidate World Wiew 𝑊 w.r.t. the K15 semantics, obtained by combining a subset 𝑊𝐵 of a K15 world view of 𝐵𝑈 (Π) with a K15 world view 𝑊𝑇 of 𝑇𝑈 (Π) (see below for Top-down Influence). According to Definition 5.4, the combination is possible only if for each epistemic literal K𝐴 ∈ 𝐸𝐶𝑅𝑄𝑇𝑈 (Π) (𝑊𝑇 ), 𝑊𝐵 |= K𝐴. If K𝐴 ∈ 𝐸𝐶𝑇𝑈 (Π) (𝑊𝑇 ), if this is not the case then there would be a constraint violation in 𝑇𝑈 (Π), so there would be no world views for 𝑇𝑈 (Π), and for the overall program Π. Considering K𝐴 ∈ 𝑅𝑄𝑇𝑈 (Π) (𝑊𝑇 ), if it were not that 𝑊𝐵 |= K𝐴, then by definition of K15 K𝐴 would have been substituted by ⊥ instead of by 𝐴, so 𝑊𝑇 would have been a different set. The Top-down Influence step can be disregarded, since it performs in advance on elements of 𝐸𝐶𝑅𝑄𝑇𝑈 (Π) (𝑊𝑇 ), that are required to be entailed by 𝑊𝐵 anyway, the same transformation performed by K15, step 2. Then, a Candidate World view 𝑊 obtained according to Definition 5.4 is indeed a K15 world view. 7. Conclusions In this paper, we have discussed properties of semantics of ELPs. We explored a similar though complementary approach w.r.t. the work of Cabalar et al., starting from the concept, that they propose, of epistemic splitting of an ELP. In particular, we defined the Top-down Epistemic Splitting Property. We proved that the K15 semantics satisfies this property, and in consequence so do G11 and S16. An investigation of which other semantics might satisfy this property is a subject of future work. A question that may arise concerns efficiency of computing world views in a top-down fashion. We believe that, if the subjective literals connecting adjacent layers are in small number (as it seems reasonable), then efficiency might not be a concern. In [25] Section 6, it is argued that, with epistemic splitting and answer sets computation in the bottom-up fashion, a problem of conformant planning can be expressed in a way which is ‘more natural’ than under other semantics. It remains to be seen in which kinds of applications the different approaches (top-down and bottom-up) might be profitably exploited. References [1] M. Gelfond, H. Przymusinska, Definitions in epistemic specifications, in: A. Nerode, V. W. Marek, V. S. Subrahmanian (Eds.), Logic Programming and Non-monotonic Reasoning, Proceedings of the First Intl. Workshop, The MIT Press, 1991, pp. 245–259. [2] M. Gelfond, Logic programming and reasoning with incomplete information, Ann. Math. Artif. Intell. 12 (1994) 89–116. doi:10.1007/BF01530762. [3] V. W. Marek, M. Truszczyński, Stable logic programming - an alternative logic programming paradigm, Springer, 1999, pp. 375–398. [4] M. Gelfond, V. Lifschitz, The stable model semantics for logic programming, in: R. Kowal- ski, K. Bowen (Eds.), Proceedings of the 5th Intl. Conf. and Symposium on Logic Program- ming, MIT Press, 1988, pp. 1070–1080. [5] M. Gelfond, V. Lifschitz, Classical negation in logic programs and disjunctive databases, New Generation Computing 9 (1991) 365–385. [6] G. Brewka, T. Eiter, M. T. (eds.), Answer set programming: Special issue, AI Magazine 37 (2016). [7] C. Baral, Knowledge representation, reasoning and declarative problem solving, Cambridge University Press, 2003. [8] M. Truszczyński, Logic programming for knowledge representation, in: V. Dahl, I. Niemelä (Eds.), Logic Programming, 23rd Intl. Conf., ICLP 2007, 2007, pp. 76–88. [9] M. Gelfond, Answer sets, in: Handbook of Knowledge Representation. Chapter 7, Elsevier, 2007. [10] M. Gebser, N. Leone, M. Maratea, S. Perri, F. Ricca, T. Schaub, Evaluation techniques and systems for answer set programming: a survey, in: Proceedings of the Twenty- Seventh International Joint Conference on Artificial Intelligence, IJCAI-18, International Joint Conferences on Artificial Intelligence Organization, 2018, pp. 5450–5456. URL: https://doi.org/10.24963/ijcai.2018/769. doi:10.24963/ijcai.2018/769. [11] Y. Shen, T. Eiter, Evaluating epistemic negation in answer set programming, Artificial Intelligence 237 (2016) 115–135. [12] M. Gelfond, New semantics for epistemic specifications, in: J. P. Delgrande, W. Faber (Eds.), Logic Programming and Nonmonotonic Reasoning - 11th Intl. Conf., LPNMR 2011, Proceedings, volume 6645 of Lecture Notes in Computer Science, Springer, 2011, pp. 260–265. [13] M. Truszczynski, Revisiting epistemic specifications, in: M. Balduccini, T. C. Son (Eds.), Logic Programming, Knowledge Representation, and Nonmonotonic Reasoning, volume 6565 of Lecture Notes in Computer Science, Springer, 2011, pp. 315–333. [14] L. Fariñas del Cerro, A. Herzig, E. I. Su, Epistemic equilibrium logic, in: Q. Yang, M. Wooldridge (Eds.), Proceedings of the Twenty-Fourth Intl. Joint Conf. on Artificial Intelligence, IJCAI 2015, AAAI Press, 2015, pp. 2964–270. [15] E. I. Su, A monotonic view on reflexive autoepistemic reasoning, in: M. Balduccini, T. Janhunen (Eds.), Logic Programming and Nonmonotonic Reasoning - 14th Intl. Conf., LPNMR 2017, Proceedings, volume 10377 of Lecture Notes in Computer Science, Springer, 2017, pp. 85–100. [16] P. T. Kahl, A. P. Leclerc, Epistemic logic programs with world view constraints, in: A. D. Palù, P. Tarau, N. Saeedloei, P. Fodor (Eds.), Technical Communications of the 34th Intl. Conf. on Logic Programming, ICLP 2018, volume 64 of OASIcs, Schloss Dagstuhl, 2018, pp. 1:1–1:17. [17] E. I. Su, Epistemic answer set programming, in: F. Calimeri, N. Leone, M. Manna (Eds.), Logics in Artificial Intelligence - 16th European Conf., JELIA 2019, Proceedings, volume 11468 of Lecture Notes in Computer Science, Springer, 2019, pp. 608–626. [18] P. Cabalar, J. Fandinno, L. Fariñas del Cerro, Founded world views with autoepistemic equilibrium logic, in: M. Balduccini, Y. Lierler, S. Woltran (Eds.), Logic Programming and Nonmonotonic Reasoning - 15th Intl. Conf., LPNMR 2019, Proceedings, volume 11481 of Lecture Notes in Computer Science, 2019, pp. 134–147. [19] P. Cabalar, J. Fandinno, L. Fariñas del Cerro, Splitting epistemic logic programs, in: M. Balduccini, Y. Lierler, S. Woltran (Eds.), Logic Programming and Nonmonotonic Reasoning - 15th Intl. Conf., LPNMR 2019, Proceedings, volume 11481 of Lecture Notes in Computer Science, 2019, pp. 120–133. [20] T. C. Son, T. Le, P. T. Kahl, A. P. Leclerc, On computing world views of epistemic logic programs, in: C. Sierra (Ed.), Proc. of the Twenty-Sixth Intl. Joint Conf. on Artificial Intelligence, IJCAI 2017, ijcai.org, 2017, pp. 1269–1275. [21] A. P. Leclerc, P. T. Kahl, A survey of advances in epistemic logic program solvers, CoRR abs/1809.07141 (2018). URL: http://arxiv.org/abs/1809.07141. arXiv:1809.07141. [22] P. T. Kahl, A. P. Leclerc, T. C. Son, A parallel memory-efficient epistemic logic program solver: harder, better, faster, Ann. Math. Artif. Intell. 86 (2019) 61–85. doi:10.1007/ s10472-019-09621-1. [23] P. Cabalar, J. Fandinno, J. Garea, J. Romero, T. Schaub, eclingo : A solver for epistemic logic programs, Theory Pract. Log. Program. 20 (2020) 834–847. [24] P. Kahl, R. Watson, E. Balai, M. Gelfond, Y. Zhang, The language of epistemic specifications (refined) including a prototype solver, J. Log. Comput. 30 (2015) 953–989. doi:10.1093/ logcom/exv065. [25] P. Cabalar, J. Fandinno, L. Fariñas del Cerro, Splitting epistemic logic programs, in: M. Balduccini, Y. Lierler, S. Woltran (Eds.), Logic Programming and Nonmonotonic Reasoning - 15th International Conference, LPNMR 2019, Philadelphia, PA, USA, June 3-7, 2019, Proceedings, volume 11481 of Lecture Notes in Computer Science, Springer, 2019, pp. 120–133. [26] P. Cabalar, J. Fandinno, L. Fariñas del Cerro, On the splitting property for epistemic logic programs (extended abstract), in: C. Bessiere (Ed.), Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence, IJCAI 2020, ijcai.org, 2020, pp. 4721–4725. [27] P. Cabalar, J. Fandinno, L. Fariñas del Cerro, Autoepistemic answer set programming, Artif. Intell. 289 (2020) 103382. [28] V. Lifschitz, H. Turner, Splitting a logic program, in: Proc. of ICLP’94, Intl. Conf. on Logic Programming, 1994, pp. 23–37. [29] K. Marple, G. Gupta, Dynamic consistency checking in goal-directed answer set program- ming, TPLP 14 (2014) 415–427. [30] S. Costantini, A. Formisano, Query answering in resource-based answer set semantics, Theory and Practice of Logic Programming 16 (2016) 619–635. [31] Y. Lierler, M. Truszczynski, On abstract modular inference systems and solvers, Artif. Intell. 236 (2016) 65–89. doi:10.1016/j.artint.2016.03.004. [32] B. Bogaerts, A. Weinzierl, Exploiting justifications for lazy grounding of answer set pro- grams, in: J. Lang (Ed.), Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, July 13-19, 2018, Stockholm, Sweden, ijcai.org, 2018, pp. 1737–1745. doi:10.24963/ijcai.2018/240. [33] J. W. Lloyd, Foundations of Logic Programming, Springer-Verlag, 1987. [34] V. Lifschitz, Thirteen definitions of a stable model, in: A. Blass, N. Dershowitz, W. Reisig (Eds.), Fields of Logic and Computation, Essays Dedicated to Yuri Gurevich on the Occasion of His 70th Birthday, volume 6300 of Lecture Notes in Computer Science, Springer, 2010, pp. 488–503. [35] S. Costantini, A. Formisano, Negation as a resource: a novel view on answer set semantics, Fundamenta Informaticae 140 (2015) 279–305. [36] S. Costantini, About epistemic negation and world views in epistemic logic programs, Theory Pract. Log. Program. 19 (2019) 790–807. doi:10.1017/S147106841900019X. [37] S. Costantini, Meta-reasoning: A survey, in: A. C. Kakas, F. Sadri (Eds.), Computational Logic: Logic Programming and Beyond, Essays in Honour of Robert A. Kowalski, Part II, volume 2408 of Lecture Notes in Computer Science, Springer, 2002, pp. 253–288. [38] J. Dix, A classification theory of semantics of normal logic programs I-II., Fundamenta Informaticae 22 (1995) 227–255 and 257–288. [39] Y. Shen, T. Eiter, Constraint monotonicity, epistemic splitting and foundedness are too strong in answer set programming, CoRR abs/2010.00191 (2020). URL: https://arxiv.org/ abs/2010.00191.