Epistemic Logic Programs: a Novel Perspective and Some Extensions⋆ Stefania Costantini1 , Andrea Formisano2,** 1 DISIM - Università dell’Aquila, via Vetoio, 67100, L’Aquila, Italy 2 DMIF - Università di Udine, via delle Scienze 206, 33100 Udine, Italy Abstract Epistemic Logic Programs (ELPs), which propose an extension to Answer Set Programming (ASP) with epistemic operators, have their semantic defined, in various ways, in terms of world views, which are sets of belief sets. Several semantic approaches have in fact been proposed over time to characterize world views, and, recently, to also characterize semantic properties that should be met by any semantics for ELPs. We propose a new semantics, easy also from the computational point of view, but effective, also in order to compare the different semantic approaches. We also propose a significant extension to the ELP approach, by allowing epistemic atoms in rule heads. Keywords Answer Set Programming, Epistemic Logic Programs, ELP semantics 1. Introduction It is now quite some time since the first definition of Epistemic Logic Programs (ELPs, in the following just ‘programs’ if not explicitly stated differently) was presented in [2, 3]. ELPs were meant to extend in a straightforward way Answer Set Programs (ASP programs), defined under the Answer Set Semantics [4], with epistemic operators. The extension resulted however more tricky than expected, because the new epistemic operators are able to introspectively “look inside” a program’s own semantics, defined in terms of its “answer sets”. This because K𝐴, K standing for knowledge, means that the (ground) atom 𝐴 is true in every answer set of the very program Π where K𝐴 occurs. The derived operator of possibility 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 Π, i.e., 𝑛𝑜𝑡 K𝑛𝑜𝑡 𝐴 holds, where 𝑛𝑜𝑡 is standard ASP default negation. Semantics of ELPs is provided in terms of some kind of mechanism to characterize world views, which are sets of answer sets (instead of a unique set of answer sets like in Answer Set Programming), where each world view consistently satisfies (according to a given semantic 15th Workshop on Answer Set Programming and Other Computing Paradigms, July 31, 2022, Haifa, Israel ⋆ Research partially supported by Action COST CA17124 “DigForASP” and by project INDAM GNCS-22 InSANE (CUP_E55F22000270001). This paper extends the research appeared in [1]. ** Corresponding author. stefania.costantini@univaq.it (S. Costantini); andrea.formisano@uniud.it (A. Formisano)  0000-0002-5686-6124 (S. Costantini); 0000-0002-6755-9314 (A. Formisano) © 2022 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) approach) the epistemic expressions that appear in a given program. Many semantic approaches for ELPs have been introduced beyond the seminal ones, among which [5, 6, 7, 8, 9, 10, 11]. An interesting attempt to establish useful properties that ELP’s semantics should obey is presented by Cabalar et al. in [12, 13, 14]. Their point is that the analogous of notions which have been originally defined for ASP might prove useful in ELPs as well. The main property considered is splitting (defined for ASP in [15]), which allows a program to be (iteratively) divided into parts (“top” and “bottom”) in a principled way: the answer sets of a given program can be computed incrementally, starting from the answer sets of the bottom, which are used to simplify the top. Then, the union of each answer set of the bottom with each answer set of the corresponding simplified top is an answer set of the overall program. They extend to ELPs, where it is the world views that must be calculated, the concept of program splitting and the method of incremental calculation. Their result is a notion of Epistemic Splitting, where top and bottom are defined with respect to the occurrence of epistemic operators. As consequences of the splitting property, they define Subjective Constraint Monotonicity, which states that adding constraints may lead, for ELPs, to purge some of the world views (but not to purge answer sets within world views), and Foundedness, meaning that atoms composing answer sets cannot have been derived through cyclic positive dependencies, where, for ELPs, such dependencies may involve epistemic operators. In this paper, we explore a different stance: in order to establish a term of comparison among the various semantics, we introduce a semantic approach which is very plainly based on the basic understanding of ELP and world views. We then experiment the new approach on many examples taken from the relevant literature, and we “observe” its behaviour, in terms of the correspondence or discrepancy with the results returned by other relevant semantic approaches. Then, we propose an extension to ELPs so as to allow for (positive) subjective literals in the head of rules. This extension gives a greater importance to meta-reasoning, and, we argue, this goes in favour of explainability and trustworthy Artificial Intelligence; technically, the extension rules out some unwanted aspects of many semantics, such as unfounded world views. The paper is organized as follows. In Section 2 we briefly recall ELPs (basic notions concerning syntax, semantics, and semantic properties are summarized in the Appendix). In Section 3 we introduce and discuss our proposal. In Section 4 we discuss the proposed extensions. Finally, in Section 5 we conclude. In the Appendix, for the sake of completeness in Section A we recall Answer Set Programming. In Sections B, C, and D we report: the formal definition of the main existing semantics for ELPs, tables with the results that such semantics return on some significant programs, and the list of available ELP solvers. 2. Epistemic Logic Programs Epistemic Logic Programs 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). The literal K𝐿 means that the (ground) literal 𝐿 is true in every answer set of a given program Π (it is a cautious consequence of Π). The syntax of rules is analogous to ASP (cf., Appendix A), save that literals in the body can now be either objective or subjective. Nesting of epistemic operators 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 𝑟. Let Head (𝑟) be the head of rule 𝑟 and Bodyobj (𝑟) (resp., Bodysubj (𝑟)) be the (possibly empty) set of objective (resp., subjective) literals occurring in the body of 𝑟. We often write Head (𝑟) and Bodyobj (𝑟) in place of Atoms(Head (𝑟)) and Atoms(Bodyobj (𝑟)), respectively, when the intended meaning is clear from the context. We call subjective rules those rules whose body is made of subjective literals only. The semantics of ELPs is based on the notion of world views: namely, sets of answer sets. Each world view determines the truth value of all objective literals in a program. For example, the program {𝑎 ← 𝑛𝑜𝑡 𝑏, 𝑏 ← 𝑛𝑜𝑡 𝑎, 𝑒 ← 𝑛𝑜𝑡 K𝑓, 𝑓 ← 𝑛𝑜𝑡 K𝑒}, under every semantics, has two world views: [{𝑎, 𝑒}, {𝑏, 𝑒}], where K𝑒 is true and K𝑓 is false, and [{𝑎, 𝑓 }, {𝑏, 𝑓 }] where K𝑓 is true and K𝑒 is false. Note that, according to a widely-used convention, each world view, which is a set of answer sets, is enclosed in []. The presence of two answer sets in each world view of the above program is due to the cycle on objective atoms, whereas the presence of two world views is due to the cycle on subjective atoms (in general, the existence and number of world views is related to such cycles, cf., [16] for a detailed discussion). Let a semantics 𝒮 be a function mapping each program into sets of ‘belief views’, i.e., sets of sets of objective literals, where 𝒮 has the property that, if Π is an objective program, then the unique member of 𝒮(Π) is the set of stable models of Π. Given a program Π, each member of 𝒮(Π) is called an 𝒮-world view of Π (we will often write “world view” in place of “𝒮-world view” whenever mentioning the specific semantics is irrelevant). The main existing semantic approaches for ELPs are introduced in Section B in the Appendix. As usual, for any world view 𝑊 and any subjective literal K𝐿, we write 𝑊 |= K𝐿 iff for all 𝐼 ∈ 𝑊 the literal 𝐿 is satisfied by 𝐼 (i.e., if 𝐿 ∈ 𝐼 for 𝐿 atom, or 𝐴 ̸∈ 𝐼 if 𝐿 is 𝑛𝑜𝑡 𝐴). 𝑊 satisfies a rule 𝑟 if each 𝐼 ∈ 𝑊 satisfies 𝑟. The property of Subjective Constraint Monotonicity states that, for any ELP program Π and any subjective constraint 𝑟, 𝑊 is a world view of Π ∪ {𝑟} iff both 𝑊 is a world view of Π and 𝑊 satisfies 𝑟. Thus, if this property is fulfilled by a semantic 𝒮, a constraint can rule out world views but cannot rule out some answer set from within a world view. Foundedness, implies that atoms occurring in sets within a world view cannot have been derived through cyclic positive dependencies, where, to define such dependencies, K𝐴 is seen as the same as 𝐴. 3. Our Observations and Proposal Below we propose and discuss a method devised in order to compare the various semantics, that however can be seen as a new semantics on its own right. Let us notice that, actually, in Gelfond’s proposal, K𝐺 is intended to mean that 𝐺 is true in all the answer set of a given program, where the set of these answer sets is now called world view, or that 𝐺 is true in all the answer sets of a certain world view, if there are many of them. It is not really required for 𝐺 to be derivable from the program in a ‘founded’ way as it happens in ASP, or, at the very least, the concept of founded derivation becomes different. In the G94 computation of a world view, what is assumed to be known or not known comes from the world view, not from the program. What is required by this basic approach is that a world view is consistent w.r.t. the program, in the sense that what is assumed to be known is indeed concluded, and what is assumed to be false is not concluded. However, the point is that subjective atoms appearing in the program (and that are not derived, but elicited from the underlying world view) have a role in drawing conclusions. We introduce an approach where this seminal intuition is literally applied. We then put the new approach at work on a number of examples, taking the occasion for a comparison with various semantics appeared in the literature (that are briefly recalled in the appendix). 3.1. A new approach We consider in this context only subjective literals K𝐺 and Knot𝐺. We will consider them as new atoms, called knowledge atoms. Negation 𝑛𝑜𝑡 in front of knowledge atoms is assumed to be the standard default negation. So, instead of ELPs proper, we here consider ASP programs possibly involving knowledge atoms. First of all we introduce the concept of internal consistency of a set of atoms including knowledge atoms. Definition 3.1. A set 𝐴 of atoms, composed of objective atoms and knowledge atoms, is said to be knowledge consistent iff: (i) it contains 𝐺 whenever it contains the knowledge atom K𝐺; (ii) it does not contain 𝐺 whenever it contains the knowledge atom Knot𝐺. Let Π be a program. A set of sets of atoms 𝒲, each such set composed of objective atoms and knowledge atoms (occurring in Π), is called here epistemic interpretation. For any atom 𝐺 we write 𝒲 |= 𝐺 iff for all 𝑋 ∈ 𝒲 it holds that 𝐺 ∈ 𝑋. Similarly, we write 𝒲 |= 𝑛𝑜𝑡 𝐺 iff for all 𝑋 ∈ 𝒲 it holds that 𝐺 ̸∈ 𝑋. Definition 3.2. Given ASP program Π possibly involving knowledge atoms, let SMC (Π) be the set of those answer sets of the program which are knowledge-consistent. Property 3.1. SMC (Π) corresponds to the stable models of the program Π′ obtained from Π by adding, for each knowledge atom K𝐺 or Knot𝐺 occurring in Π, the constraints: ← K𝐺, 𝑛𝑜𝑡 𝐺 ← Knot𝐺, 𝐺. To establish a uniform comparison among semantic approaches, we propose a basic point of view on ELPs. Definition 3.3. [CF22-adaptation] The CF22-adaptation Π-𝒲 of a program Π with respect to an epistemic interpretation 𝒲 is obtained by adding to Π: (i) new fact K𝐺 whenever 𝒲 |= 𝐺, and (ii) new fact Knot𝐺 whenever 𝒲 |= 𝑛𝑜𝑡 𝐺. Let 𝐹Π-𝒲 be the set of those newly added facts of the form K𝐺. Definition 3.4 (CF22 world view). An epistemic interpretation 𝒲 is called a CF22 world view of a program Π if 𝒲 = SM ′ (Π-𝒲), where SM ′ (Π-𝒲) is obtained from SMC (Π-𝒲) by can- celling knowledge atoms. Notice that, differently from existing semantics, checking whether an epistemic interpretation is a CF22 world view just requires an ASP solver, and not specialized solvers such as those reported in Table 3 of Appendix D. We may notice that, the S16 semantics (cf., Def. B.4) is remarkable in the sense that it maximizes what is not known, which is equivalent to minimizing what is known. The proposers of S16 consider each potential world view (that in their approach is associated to a guess about what is not known) as a candidate world view, and discard those for which there exists another one with a larger guess on what is not known (equivalently, a smaller guess on what is known), in terms of set inclusion. Rephrasing their criterion (referred to as S16C) in our setting, we have: Definition 3.5 (S16 Criterion - CF22+S16C). Each world view 𝒲 as of Def. 3.4 is consid- ered to be a candidate world view. A candidate world view 𝒲 is indeed a world view under CF22+S16C if no other candidate world view 𝒲’ exists, where 𝐹Π-𝒲 ′ ⊂𝐹Π-𝒲 . 3.2. CF22 world views: Examples of application It can be easily seen that, on the examples on the left-column of Table 1 in the Appendix, on which all the main existing semantic approaches (cf., Appendix B) agree, CF22 agrees as well. Below we present in detail a number of less trivial examples, some taken from the right-hand side of Table 1, from Table 2, and from the relevant literature. The aim is to employ CF22 as a term of comparison among the various semantics. Example 1 Consider the program Π 𝑎 ∨ 𝑏. 𝑎 ← K𝑏. 𝑏 ← K𝑎. and the epistemic interpretation 𝒲 = [∅]. According to Def. 3.3, the added facts are: K𝑛𝑜𝑡 𝑎. K𝑛𝑜𝑡 𝑏. We have that SMC (Π-𝒲) = ∅, because the two rules cannot be applied, and the disjunction would generate answer sets {𝑎} and {𝑏} that are not knowledge consistent; thus, SM ′ (Π-𝒲) = ∅, so 𝒲 is not a CF22 world view. Consider the epistemic interpretation 𝒲 = [{𝑎}] (the analogous can be done for [{𝑏}]). According to Def. 3.3, the added facts are: K𝑎. K𝑛𝑜𝑡 𝑏. We have the answer set {K𝑎, K𝑛𝑜𝑡 𝑏, 𝑎, 𝑏} where 𝑎 comes from the disjunction, and 𝑏 is derived from the second rule, where however this answer set is not knowledge consistent; thus, SMC (Π-𝒲) = SM ′ (Π-𝒲) = ∅, so 𝒲 is not a CF22 world view. Consider the epistemic interpretation 𝒲 = [{𝑎, 𝑏}]. According to Def. 3.3, the added facts are: K𝑎. K𝑏. We have that SMC (Π-𝒲) = [{K𝑎, K𝑏, 𝑎, 𝑏}], with atoms 𝑎 and 𝑏 derived via the rules given the facts; this answer set is knowledge consistent, thus SM ′ (Π-𝒲) = [{𝑎, 𝑏}], so 𝒲 is a CF22 world view. Consider, finally, 𝒲 = [{𝑎}, {𝑏}]. According to Def. 3.3, there are no added facts. Then, SMC (Π-𝒲) = SM ′ (Π-𝒲) = [{𝑎}, {𝑏}], deriving from the disjunction, as the two rules cannot be applied; thus, 𝒲 is a CF22 world view. This example shows that CF22, that here agrees with G11, does not satisfy foundedness. However, if one augments it with the S16C criterion, then the unfounded world view [{𝑎, 𝑏}] is excluded, as there exists the world view [{𝑎}, {𝑏}] which is based on fewer added positive knowledge literals (none for the latter and K𝑎 and K𝑏 for the former). One may notice that, for world view [{𝑎, 𝑏}], these atoms are not derived from the program via a positive circularity: rather, they are supported, in the program, from what is deemed to be known in the world view itself. So, while this world view can be excluded by applying a minimality criterion, it is however not unreasonable in itself. Example 2 Consider the program Π: 𝑎 ← 𝑛𝑜𝑡 K𝑛𝑜𝑡 𝑎. and the epistemic interpretation 𝒲 = [∅]. By Def. 3.3, a single fact is added: K𝑛𝑜𝑡 𝑎. We have SMC (Π-𝒲) = [{K𝑛𝑜𝑡 𝑎}], thus SM ′ (Π-𝒲) = [∅], so 𝒲 is a CF22 world view. Consider the epistemic interpretation 𝒲 = [{𝑎}]. According to Def. 3.3, the added facts are: K𝑎. In this case, we have SMC (Π-𝒲) = [{K𝑎, 𝑎}] (as the fact K𝑛𝑜𝑡 𝑎 is not present, its negation is true), thus SM ′ (Π-𝒲) = [{𝑎}], so 𝒲 is a CF22 world view. On this example, CF22 agrees with G94, G11, FAAEL. Example 3 Let us now consider a more problematic example. 𝑎 ← K𝑎. 𝑎 ← 𝑛𝑜𝑡 K𝑎. and consider the epistemic interpretation 𝒲 = [∅]. By Def. 3.3, the added fact is: K𝑛𝑜𝑡 𝑎. We have that SMC (Π-𝒲) = ∅ (as fact K𝑎 is not present, its negation is true, thus allowing to derive 𝑎, within however a stable model which is not knowledge consistent), thus SM ′ (Π-𝒲) = ∅, so 𝒲 is not a CF22 world view. Consider the epistemic interpretation 𝒲 = [{𝑎}]. According to Def. 3.3, one fact is added: K𝑎. Then, SMC (Π-𝒲) = [{K𝑎, 𝑎}] and SM ′ (Π-𝒲) = [{𝑎}], so 𝒲 is a CF22 world view. On this example, CF22 and G94 agree, while all the other semantics provide no world view. If the program would simply be 𝑎 ← K𝑎. then its CF22 world views would be [∅] and [{𝑎}], in agreement with G94, or with G11, K15, F15, S16, FAAEL under CF22+S16C. Example 4 In previous examples CF22+S16C tended to agree with S16. This is however not always the case. Consider the program 𝑎 ← 𝑛𝑜𝑡 K𝑛𝑜𝑡 𝑏, 𝑛𝑜𝑡 𝑏. 𝑏 ← 𝑛𝑜𝑡 K𝑛𝑜𝑡 𝑎, 𝑛𝑜𝑡 𝑎. and the epistemic interpretation 𝒲 = [∅]. According to Def. 3.3, the added facts are: K𝑛𝑜𝑡 𝑎. K𝑛𝑜𝑡 𝑏. We have that SMC (Π-𝒲) = [K𝑛𝑜𝑡 𝑎, K𝑛𝑜𝑡 𝑏] and SM ′ (Π-𝒲) = [∅], so 𝒲 is a CF22 world view. Consider, instead, 𝒲 = [{𝑎}] (one can proceed analogously for [{𝑏}]). According to Def. 3.3, the added facts are: K𝑎. K𝑛𝑜𝑡 𝑏. We have that SMC (Π-𝒲) = ∅ (as one can derive 𝑏, obtaining however a stable model which is not knowledge consistent, because of the fact K𝑛𝑜𝑡 𝑏), thus SM ′ (Π-𝒲) = ∅, so 𝒲 is not a CF22 world view. For the epistemic interpretation 𝒲 = [{𝑎}, {𝑏}], where there are no added facts. We have that SMC (Π-𝒲) = SM ′ (Π-𝒲) = [{𝑎}, {𝑏}], so 𝒲 is a CF22 world view. Epistemic interpretation [{𝑎, 𝑏}] is easily discarded. On this example, CF22 agrees with G94, G11, K15, FAAEL. Under CF22+S16C nothing changes, as both CF22 world views do not rely on positive knowledge atoms. If the (seemingly) simpler program is considered: 𝑎 ← 𝑛𝑜𝑡 K𝑛𝑜𝑡 𝑏. 𝑏 ← 𝑛𝑜𝑡 K𝑛𝑜𝑡 𝑎. we have that, similarly to before, [{𝑎}] and [{𝑏}] are not CF22 world views. However, for 𝒲 = [∅], we obtain SMC (Π-𝒲) = [∅] is a CF22 world view, because from added facts K𝑛𝑜𝑡 𝑎. K𝑛𝑜𝑡 𝑏. one does not derive anything. Instead, 𝒲 = [{𝑎}, {𝑏}] is not a CF22 world view, because with no added facts one can derive both 𝑎 and 𝑏, so SMC (Π-𝒲) = SM ′ (Π-𝒲) = [{𝑎, 𝑏}]. But, 𝒲 = [{𝑎, 𝑏}] is a CF22, world view, because adding new facts K𝑎. K𝑏. both negations in the bodies of the program rules are true, so one derives both 𝑎 and 𝑏 obtaining SMC (Π-𝒲) = SM ′ (Π-𝒲) = [{𝑎, 𝑏}]. On this program, CF22 does not agree with the other semantics: it has world view [∅] like G94, G11, and FAEEL, but returns [{𝑎, 𝑏}], that no other semantics provides, and does not return [{𝑎}, {𝑏}], that is provided by all the other semantics. The rationale underlying world view [{𝑎, 𝑏}] is that, again, it is consistent with the given program, relatively to the positive knowledge atoms that the world view entails. Example 5 Consider the epistemic logic program: 𝑎 ∨ 𝑏. 𝑎 ← K𝑛𝑜𝑡 𝑏. Clearly, because of the disjunction [∅] cannot be a CF22 world view. Consider 𝒲 = [{𝑎}]. According to Def. 3.3, the added facts are: K𝑎. K𝑛𝑜𝑡 𝑏. We have that SMC (Π-𝒲) = [{K𝑎, K𝑛𝑜𝑡 𝑏, 𝑎}], thus SM ′ (Π-𝒲) = [{𝑎}], so 𝒲 is a CF22 world view. If 𝒲 = [{𝑏}]. According to Def. 3.3, the added facts are: K𝑏. K𝑛𝑜𝑡 𝑎. SMC (Π-𝒲) = [{K𝑏, K𝑛𝑜𝑡 𝑎, 𝑏}] and SM ′ (Π-𝒲) = [{𝑏}]. Hence, 𝒲 is a CF22 world view. Consider the epistemic interpretation 𝒲 = [{𝑎}{𝑏}]. By Def. 3.3, there are no added facts. We have that SMC (Π-𝒲) = SM ′ (Π-𝒲) = [{𝑎}, {𝑏}], so 𝒲 is a CF22 world view. It is easy to verify that instead [{𝑎, 𝑏}] is not a CF22 world view (because the disjunction cannot generate both 𝑎 and 𝑏). On this example, CF22 does not agree with existing semantics, because of the world view [{𝑏}], that they do not produce. Under CF22+S16C, there is agreement with S16, as in fact world view [{𝑎}, {𝑏}], based upon an empty set of added knowledge atoms of the form K𝐴, rules out both [{𝑎}] and [{𝑏}]. Example 6 Consider the epistemic logic program make of the two rules: 𝑎 ∨ 𝑏. ← 𝑛𝑜𝑡 K𝑎. Clearly, because of the disjunction, [∅] cannot be a CF22 world view. Considering the epistemic interpretation 𝒲 = [{𝑎}], by Def. 3.3, the facts to be added are: K𝑎. K𝑛𝑜𝑡 𝑏. We have that SMC (Π-𝒲) = [{K𝑎, K𝑛𝑜𝑡 𝑏, 𝑎}] (the stable model with 𝑏 is excluded as it is not knowledge consistent), thus SM ′ (Π-𝒲) = [{𝑎}], so 𝒲 is a CF22 world view. For the epistemic interpretation 𝒲 = [{𝑏}], by Def. 3.3, the added facts are: K𝑏. K𝑛𝑜𝑡 𝑎. Here, the constraint is clearly violated, then we have SMC (Π-𝒲)=SM ′ (Π-𝒲)=∅, thus 𝒲 is not a CF22 world view. Consider instead 𝒲 = [{𝑎}{𝑏}]. There are no added facts. Again, the constraint is violated, then we have SMC (Π-𝒲)=SM ′ (Π-𝒲)=∅, thus 𝒲 is not a CF22 world view. It is easy to verify that [{𝑎, 𝑏}] is not a CF22 world view (because the constraint is not violated, but the disjunction cannot generate both 𝑎 and 𝑏). Thus, CF22 on this program agrees with K15 and S16, and, like them, it does not satisfy Subjective Constraint Monotonicity as defined in [11]. This property imposes that a constraint (in the above example ← 𝑛𝑜𝑡 K𝑎.) put at a higher level (in the sense of Lifschitz and Turner splitting notion, extended in the above-mentioned works to ELPs) w.r.t. an “object program” (that in the above example is 𝑎 ∨ 𝑏.) might have one of the following two effects: (i) the constraint is satisfied in a world view of the object (or “bottom”), program, thus such world view remains untouched; or, (ii) the constraint is violated in a world view, and in this case the world view is excluded. In particular, according to the FAAEL semantics, that satisfies Subjective Constraint Monotonicity, the above program has no world views, since the unique world view of the bottom part, i.e., [{𝑎}, {𝑏}], is eliminated by the constraint. However, it is not easy to understand this property, because in the “analogous” ASP program 𝑎 ∨ 𝑏. ← 𝑛𝑜𝑡 𝑎. the constraint is indeed allowed, in ASP, to expunge from the (unique) world view [{𝑎}, {𝑏}] of the bottom part (the set of its answer sets) the answer set {𝑏}, thus producing for the program the unique world view [{𝑎}]. This however, according to Subjective Constraint Monotonicity, should not be allowed for ELPs. 4. Extensions In this section we introduce the possibility of having positive knowledge atoms as heads of rules in ELPs. This goes toward the wish, underlying part of the current literature, to derive what is known in a founded way from the program, instead of just requiring the program and its world views to be mutually consistent. Actually, the proposed extension allows for a mixture of the two attitudes. The new syntax for ELPs is, synthetically, the following. Definition 4.1. The syntax of enhanced ELP programs (EELPs) is the same as for ELPs, except that the head of a rule can be a positive knowledge atom of the form K𝐺. Below is the definition of the enhanced program adaptation CF22M (M standing for “Meta”). Definition 4.2. [CF22M-adaptation] The CF22-adaptation Π-𝒲 of an EELP program Π with respect to an epistemic interpretation 𝒲 is obtained by adding to Π: (i) new fact K𝐺 whenever 𝒲 |= 𝐺 and K𝐺 does not occur as the head of a rule in Π, or (ii) new rule 𝐺 ← K𝐺 whenever K𝐺 occurs as the head of a rule in Π, or (iii) new fact Knot𝐺 whenever 𝒲 |= 𝑛𝑜𝑡 𝐺. Let 𝐹Π-𝒲 be the set of those newly added facts of the form K𝐺. Notice that the rule added in point (ii) corresponds to axiom T in modal logic S5, The definition of world view, now called CF22M world view, remains the same as in Def. 3.4, and can be extended as before to CF22M+S16C. To see why the proposed extension is epistemically different from the original ELP approach, consider the following ELP program Π1 (which refers to the Italian system, where in order to get promoted a positive evaluation of behaviour at school is required, in addition to having achieved good grades): promoted ← Kgood _grades, Kgood _behavior . A corresponding EELP program Π2 is: Kpromoted ← Kgood _grades, Kgood _behavior . promoted ← Kpromoted . where the latter rule is added by definition of CF22M-adaptation. Consider now to add to both programs the set of facts: good _grades. good _behavior ∨ bad _behavior . Both programs have the same world views (where, on Π1 , all existing seman- tics, including CF22, coincide), i.e.: [{promoted , good _grades, good _behavior }] and [{good _grades, bad _behavior }]. So, it would seem that there is no change in evolving from CF22 to CF22M. Assume, however, to add a different set of facts, namely the single fact: promoted . In Π1 , as it is customary in ASP and more generally in logic programming, the fact overrides the rule, so the unique world view of the resulting program would be [{promoted }]. Considering now Π2 under CF22M: this answer set is not knowledge consistent because Kpromoted is not derived, so there exists no CF22M world view. This is to say, meta-level rules for an atom 𝐺, i.e., rules with head K𝐺, if existing, cannot be overridden by object-level (“bottom”) rules. In the above example, it can be said that under CF22M promoted cannot be concluded because there is no explanation/justification for it, as the meta-level rule is not applicable. Notice that, it is left to the programmer to decide for which rules to introduce the head K𝐺, or instead to leave simply the head 𝐺. This accounts to deciding which atoms are more “critical”, and so one wants a trustworthy derivation for them. It is possible to prove the following theorem, that deals with the limit case where all atoms defined by rules are “managed” at the meta-level: Theorem 4.1. If, given ELP program Π, one constructs program Π′ by substituting every atom 𝐺 in the head of some rule with K𝐺, then the CF22M world views of Π′ coincide with the founded CF22 world views of Π. We can see how this happens by means of an example. Example 7 Consider the program Π below. 𝑎 ← 𝑛𝑜𝑡 K𝑏. 𝑏 ← 𝑛𝑜𝑡 K𝑎. 𝑒 ← K𝑓. 𝑓 ← K𝑒. As it is easy to see, CF22 world views are [{𝑎, 𝑒, 𝑓 }] and [{𝑏, 𝑒, 𝑓 }], both unfounded. Let us now consider Π′ : K𝑎 ← 𝑛𝑜𝑡 K𝑏. K𝑏 ← 𝑛𝑜𝑡 K𝑎. K𝑒 ← K𝑓. K𝑓 ← K𝑒. Note that the CF22M-adaptation adds the rule 𝐴 ← K𝐴 for each 𝐴 ∈ {𝑎, 𝑏, 𝑒, 𝑓 }. CF22M world views would thus be [{𝑎}] and [{𝑏}] because the last two rules of Π′ form now a positive even cycle from which nothing is derived. We emphasize the difference: in Π′ , under CF22M, what is known is derived by the program; in Π, under CF22 and most of the other semantics, what is known is dictated by the world view, although it must be consistent with the program. 5. Conclusions We have presented a new semantic approach for ELP, called CF22, which applies in a straight- forward way the underlying principles of the seminal ELP approach as presented and discussed by Gelfond in [3]. We devised CF22 not exactly to propose “yet another semantics”, but rather in order to establish a principled way of comparing the different semantic approaches. We have augmented CF22 to CF22+S16C by adding a minimality criterion, S16C, “inherited” from the semantics S16 [8], that excludes some world views if there are others that rely on fewer assumptions about what is known. We have experimented CF22 on several examples taken from the relevant literature, for which the outcome of the other most relevant semantic approaches was well-known. Results are quite surprising, as the new semantics does not agree uniformly with the others, and in some cases it agrees with none of them. More investigation is required to understand the reasons for these discrepancies. Moreover, even when CF22 agrees with S16 (which is often the case), it is not always needed to apply the S16C Criterion in order to get the same world views. Finally, we have taken CF22 as a basis for an extensions of the ELP paradigm, where ELPs are now allowed to include rules with positive knowledge atoms as the head. We have shown the power of this extension, that prevents conclusions to be drawn that are not epistemically justified. This formulation is able to force a founded derivation of “critical” atoms, dictated by the meta-level. In general terms, which knowledge atoms are to occur in rule heads is left to the knowledge engineer. If the approach is applied extensively, i.e., all rules have knowledge atoms as their head, this rules out unfounded world views, because what is known is in this case dictated by program rules. References [1] S. Costantini, A. Formisano, Epistemic logic programs: an approach to semantic comparison, in: R. Calegari, G. Ciatto, A. Omicini (Eds.), Proc. of the 37th Italian Conference on Computational Logic (CILC 2022), CEUR Workshop Proceedings, CEUR-WS.org, 2022. [2] M. Gelfond, H. Przymusinska, Definitions in epistemic specifications, in: A. Nerode, V. W. Marek, V. S. Subrahmanian (Eds.), Proc. of the 1st Intl. Workshop on Logic Programming and Non-monotonic Reasoning, The MIT Press, 1991, pp. 245–259. [3] M. Gelfond, Logic programming and reasoning with incomplete information, Ann. Math. Artif. Intell. 12 (1994) 89–116. [4] M. Gelfond, V. Lifschitz, The stable model semantics for logic programming, in: R. Kowal- ski, K. Bowen (Eds.), Proc. of the 5th Intl. Conf. and Symp. on Logic Programming, MIT Press, 1988, pp. 1070–1080. [5] M. Gelfond, New semantics for epistemic specifications, in: J. P. Delgrande, W. Faber (Eds.), Proc. of LPNMR’11, volume 6645 of LNCS, Springer, 2011, pp. 260–265. [6] M. Truszczynski, Revisiting epistemic specifications, in: M. Balduccini, T. C. Son (Eds.), Logic Programming, Knowledge Representation, and Nonmonotonic Reasoning, volume 6565 of LNCS, Springer, 2011, pp. 315–333. [7] L. Fariñas del Cerro, A. Herzig, E. I. Su, Epistemic equilibrium logic, in: Q. Yang, M. J. Wooldridge (Eds.), Proc. of IJCAI 2015, AAAI Press, 2015, pp. 2964–2970. [8] Y. Shen, T. Eiter, Evaluating epistemic negation in answer set programming, Artificial Intelligence 237 (2016) 115–135. [9] P. T. Kahl, A. P. Leclerc, Epistemic logic programs with world view constraints, in: A. D. Palù, P. Tarau, N. Saeedloei, P. Fodor (Eds.), Tech. Comm. of ICLP 2018, volume 64 of OASIcs, Schloss Dagstuhl, 2018, pp. 1:1–1:17. [10] E. I. Su, Epistemic answer set programming, in: F. Calimeri, N. Leone, M. Manna (Eds.), Proc. of JELIA’19, volume 11468 of LNCS, Springer, 2019, pp. 608–626. [11] P. Cabalar, J. Fandinno, L. Fariñas del Cerro, Splitting epistemic logic programs, in: M. Balduccini, Y. Lierler, S. Woltran (Eds.), Proc. of LPNMR’19, volume 11481 of LNCS, Springer, 2019, pp. 120–133. [12] P. Cabalar, J. Fandinno, L. Fariñas del Cerro, Splitting epistemic logic programs, Theory Pract. Log. Program. 21 (2021) 296–316. [13] 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 IJCAI 2020, ijcai.org, 2020, pp. 4721–4725. [14] P. Cabalar, J. Fandinno, L. Fariñas del Cerro, Autoepistemic answer set programming, Artif. Intell. 289 (2020) 103382. [15] V. Lifschitz, H. Turner, Splitting a logic program, in: Proc. of ICLP’94, MIT Press, 1994, pp. 23–37. [16] S. Costantini, About epistemic negation and world views in epistemic logic programs, Theory Pract. Log. Program. 19 (2019) 790–807. [17] V. Lifschitz, Thirteen definitions of a stable model, in: A. Blass, N. Dershowitz, W. Reisig (Eds.), Fields of Logic and Computation, vol. 6300 of LNCS, Springer, 2010, pp. 488–503. [18] S. Costantini, A. Formisano, Negation as a resource: a novel view on answer set semantics, Fundamenta Informaticae 140 (2015) 279–305. [19] J. W. Lloyd, Foundations of Logic Programming, Springer-Verlag, 1987. [20] 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. [21] E. I. Su, L. Fariñas del Cerro, A. Herzig, Autoepistemic equilibrium logic and epistemic specifications, Artif. Intell. 282 (2020) 103249. [22] D. Pearce, A new logical characterization of stable models and answer sets, in: NMELP’96, number 1216 in LNAI, Springer, 1997, pp. 55–70. [23] D. Pearce, A. Valverde, Synonymous theories in answer set programming and equilibrium logic, Proc. of ECAI04, 16th Europ. Conf. on Art. Intell. (2004) 388–390. [24] D. Pearce, Equilibrium logic, Ann. Math. Artif. Intell. 47 (2006) 3–41. [25] E. I. Su, Refining the semantics of epistemic specifications, in: A. F. et al. (Ed.), Proc. ICLP 2021,Tech. Comm., volume 345 of EPTCS, 2021, pp. 113–126. A. Answer Set Programming and Answer Set Semantics In Answer Set Programming (ASP), one can see a 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 that compute the answer sets of a given program. Syntactically, an ASP program Π is a collection of rules of the form 𝐴1 ∨ . . . ∨ 𝐴𝑔 ← 𝐿1 , . . . , 𝐿𝑛 . where each 𝐴𝑖 , 0 ≤ 𝑖 ≤ 𝑔, is an atom, ∨ indicates disjunction and the 𝐿𝑖 s, 0 ≤ 𝑖 ≤ 𝑛, are literals (i.e., atoms or negated atoms of the form 𝑛𝑜𝑡 𝐴). The left-hand side and the right-hand side of the rule are called head and body, resp. A rule with empty body is called a fact. Disjunction can occur in rule heads only, so, in facts. A rule with empty head (or, equivalently, with head ⊥), of the form ‘← 𝐿1 , ..., 𝐿𝑛 .’ or ‘⊥ ← 𝐿1 , ..., 𝐿𝑛 .’, is a constraint, stating that 𝐿1 , . . . , 𝐿𝑛 are not allowed to be simultaneously true in an answer set; the impossibility to fulfil such requirement is one of the reasons that make a program inconsistent. All extensions of ASP not explicitly mentioned above are not considered in this paper. We implicitly refer to the “ground” version of Π, which is obtained by replacing in all possible ways the variables occurring in Π with constants occurring in Π, and is thus composed of ground atoms, i.e., atoms which contain no variables. The answer set (or “stable model”) semantics can be defined in several ways [17, 18]. 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 from [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 the program Π𝐼 , namely, the (so-called) Gelfond-Lifschitz reduct of Π w.r.t. 𝐼. Π𝐼 is obtained from Π by: 1. removing all rules which contain a negative literal 𝑛𝑜𝑡 𝐴 for 𝐴 ∈ 𝐼; and 2. removing all negative literals from the remaining rules. The fact that Π𝐼 is a positive program ensures that a least Herbrand model exists and can be computed via the standard immediate consequence operator [19]. Then, 𝐼 is an answer set whenever 𝐺𝐿Π (𝐼) = 𝐼. B. Proposals for ELP Semantics We report below some of the most relevant semantic definitions for ELPs. We start with the seminal definition of the first ELP semantics, introduced in [3], that we call for short G94. Let Π be an ELP program, and 𝑟 a rule occurring therein. Definition B.1 (G94-world views). The G94-reduct of Π with respect to a non-empty set of interpretations 𝑊 is obtained by: (i) replacing by ⊤ every subjective literal 𝐿 ∈ Bodysubj (𝑟) such that 𝐿 is of the form K𝐺 and 𝑊 |= 𝐺, and (ii) replacing all other occurrences of subjective literals of the form K𝐺 by ⊥. A non-empty set of interpretations 𝑊 is a G94-world view of Π iff 𝑊 coincides with the set of all stable models of the G94-reduct of Π with respect to 𝑊 . This definition was then extended to a new one [5], that we call for short G11. Definition B.2 (G11-world views). The G11-reduct of Π w.r.t. a non-empty set of interpretations 𝑊 is obtained by: (i) replacing by ⊥ every subjective literal 𝐿 ∈ Bodysubj (𝑟) such that 𝑊 ̸|= 𝐿, (ii) removing all other occurrences of subjective literals of the form 𝑛𝑜𝑡 K𝐿. (iii) replacing all other occurrences of subjective literals of the form K𝐿 by 𝐿. The set 𝑊 is a G11-world view of Π iff 𝑊 coincides with the set of all stable models of the G11-reduct of Π w.r.t. 𝑊 . In [12], it is noticed that K15 [20] slightly generalizes the semantics proposed in [5]: Definition B.3 (K15-world views). The K15-reduct of Π w.r.t. a non-empty set of interpretations 𝑊 is obtained by: (i) replacing by ⊥ every subjective literal 𝐿 ∈ Bodysubj (𝑟) such that 𝑊 ̸|= 𝐿, and (ii) replacing all other occurrences of subjective literals of the form K𝐿 by 𝐿. The set 𝑊 is a K15-world view of Π iff 𝑊 coincides the set of all stable models of the K15-reduct of Π w.r.t. 𝑊 . Semantics G11 and K15, that are refinements of the original G94 semantics, have been proposed over time to cope with new examples that were discovered, on which existing semantic approaches produced unwanted or unintuitive world views. K15 can be seen as a basis for the semantics proposed in [8] (called S16 for short). In particular, S16 treats K15 world views as candidate solutions, to be pruned in a second step, where some world views are removed, by applying the principle of keeping those which maximize what is not known. World views in [8] are obtained in particular as follows, where note however that they consider the operator not, that can be rephrased as 𝑛𝑜𝑡 K𝐴 where 𝑛𝑜𝑡 is ASP standard ‘default negation’ (meaning that 𝐴 must be false in some answer set of a given world view). Let 𝐸𝑃 (Π) be the set of literals of the form not 𝐹 occurring in given program Π. Definition B.4 (S16-world views). Given Φ ⊆ 𝐸𝑃 (Π), the Epistemic reduct ΠΦ of Π w.r.t. Φ is obtained by: (i) replacing every not 𝐹 ∈ Φ with ⊤, and (ii) replacing every not 𝐹 ̸∈ Φ with 𝑛𝑜𝑡 𝐹 . Then, the set 𝒜 of the answer sets of ΠΦ is a candidate world view if every not 𝐹 ∈ Φ is true w.r.t. 𝒜 (i.e., 𝐹 is false in some answer set 𝐽 ∈ 𝒜) and every not 𝐹 ̸∈ Φ is false (i.e., 𝐹 is true in every answer set 𝐽 ∈ 𝒜). We say that 𝒜 is obtained from Φ (or it is corresponding to Φ, or that it is a candidate world view w.r.t. Φ), where Φ is called a candidate valid guess. Then, 𝒜 is an S16 world view if it is maximal, i.e., if there exists no other candidate world view obtained from guess Φ′ where Φ ⊂ Φ′ (so, Φ is called a valid guess). All the above semantics, in order to check whether a belief view 𝒜 is indeed a world view, adopt some kind of reduct, reminiscent of that related to the stable model semantics, and 𝒜 is a world view if it is stable w.r.t. this reduct. The F15 semantics [7, 21] is based on very different principles, namely, it is based on a combination of Equilibrium Logic [22, 23] with the modal logic S5. There, an EHT interpretation associates, via a function ℎ, a belief view 𝒜 with another belief view 𝒜′ composed, for every set 𝐴 ∈ 𝒜, of sets 𝐴′ ⊆ 𝐴. The purpose is to state that an implication is entailed, in any “belief point”, i.e., in any interpretation 𝐴 ∈ 𝒜, by the couple ⟨𝒜, 𝒜′ ⟩ if it is entailed either by 𝒜 or by 𝒜′ . An EHT interpretation satisfies a theory in the usual way, and is total on a subset 𝒳 of 𝒜 if ℎ gives back sets in 𝒳 unchanged. A total EHT model can be an equilibrium EHT model, and is defined to be an F15 world view, if it is minimal according to two particular minimality conditions (not reported here). Differently from F15, FAAEL [14] is based on the modal logic KD45. To define FAAEL, a belief view is transformed from a set of interpretations to a set of HT-interpretations, i.e., interpretations in terms of the logic of Here-and-There (HT) [24] which are couples ⟨𝐻, 𝑇 ⟩ of ‘plain’ interpretations. A belief view is total if 𝐻 = 𝑇 for all composing interpretations, thus reducing to the previous notion of belief view. A total version of any belief view can be formed, taking all the 𝑇 ’s as components. A belief interpretation is now a belief view plus an HT Table 1 On the left, examples where G94, G11, K15, F15, S16, and FAEEL agree. On the right, examples where G94/G11/FAEEL differ from K15/F15/S16. (Taken from [14].) Program World views 𝑎∨𝑏 [{𝑎}, {𝑏}] Program G94/G11/FAEEL K15/F15/S16 𝑎∨𝑏 𝑎 ← 𝑛𝑜𝑡 K𝑛𝑜𝑡 𝑎 [∅], [{𝑎}] [{𝑎}] [{𝑎}, {𝑏}] 𝑎 ← K𝑏 𝑎∨𝑏 none [{𝑎}] 𝑎∨𝑏 𝑎 ← 𝑛𝑜𝑡 K𝑛𝑜𝑡 𝑏 [{𝑎}] 𝑎 ← 𝑛𝑜𝑡 K𝑏 𝑎∨𝑏 [{𝑎}], [{𝑎}, {𝑏}] [{𝑎}, {𝑏}] 𝑎∨𝑏 𝑎 ← K𝑛𝑜𝑡 𝑏 [{𝑎, 𝑐}, {𝑏, 𝑐}] 𝑐 ← 𝑛𝑜𝑡 K𝑏 𝑎←𝑏 [∅], [{𝑎, 𝑏}] [{𝑎, 𝑏}] 𝑎 ← 𝑛𝑜𝑡 K𝑏 𝑏 ← 𝑛𝑜𝑡 K𝑛𝑜𝑡 𝑎 [{𝑎}], [{𝑏}] 𝑏 ← 𝑛𝑜𝑡 K𝑎 𝑎 ← 𝑛𝑜𝑡 K𝑛𝑜𝑡 𝑏 [∅], [{𝑎}, {𝑏}] [{𝑎}, {𝑏}] 𝑎 ← 𝑛𝑜𝑡 K𝑛𝑜𝑡 𝑎 𝑏 ← 𝑛𝑜𝑡 K𝑛𝑜𝑡 𝑎 [{𝑎}] 𝑎 ← 𝑛𝑜𝑡 K𝑎 interpretation, say 𝐻ˆ , possibly not belonging to the belief view. The peculiarity of the entailment relation (defined in terms of HT logic) is in the implication, that must hold (in the usual way) in the belief interpretation, but also in the total version of the belief view therein. For total belief interpretations, the new relation collapses to the modal logic KD45. An epistemic interpretation is defined to be a belief model if all its composing HT interpretation as well as 𝐻ˆ entail all formulas ˆ of a given theory. It is an epistemic model, if 𝐻 is among the composing interpretations, and it is an equilibrium belief model if it satisfies certain minimality conditions. A belief view is a FAAEL world view if it is “extracted” from an equilibrium belief model ℰ by taking all the 𝑇 components of each ⟨𝐻, 𝑇 ⟩ which is found in ℰ. For formal definitions of F15 and FAAEL, that for lack of space we cannot report here, we refer the reader to the aforementioned references. FAAEL satisfies [13] Epistemic Splitting, Subjective Constraint Monotonicity, and Founded- ness. G94 satisfies Epistemic Splitting, Subjective Constraint Monotonicity, but not Foundedness. In [14], it is proved that FAAEL world views coincide with founded G94 world views, where (roughly) founded world views are those where in every composing interpretation, objective atom 𝐺 is never derived, directly or indirectly, from K𝐺. We apologize with the readers and with the authors, because for lack of space, we do not consider other recent semantics, such as [10, 25]. C. Semantic Results for Interesting ELP Programs In Tables 1 and 2 a summary is reported, taken from [14], of how the semantics presented in this paper behave on some examples which are considered to be significant of situations that can be found in practical programming. Table 2 Examples showing differences among several semantics. (Taken from [14].) Program G94 G11/FAEEL K15 F15/S16 𝑎 ← 𝑛𝑜𝑡 K𝑛𝑜𝑡 𝑏 ∧ 𝑛𝑜𝑡 𝑏 [∅], [{𝑎}, {𝑏}] [{𝑎}, {𝑏}] 𝑏 ← 𝑛𝑜𝑡 K𝑛𝑜𝑡 𝑎 ∧ 𝑛𝑜𝑡 𝑎 𝑎 ← K𝑎 [∅], [{𝑎}] [∅] 𝑎 ← K𝑎 [{𝑎}] none 𝑎 ← 𝑛𝑜𝑡 K𝑎 Table 3 List of solvers available for the semantics summarized in Section B Solver Year Semantics Underlying Impl. language Available form ASP-solver ELMO 1994 G94 dlv Prolog n/a sismodels 1994 G94 claspD C++ n/a Wviews 2007 G94 clingo C++ Windows binary Esmodels 2013 G11 clingo (unknown) Windows binary ELPS 2014 K15 clingo Java source+binary GISolver 2015 K15 clingo (unknown) Windows binary ELPsolve 2016 K15/S16 clingo C++ binary only Wviews2 2017 G94 clingo Python Windows binary EP-ASP 2017 K15/S16 clingo Python+ASP Windows binary PelpSolver 2017 S16 clingo Java Windows binary ELPsolve2 2017 S16 clingo C++ currently not for public release EHEX 2018 S16 clingo Python source selp 2018 S16 clingo Python source eclingo 2020 G94 clingo Python source D. Available ELP Solvers Table 3 shows, to the best of our knowledge, a list of available solvers for the semantics reported in previous sections.