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.
approach) the epistemic expressions that appear in a given program. Many semantic approaches
for ELPs have been introduced beyond the seminal ones, among which [
An interesting attempt to establish useful properties that ELP’s semantics should obey is
presented by Cabalar et al. in [
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.
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., [
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 .
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).
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 |= .
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 cancelling 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 considered 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 Π-′ ⊂ Π- .
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.
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.
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.
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.
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.
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 [{}].
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 [
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.
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 semantics, 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.
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.
We have presented a new semantic approach for ELP, called CF22, which applies in a
straightforward way the underlying principles of the seminal ELP approach as presented and discussed
by Gelfond in [
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 [
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 [
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 [
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 [
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 [
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 [
Differently from F15, FAAEL [
FAAEL satisfies [
We apologize with the readers and with the authors, because for lack of space, we do not
consider other recent semantics, such as [
In Tables 1 and 2 a summary is reported, taken from [
Table 3 shows, to the best of our knowledge, a list of available solvers for the semantics reported in previous sections. 2018 S16 2018 S16 2020 G94