On the Splitting Property for Epistemic Logic Programs (Extended Abstract)

1 Introduction

The language of epistemic specifications, proposed by Gelfond [1991], constituted an extension of disjunctive logic programming that introduced modal operators to quantify over the set of stable models [Gelfond and Lifschitz, 1988] of a program. These new constructs were later incorporated as an extension of the Answer Set Programming (ASP) paradigm in different implemented solvers (see Lecrerc and Kahl 2018 for a recent survey). The new constructs, subjective literals, have the form Kl and Ml and allow respectively checking whether an objective literal l is true in every stable model

∗This work is based on "Splitting Epistemic Logic Programs," which was presented at the International Conference on Logic Programming and Non-Monotonic Reasoning, LPNMR 2019 [Cabalar et al., 2019b] awarded as best technical paper. It was partially supported by the Ministry of Science and Innovation, Spain (TIC201784453-P), Xunta de Galicia, Spain (GPC ED431B 2019/03), the Centre International de Math´ematiques et d'Informatique de Toulouse (CIMI) through contract ANR-11-LABEX-0040-CIMI within the program ANR-11-IDEX-0002-02 and the Alexander von Humboldt Foundation.

(cautious consequence) or in some stable model (brave consequence). In many cases, these subjective literals can be seen as simple queries, but what makes them really interesting is their use in rule bodies, which may obviously affect the set of stable models they are meant to quantify. This feature makes them suitable for modelling introspection, that is, reasoning about the knowledge and lack of knowledge that the system possesses rather than reasoning exclusively about the facts themselves. However, at the same time, it easily involves cyclic specifications whose intuitive behaviour is not always easy to define. For instance, the semantics of epistemic specifications may yield alternative sets of stable models, each set being called a world view. Deciding the intuitive world views of a cyclic specification has motivated a wide debate in the literature. In fact, in Gelfond's original semantics [G91; Gelfond 1991] or in its extensions to arbitrary propositional formulas [Wang and Zhang, 2005; Truszczy´nski, 2011], some cyclic examples manifested selfsupportedness, so Gelfond [2011] himself and, later on, other authors [Kahl et al., 2015; Fari˜nas del Cerro et al., 2015; Shen and Eiter, 2017; Cabalar et al., 2019a] proposed different variants trying to avoid unintended results.

Epistemic logic programs constitute a syntactic fragment of arbitrary epistemic theories that is aligned to the syntax of logic programming. In this paper we review a property called epistemic splitting [Cabalar et al., 2019b], which not only defines an intuitive behaviour for stratified epistemic logic programs but also goes further, extending the splitting theorem, well-known for standard logic programs [Lifschitz and Turner, 1994], to the epistemic case. Informally speaking, we say that an epistemic logic program can be split if a part of the program (the top) only refers to the atoms of the other part (the bottom) through subjective literals. A given semantics satisfies epistemic splitting if, given any split program, it is possible to get its world views by first obtaining the world views of the bottom and then using the subjective literals in the top as "queries" on the bottom part previously obtained. If epistemic splitting holds, the semantics immediately satisfies other properties. For instance, if the use of epistemic operators is stratified, the program has a unique world view at most. Similarly, subjective constraints (those only consisting of subjective literals) can be guaranteed to only rule out candidate world views. However, we will see that, among the previously cited approaches, only the G91

semantics and the recently proposed Founded Autoepistemic Equilibrium Logic [Cabalar et al., 2019a] satisfy epistemic splitting. So, somehow, most of the recent attempts to fix the behaviour of cycles have neglected the attention on the effects produced on acyclic specifications.

The rest of the paper is organised as follows. First, we motivate the main idea through a well-known example. After that, we recall definitions of epistemic logic programs and introduce the notion of an abstract semantics. In the next section, we review the property of epistemic splitting and some of its consequences. Finally, we conclude the paper with a summary of the state-of-the-art with respect to this property.

2 Motivation

To illustrate the intuition behind our proposal, let us consider the following well-known standard example introduced in [Gelfond, 1991].

Example 1 A given college uses the following set of rules to decide whether a student X is eligible for a scholarship:

Here, '∼' stands for strong negation and high(X) and fair(X) refer to the grades of student X. We want to encode the additional college criterion "The students whose eligibility is not determined by the college rules should be interviewed by the scholarship committee" as another rule in the program. □

The problem here is that, for deciding whether eligible(X) "can be determined," we need to check if it holds in all the answer sets of the program, that is, if it is one of the cautious consequences of the latter. For instance, if the only available information for some student mike is the disjunction

we get that program {(1) - (4)} has the following two stable models:

so eligible(mike) cannot be determined and an interview should follow. Of course, if we just want to query cautious and brave consequences of the program, we can do it inside ASP. For instance, the addition of constraint

allows us to decide if eligible(mike) is a cautious consequence by just checking that the resulting program has no answer sets. The difficulty comes from the need to derive new information from a cautious consequence. This is where subjective literals come into play. Rule

allows us to prove that interview(X) holds whenever neither eligible(X) nor ∼eligible(X) are cautious consequences of

{(1) - (4)}. Recall that Kl holds when the literal l is true in all stable models of the program. The novel feature here is that (7) is also part of the program, and so, it affects the answer sets queried by Kl too, which would actually be:

So, there is a kind of cyclic reasoning: operators K and M are used to query a set of stable models that, in their turn, may depend on the application of that query. In the general case, this kind of cyclic reasoning is solved by resorting to multiple world views, but in our particular example this does not seem to be needed. One would expect that separating the queried part {(1) - (4)} and the rule that makes the query (7) should be correct, since the first four rules do not depend on (7) and the latter exclusively consults them without interacting with their results. A similar line of reasoning could be applied if we added one more level such as, for instance, by including the rule:

The two answer sets of program {(1) - (7)} contain interview(mike) and so appointment(mike) can be added to both answer sets incrementally. This method of analysing a program by division into independent parts shows a strong resemblance to the splitting theorem, well-known for standard ASP. Splitting is applicable when the program can be divided into two parts, the bottom and the top, in such a way that the bottom never refers to head atoms in the top. When this happens, we can first compute the stable models of the bottom and then, for each one, simplify the top accordingly, getting new stable models that complete the information. We could think about different ways of extending this method for the case of epistemic logic programs, depending on how restrictive we want to be on the programs where it will be applicable. However, we choose a very conservative case, looking for a wider agreement on the proposed behaviour. The condition we impose is that our top program can only refer to atoms in the bottom through epistemic operators. In this way, the top is seen as a set of rules that derive facts from epistemic queries on the bottom. Thus, each world viewW of the bottom will be used to replace the subjective literals in the top by their truth value with respect to W.

3 Epistemic Logic Programs

Given a set of atoms At, an objective literal is either an atom or a truth constant 1 , that is a ∈ At ∪ {⊤,⊥}, or an atom preceded by default negation, not a. A subjective literal is any expression of the formKl, Ml, not Kl or notMl, with l an objective literal. A literal is either an objective or subjective literal. A rule r is an implication of the form:

with n ≥ 0 and m ≥ 0, where each ai ∈ At is an atom and each Lj a literal. A rule is called objective if all literals in it are objective. The left hand disjunction of (11) is called the rule head and abbreviated as Head(r). The right hand side of (11) is called the rule body and abbreviated as Body(r). The sets Bodyobj(r) and Bodysub(r) respectively contain the objective and the subjective literals in Body(r). We write Atoms(F) to represent the set of atoms occurring in any syntactic construct F (a literal, head, body, rule or program). By abuse of notation, we will sometimes respectively write Head(r) and Body(r) instead of Atoms(Head(r)) and Atoms(Body(r)) when it is clear by the context.

1 For a simpler description of program transformations, we allow truth constants where ⊤ denotes true and ⊥ denotes false.

A rule r with Head(r) = ∅ is called a constraint. If in addition Bodyobj(r) = ∅, then it called a subjective constraint. We assume that strong negation '∼a' is just another atom in At and that the constraint ⊥ ← a, ∼a is implicitly included in the program. We allow the use of variables, but understood as abbreviations of their possible ground instances.

A programΠ is a (possibly infinite) set of rules. It is called objective if all its rules are objective. An objective program is consistent if it has a stable model in the sense of [Gelfond and Lifschitz, 1988]. A propositional interpretation I is a set of atoms. A belief view W is a non-empty set of propositional interpretations.

Definition 1 (Abstract semantics) An (abstract) semantics S is a function mapping each program into set of belief views satisfying the following conditions:

• if Π is a consistent objective program, then S(Π) is the set of stable models of Π;
• otherwise, S(Π) is the empty set.

Given a program Π, each belief view in S(Π) is called a S-world view of Π. □

4 Epistemic Splitting Property

We proceed now to introduce our definition of the epistemic splitting property. To do so, we begin by extending the idea of splitting set from [Lifschitz and Turner, 1994].

Definition 2 (Epistemic splitting set) A set of atoms U ⊆ At is said to be an epistemic splitting set of a program Π if for any rule r in Π one of the following conditions hold

• (i) Atoms(r) ⊆ U,

We define a splitting of Π as a pair 〈BU(Π), TU(Π)〉 satisfying BU(Π) ∩ TU(Π) = ∅ and BU(Π) ∪ TU(Π) = Π, and also that all rules in BU(Π) satisfy (i) and all rules in TU(Π) satisfy (ii). □

With respect to the definition of splitting sets for objective (i.e. standard) programs, we have replaced the condition for the top program, Head(r) ∩ U = ∅, by the new condition (ii). This essentially means that the top program may only refer to atoms U in the bottom through epistemic operators. This introduces a new kind of "dependence" in the sense that, as happens with head atoms, objective literals in the body also depend on atoms occurring in subjective literals. For instance, U= {p, q} is not an epistemic splitting set of programΠ1 = {p∨q , s ← p,Kq} because of the second rule: s ̸∈ U requires p ̸∈ U. The reason for this restriction is to avoid imposing (to a potential semantics) a fixed way of evaluating p with respect to the world view [{p}, {q}] for the bottom. Another observation is that we keep the definition of BU(Π) and TU(Π) non-deterministic: some rules can be arbitrarily included in one set or the other. These rules correspond to subjective constraints on atoms in U, since these are the only cases that may satisfy conditions (i) and (ii) simultaneously.

Continuing with our motivating example, we can see that the set U consisting of atoms high(mike), fair(mike), eligible(mike),minority(mike) and their corresponding strong negations is an epistemic splitting set that divides program Π2 = {(1) - (7)} into a bottom BU(Π2) = {(1) - (4)} and top part TU(Π2) = {(7)}. As in objective splitting, the idea is computing first the world views of the bottom program BU(Π) and, for each one, simplifying the corresponding subjective literals in the top program. Given an epistemic splitting set U for a program Π and a set of interpretations W, we define EU(Π,W) def = TU(Π)WU , that is, we make the subjective reduct of the top with respect to W and signature U.

Definition 3 Given a semantics S, a pair 〈Wb,Wt〉 is said to be an S-solution of Π with respect to an epistemic splitting set U if Wb is a S-world view of BU (Π) and Wt is a S-world view of EU (Π, Wb). □

This definition is semantics-dependent in the sense that each alternative semantics S for epistemic specifications may define its own S-solutions for a given U and Π. This is because different semantics may define the selected S-world views for a program in a different way. Back to our example, notice that BU(Π2) is an objective program without epistemic operators. Thus, any semantics provides Wb = [{fair(mike)}, {high(mike), eligible(mike)}] as the unique world view for the bottom. The corresponding simplification of the top would be EU(Π2,Wb) containing (after grounding) the single rule

Again, this program is objective and its unique world view is Wt = [{interview(mike)}]. Now, in the general case, to reconstruct the world views for the global program, we define the operation:

(remember that both the bottom and the top may produce multiple world views, depending on the program and the semantics we choose). In our example, Wb ⊔Wt would exactly contain the two stable models (8) and (9) we saw in the introduction.

Property 1 (Epistemic splitting) A semantics S satisfies epistemic splitting if for any epistemic splitting set U of any program Π: W is an S-world view of Π iff there is an S-solution 〈Wb,Wt〉 of Π with respect to U such that W = Wb ⊔ Wt. □

In our running example, it can be easily seen that the world view we obtain in two steps is indeed the unique world view of the whole program, under any semantics satisfying epistemic splitting. Uniqueness of world view was obtained in this case because both the bottom program BU(Π2) and the top, after simplification, EU(Π2,Wb) were objective programs. In fact, as we see next, we can still get a unique world view (at most) when there are no cyclic dependences among subjective literals. This mimics the well-known result for stratified negation in logic programming. Let us define a modal dependence relation among atoms in a program Π so that dep(a, b) is true iff there is a rule r ∈ Π such that a ∈ (Head(r) ∪ Bodyobj(r)) and b ∈ Bodysub(r).

Definition 4 (Epistemic stratification) We say that an epistemic program Π is epistemically stratified if we can assign an integer mapping λ : At → N to each atom such that

1. λ(a) = λ(b) for any rule r ∈ Π and atoms a, b ∈ (Atoms(r) \ Bodysub(r)),
2. λ(a) > λ(b) for any pair of atoms a, b satisfying dep(a, b). □

Take, for instance, the program Π3 = {(1) - (7), (10)}. We can assign atoms high(mike), fair(mike), minority(mike) and eligible(mike) layer 0. Then interview(mike) could be assigned layer 1 and, finally, appointment(mike) can be located at layer 2. So, Π3 is epistemically stratified.

Theorem 1 Let S be any semantics satisfying epistemic splitting and let Π be a finite, epistemically stratified program. Then, if Π has some S-world view, this is unique. □

The proof of the theorem just relies on multiple applications of splitting to each layer and the fact that each simplification EU(Π,Wb) will be an objective program. This is very easy to see in the extended example Π3. We can split the program using as U all atoms but appointment(mike) to get a bottom Π2 and a top {(10)}. Program Π2 can be split in its turn as we saw before, producing the unique world view [(8), (9)]. Then EU(Π3, [(8), (9)]) contains the single rule

This is also an objective program whose unique world view is [{appointment(mike)}] and, finally, the combination of these two world views yields again a unique world view

[ (8)∪{appointment(mike)} , (9)∪{appointment(mike)} ]

Epistemic splitting not only guarantees the existence of (at most) one world view for an epistemically stratified program but, in fact, it also forces all semantics that fulfill that property to coincide on this class of programs [Fandinno, 2019, Theorem 7] - that is, either none has a world view or all of them yield the same, unique world view.

Property 2 (Subjective constraint monotonicity) A semantics S satisfies subjective constraint monotonicity if, for any epistemic program Π and any subjective constraint r, W is a world view of Π ∪ {r} iff both W is a world view of Π and W satisfies r. □

Theorem 2 Epistemic splitting implies subjective constraint monotonicity. □

5 Conclusions

We review a formal property for epistemic logic programs called epistemic splitting. This property has a strong resemblance to the splitting theorem well-known for regular ASP programs. Epistemic splitting can be applied when we can divide an epistemic logic program into a bottom part for a subset U of atoms and a top part, that only refers to atoms in U through subjective literals (those using modal epistemic operators). When this happens, it allows obtaining the world views of the program in two steps: first, computing the world views of the bottom and, second, using each bottom world viewW to replace subjective literals for atoms in U in the top by their truth value with respect to W. One interesting consequence of this property is that programs that are stratified with respect to subjective literals have a unique world view, at most. Another consequence is that constraints only consisting of subjective literals have a monotonic behaviour, ruling out world views that satisfy the constraint body.

Our study of the main semantics in the literature shows that only a bunch of semantics satisfy the epistemic property we studied. Table 1 is taken from [Fandinno, 2019] and summarises the known results for different semantics with respect to the properties discussed through this paper plus the foundedness property from [Cabalar et al., 2019a]. Recall that most of the semantics were born motivated by the existence of selfsupported world views in the G91 semantics: for instance, the program consisting of the single rule a ← Ka yields two world views [∅] and [{a}] but the latter justifies the atom a by the mere assumption of Ka without further evidence, something that seems counterintuitive. The foundedness property precisely characterises this problem in terms of unfounded sets and, as shown in the table, is currently satisfied only by C19, which in addition keeps the good behaviour of G91 with respect to epistemic splitting and subjective constraint monotonicity.

Recall that our main motivation when defining the splitting property was to establish a minimal requirement that seemed reasonable. Still, this property was not satisfied by most semantics. On the other hand, semantics that satisfy this property may satisfy even stronger notions of splitting worth studying. Finally, we refer to [Cabalar et al., 2019b] for more details about epistemic splitting. In particular, how this property may facilitate the simple application of the generatedefine-test methodology to the formalisation of conformant planning.