Top-down Splitting Property for Epistemic Logic Programs

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

• eol>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 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 specicfi 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 (abstract) 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 computation 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 epistemic 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 ifrst 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 metareasoning 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 topdown 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 K1, . . . , 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 correspondence); – 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 {K1, . . . , 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 substituting 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 Topdown 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].

Here, (Π 1) consists of rule (r1), and (Π 1) of constraint (C). So, ′ (Π 1) is (where is a fresh atom): | ⊥ ←

(1) K () 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 (Π1)( ), then it is the one selected by our 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:

Here, (Π 0) consists of rule (r1), and (Π 0) of rule (r2) and constraint (C). So, ′ (Π 0) is (where is a fresh atom): | ← ←

(1)

K (2) () | ← ← (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 ) eligible(X ) ← minority (X ), fair (X ) noeligible(X ) ← fair (X ), high(X ) fair (mike) | high(mike) (1) (2) (3) ( 1) (5) interview (X ) ←

K eligible(X ), K noeligible(X ) (4) appointment (X ) ←

K interview (X )

Since in this version of the program we have only mike as an individual, we may obtain the following ground abbreviated version: ← ← ← | ℎ ← ← ℎ , , ℎ K, K (4) K (1) (2) (3) ( 1) (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), 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 | | ← , (4′) ← ← ← | ℎ ℎ , , ℎ (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. [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 programs, 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.

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. Truszczyn´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. Kowalski , K. Bowen (Eds.), Proceedings of the 5th Intl. Conf. and Symposium on Logic Programming , 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. Truszczyn ´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 TwentySeventh 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-efcfiient 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 programming , TPLP 14 ( 2014 ) 415 - 427 .