Epistemic Equilibrium Logic

1 Introduction

Gelfond extended disjunctive answer set programs by epistemic operators in order to quantify over answer sets [Gelfond, 1991; 1994; Baral and Gelfond, 1994]. He called programs with epistemic operators in rule bodies epistemic specifications. They allow to reason about incomplete information, understood as situations where there are multiple answer sets. The semantics of epistemic specifications is in terms of world views, which are maximal collections of answer sets. Similar to answer set semantics, a world view S of an epistemic specification � is defined by means of the reduct � S of � by S. The construction is in two steps: first, compute the reduct � S , eliminating the modal operators; second, compute the maximal collection of answer sets of � S and check whether it equals S.

Subsequently various di�erent semantics were proposed for epistemic specifications [Chen, 1997; Wang and Zhang, 2005; Truszczy´nski, 2011; Gelfond, 2011; Kahl, 2014]. Some propose other definitions of reducts, while others propose semantics inspired by the Kripke semantics of modal logics. We here introduce a new semantics that is based on an epistemic extension of Pearce's equilibrium logic [1996;

� We thank Pedro Cabalar, Michael Gelfond, Patrick Thor Kahl and David Pearce for useful discussions and feedback. Our work was supported by the French-Spanish Lab of Advanced Studies in Information Representation and Processing (LEA CNRS).

2006]. This had been undertaken by Wang and Zhang [2005], however for the somewhat outdated version of epistemic specifications of [Gelfond, 1991; 1994]. Our version is closer to Gelfond's [2011] and Kahl's [2014] more recent versions.

Pearce's equilibrium logic allows to characterise answer set semantics of non-epistemic logic programs. The underlying here-and-there logic (HT) characterises their strong equivalence [Lifschitz et al., 2001]. We here add two epistemic operators K and ˆK to the language of HT and define epistemic HT models (EHT models). We then define epistemic equilibrium models by generalising the usual minimality criterion over HT models to EHT models. We finally define autoepistemic equilibrium models (AEEMs) as epistemic equilibrium models that are maximal both under set inclusion and under a preference ordering on epistemic equilibrium models. The latter provide a new logical semantics for epistemic specifications and more generally for nested epistemic logic programs. We establish a strong equivalence result and compare our semantics with existing approaches. We demonstrate by means of examples that all other semantics di�er from our approach and that Kahl's comes closest.

The rest of the paper is organised as follows. Section 2 recalls epistemic specifications. Section 3 introduces the logic EHT. Section 4 defines epistemic equilibrium models (EEM) and autoepistemic equilibrium models (AEEM). Section 5 compares the latter with existing semantics of epistemic specifications, in particular with Kahl's. Section 6 provides strong equivalence characterisations in terms of EHT equivalence for both kinds of models. Section 7 concludes.

2 Epistemic specifications

Several versions of epistemic specifications were introduced by Gelfond [1991; 2011]. Kahl [2014] recently proposed a further improvement that we recall here.

2.1 The language of epistemic specifications

The language of epistemic specifications extends that of disjunctive logic programming by the modal operator K . The formula K' is read "' is known to be true". 1 Literals of this language are of three di�erent kinds: objective literals (l), extended objective literals (�) and extended subjective literals (L). They are defined by the following grammar:

1 The original presentation also has a modal operator M that is dual to K : instead of K not l it has not M l and instead of not K not l it has M l. Due to this definability via K we do without M here.

L FK� j notK�

where p ranges over the set of propositional variables P. So the language has two negations: strong negation � and default negation not , where not ' is read "' is false by default". 2

A rule � is of the form

where the literals of the head l1 or : : : or lm are objective literals and the literals of the body G1; : : : ; Gn are extended literals (either extended objective literals or extended subjective literals). We suppose that the head of � is ? if m = 0 and that the body of � is > if n = 0.

An epistemic specification is a finite collection of rules. Here is Gelfond's [1991] 'eligibility' example that was taken up in almost all papers on epistemic specifications:

where h stands for 'high GPA', f stands for 'fair GPA', e stands for 'eligible for scholarship' and i stands for 'to be interviewed'. Let us call that epistemic specification �G.

2.2 The semantics of epistemic specifications

Let S be a consistent set of objective literals, i.e., a set of objective literals such that there is no p 2 P with both p 2 S and �p 2 S . Satisfaction of extended objective literals in S is defined by:

Let S be a non-empty collection of such consistent S 's. Satisfaction of extended subjective literals in S is defined by:

For example, � fpg � j=ES notKnot p because � fpg � 6 j=ES K not p.

Let � be an epistemic specification and let S be a nonempty collection of consistent sets of objective literals. Whether S is a world view of � is decided by computing the reduct of � and then checking a fixed-point equation. The reduct � S of a rule � 2 � with respect to S is obtained from � by eliminating the K operator according to Table 1. The reduct of � with respect to S, noted � S , is then defined as

2 Gelfond's original language is slightly di�erent, with �K l instead of notK l, etc. They however have the same semantics, mutatis mutandis.

Finally, S is a world view of � if it equals the set of all answer sets of � S . As the case notKnot l may introduce double negation notnot l, the computation of such answer sets has to resort to answer-set programming with nested expressions [Lifschitz et al., 1999].

For example, the only world view of Gelfond's 'eligibility' specification �G of Section 2.1 is � fh; e; ig; f f ; ig � . Table 2 contains more examples. The reduct of � p K p � by � ; � is p ? and its reduct by � fpg � is p p. Both have exactly one answer set: � ; � . Only the former matches its reduct, so the unique world view is � ; � . The reduct of � porq ; p notKnotq � by � fpg � is � porq ; p notnotq � and its reduct by � fqg � is � porq ; p > � . Both have exactly one answer set: fpg; therefore the former � fpg � is the unique world view. 3

Observe that when � does not contain K then it has at most one world view: the collection of all answer sets of �.

3 Epistemic here-and-there logic EHT

The logic of here-and-there HT is a monotonic three-valued logic that is intermediate between classical logic and intuitionistic logic. An HT model is an ordered pair (H; T) of valuations (sets of propositional variables) satisfying the heredity constraint H � T. In this section we introduce epistemic HT logic (EHT), which extends HT by two epistemic modal operators K and ˆK in the spirit of intuitionistic modal logics [Fischer-Servi, 1976; Fari˜nas del Cerro and Raggio, 1983; Simpson, 1994; Bierman and de Paiva, 2000]. Its epistemic HT models (EHT models) are collections of HT models. From the perspective of modal logic, an EHT model can be viewed as a refinement of S5 models (which are sets of valuations) where valuations are replaced by HT models.

3.1 The language of EHT

The language of EHT is given by the following grammar:

where p ranges over the set of propositional variables P. An EHT theory is a finite set of EHT formulas, noted �, �, . . .

3 Gelfond's [2011] approach di�ers for the case notK�: when S 6 j= notK� then it is replaced by ?. As a result of this subtle di�erence, Gelfond gets the world views � ; � and � fpg � for the 2nd example, and no world view at all for the 3rd. As Kahl argues, both are not as intuitive as his results.

The set of propositional variables occurring in a formula ' is noted P '. For example, PK(p!q) = fp; qg. This generalises to EHT theories: P� = S '2� P '.

As usual, >, :' and ' $ respectively abbreviate ?!?, '!? and ('! ) ^ ( ! '). A formula is said to be nonmodal if it does not contain the modal operators K and ˆK .

3.2 EHT models

An EHT model is an ordered pair � T ; ~ � in which

• � T � 2 P is a nonempty set of valuations;
• � ~ : T ! 2 P is a map such that ~(T) � T for every T 2 T .

When T = fTg is a singleton then the EHT model � T; ~ � can be identified with the HT model (~(T); T).

The inclusion constraint on ~ generalises the heredity constraint of HT logic to EHT. We say that � T; ~ � is total on S � T if ~(T) = T for every T 2 S. When � T; ~ � is total on T then ~ is the identity function id. We identify � T; id � with the classical S5 model T .

A pointed EHT model is a pair �� T ; ~ � ; T0 � where � T ; ~ � is an EHT model and T0 2 T , the latter being the actual world. A multipointed EHT model is a pair �� T ; ~ � ; T0 � where � T ; ~ � is an EHT model and T0 � T .

3.3 EHT truth conditions

We now define the satisfaction relation for EHT formulas. Those for ?, ^ and _ are standard.

It follows that for negation we have

� T ; ~ � ; T j=EHT :' i� � T; ~ � ; T 6 j=EHT ' and � T; id � ; T 6 j=EHT ': This can be simplified further, see Proposition 3.5.1 below. For example, � T; ~ �

; T0 j=EHT p_:p i� p 2 ~(T0) or p < T0. Raising the bar of our examples,

When for an EHT model � T; ~ � and a set of designated worlds T0 � T we have � T; ~ � ; T j=EHT ' for every T 2 T0 then we write � T; ~ � ; T0 j=EHT ' for short. We call �� T ; ~ � ; T0 � a multipointed EHT model of '. Finally, we write � T ; ~ � ; T0 j=EHT �when � T; ~ � ; T0 j=EHT ' for every ' 2 �.

Proposition 3.1. The following are equivalent.

• � � T; ~ � ; T j=EHT �;
• � � T; ~ � ; T j=EHT K( V �) for every T 2 T;
• � � T; ~ � ; T j=EHT K( V �) for some T 2 T.

An EHT model � T; ~ � can alternatively be described as a collection � (~(T); T) � T2T of HT models. We display concrete pointed and multipointed models as collections � (~(T ); T ) � T2T where the actual worlds are underlined. Here are some examples:

� (;; fpg); (;; fqg) � j=EHT :p � (;; ;) � j=EHT :K:p ! p � (;; fpg); (;; fqg) � j=EHT ::p � (fpg; fpg) � j=EHT :K:p ! p � (;; fpg); (;; fqg) � j=EHT :K:p � (;; fpg) � 6 j=EHT :K:p ! p

Observe that the satisfaction of formulas of the form K', :K', ::K', ˆK', :ˆK' and ::ˆK' does not depend on the designated worlds: when � T; ~ � ; T0 j=EHT K' for some T0 � T then � T; ~ � ; T0 j=EHT K' for every T0 � T, etc.

The next result is the heredity property in EHT: if a formula has an EHT model then it also has a classical S5 model.

We now list some useful properties.

Proposition 3.3. Let ' be an EHT formula. Then:

1. � T; ~ � ; Tj=EHT:' i� � T; id � ; T6 j=EHT';
2. � T; ~ � ; Tj=EHT::' i� � T; id � ; T j=EHT';
3. � T; ~ � ; Tj=EHT:K' i� � T; id � ; T 0 6 j=EHT' for some T 0 2 T;

We end with an appropriate definition of bisimilarity. Let � T1; ~1 � and � T2; ~2 � be two EHT models and P � P. A relation Z � T1 � T2 is called a P-bisimulation if

1. both Z and Z �1 are serial 4 , and
2. if T1ZT2 then T1\P = T2\P and ~1(T1)\P = ~2(T2)\P.

If there exists a P-bisimulation Z between � T1; ~1 � and � T2; ~2 � such that T1ZT2 then T1 and T2 are called Pbisimilar.

Proposition 3.4. Let ' be an EHT formula. Let �� T1; ~1 � ; T1 � and �� T2; ~2 � ; T2 � be two pointed EHT models such that T1 and T2 are P '-bisimilar. Then

3.4 EHT validity

A formula ' is called EHT valid if � T ; ~ � ; T j=EHT ' for every EHT model � T; ~ � .

All principles of intuitionistic modal logics that were studied in the literature [Simpson, 1994] are EHT valid. As always in intuitionistic modal logics, K and ˆK are not dual: while ˆK' ! :K:' is valid, the other direction is not. Here are some more examples: K' ! :ˆK:', :ˆK:' ! ::ˆK' and ::K' ! :K:' are all valid while their converses are not. On the other hand, none of ::K' ! K' and K::' ! K' is EHT valid. The same holds if we replace K by ˆK . (The EHT model �� ;; fpg �� provides a countermodel for all examples above.) However:

Proposition 3.5. The equivalences :K' $ ˆK:' and : ˆK ' $ K :' are EHT valid.

4 Epistemic and autoepistemic equilibrium models

Pearce defined equilibrium models (EMs) of a formula as classical models satisfying a minimality condition when viewed as total HT models. Our epistemic equilibrium models (EEMs) generalise such models from classical to S5 models in a natural way. Such models however only minimise truth, while the semantics of epistemic specifications involves also a minimisation of knowledge. We therefore define autoepistemic equilibrium models (AEEMs) as EEMs that are maximal under some order that comprises set inclusion.

4 The relation Z � T1 � T2 is serial when for every T1 2 T1 there is a T2 2 T2 such that � T1; T2 � 2 Z.

4.1 Epistemic equilibriummodels

We have already observed that total EHT models can be identified with classical S5 models: for T � 2 P and T0 2 T, we write T; T0 j=S5 ' instead of � T; id � ; T0 j=EHT '. We define the epistemic equilibrium models of ' as particular S5 models:

Table 3 illustrates our definition by means of the EHT counterparts of the epistemic specifications of Table 2 together with their world views and EEMs. Note that not every EEM is also a world view.

Proposition 4.1. Let ' be an EHT formula.

1. If ' is EHT valid then EEM(') = n� ; �o .
2. If � ; � j=S5 ' then EEM(::') = n� ; �o and EEM(:') = ;. If � ; � 6 j=S5 ' then EEM(::') = ; and EEM(:') = n� ; �o .
3. EEM(K') = EEM(').
4. If EEM(') = ; then EEM( ˆK') = ;.

Proposition 4.2. Let ' be a non-modal EHT formula. Let EM(') be the set of (classical) equilibrium models of '.

We illustrate the above propositions by two examples. Remember that EM(p_:p) = � ;; fpg � . It follows from Proposition 4.2 that ˆK(p_:p) has the EEMs � ; � and � fpg � and that p_:p has one more EEM, viz. � ;; fpg � . It then follows from Proposition 4.1.3 that the EEMs of K(p_:p) are � ; � , � fpg � and � ;; fpg � . Remember that ::p has no EMs: the only candidate is ;, but ; 6 j= p. So ::p, ˆK::p and K::p have no EEMs (cf. Proposition 4.1.2), and neither do :K:p and : ˆK:p (cf. Proposition 3.5).

4.2 Autoepistemic equilibriummodels

While EEMs provide an interesting epistemic generalisation of EMs, they are somewhat too weak to provide an interesting semantics of epistemic specifications. Consider the 2nd epistemic specification :K:p ! p of Table 3: its EEM � ; �

seems to contradict our intuitions about epistemic specifications. Roughly speaking, the interpretation of K in EEMs should quantify over all possible answer sets. We take that set to be S EEM(') and we are going to select the most preferred EEMs in EEM(') under set inclusion and an ordering that is determined by the answer sets from S EEM(') that can be taken into account.

We start by defining a nonmonotonic satisfaction relation j= � for multipointed S5 models � T; T0 � involving minimisation of truth over the set of designated worlds T0:

The first condition requires that for the total multipointed EHT model � T; id � ; T0 we have � T; id � ; T0 j=EHT '. The second 'minimality of truth' condition, requires that there be no EHTmodel �� T; ~ � ; T0 � of ' strictly weaker than �� T ; id � ; T0 � on T0, where by the latter we understand that ~(T) � T for some T 2 T0 and ~(T) = T for every T 2 T n T0. Here are two examples (remember that the designated worlds are underlined):

• � � fpg; ; � 6 j= � :K:p!p because � fpg; ; � 6 j=S5 :K:p!p.
• � � fpg; ; � j= � :K:p!p because � fpg; ; � j=S5 :K:p!p and � (;; fpg); (;; ;) � 6 j=EHT :K:p!p.

Let ' be an EHT formula. We define a '-indexed partial preorder over S5 models by:

The strict version of �' is defined as usual:

When T <' S we say that S is preferred over T for '.

We are then interested in EEMs of ' that are maximal w.r.t. set inclusion and w.r.t. � ': we say that T is an autoepistemic equilibrium model (AEEM) of ' if

1. T 2 EEM(');
2. there is no S 2 EEM(') such that T � S;
3. there is no S 2 EEM(') such that T <' S.

For example, K(p_q) has three EEMs � fpg � , � fqg � and � fpg; fqg � . While they are incomparable under �', the latter is the only AEEM because it is set-inclusion maximal. Consider again � � = :K:p ! p of Table 3. For its two EEMs � ; � and � fpg � we have � ; � <� � � fpg � . This is the case because � ;; fpg � j= � � � while � ;; fpg � 6 j= � � � . So � fpg � is the only AEEM of � � , matching Kahl's semantics.

When ' has an EEM then ' also has an AEEM. It follows from Proposition 4.2 that a nonmodal formula ' has at most AEEM: the set of all EMs of '.

Proposition 4.3. If EEM(') = ; then ' has no AEEM. If EEM(') is a singleton then then the AEEMs of ' equal the EEMs of '.

5 AEEMs for epistemic specifications

We now compare AEEMs with existing semantics for epistemic specifications. But first we translate epistemic specifications into EHT formulas.

5.1 Embedding epistemic specifications

Let � be an epistemic specification. Our translation (:) � replaces ' ', ' or ', ';' and 'not ' respectively by '!', '_', '^' and ':'. Furthermore, it introduces a fresh variable ˜p for each �p occurring in �. For these new variables, the formula Cons(�) = V p2P� :(p^ ˜p) ensures that p and ˜p cannot be true at the same time. (We only need it for those p that are prefixed by a strong negation in �.) Here is an example:

5.2 Comparison with Kahl's semantics

We now compare Kahl's world views of an epistemic specification � with our AEEMs of � � . We do so by means of a series of examples most of which stem from [Kahl, 2014].

Table 4 lists epistemic specifications together with their (ordered) EEMs. The only example where the two semantics di�er is the last one. The intuitions of quantification about answer sets seem to argue in favour of our semantics here.

Let us terminate with the AEEMs of Gelfond's 'eligibility' specification �G of Section 2.1. The formula � � G has three EEMs: T1 = � fh; e; ig; f f ; ig � , T2 = � fh; eg � and T3 = � f f ; ig � of which only T1 is intended. It can be checked that T3 � T1 and T2 <� � G T1.

5.3 Comparison with older approaches

We here discuss some older approaches that tried to generalise or to refine epistemic specifications and then compare our approach to an epistemic extension of equilibrium logic that is due to Wang and Zhang [2005] and that is close in spirit to our approach. All the approaches that we discuss here deal with the former version of epistemic specifications of [Gelfond, 1991; 1994; Baral and Gelfond, 1994], which behaves di�erently from the more recent versions in [Gelfond, 2011; Kahl, 2014].

As far as we know, the first embedding of epistemic specifications into an epistemic modal logic with a kind of minimal model reasoning about epistemic concepts knowledge and belief was Chen's [1997]. His approach significantly di�ers from ours because our approach is in terms of an intuitionistic modal logic with non-dual epistemic operators. More recently, Truszczy´nski [2011] proposed a refinement of epistemic specifications. His approach allows for the model � ; � of the formula (p_:p) ! p, which departs from all other approaches (in particular it has no EMs).

Wang and Zhang (WZ) [2005] described an epistemic extension of equilibrium logic into which they were able to embed Gelfond's first version of epistemic specifications. This extension also gives semantics to nested epistemic logic programs. The language extends that of HT by two modal operators K and M. Let us call WZ-EHT models their epistemic HT models. A WZ-EHT model is a triple (A; H; T) where A � 2 P is a collection of valuations and (H; T) is an HT model. Note that H and T are not necessarily contained in A. Given A, define the collection

Then the definition of the satisfaction relation can be recast in terms of our semantics as follows:

• A; H; T j=EHT p if p 2 H;
• A; H; T j=EHT K' if coll(A); A j=EHT ' for all A 2 coll(A);

A; H; T j=EHT M' if coll(A); A j=EHT ' for some A 2 coll(A).

Then WZ-EEMs for a theory � are total WZ-EHT models (A; T; T) of � such that there is no EHT model (A; H; T) of � with H � T. Finally, Wang and Zhang define equilibrium views of � to be the maximal collections A � 2 P satisfying the fixed-point equation

While both we and Wang and Zhang propose an epistemic extension of equilibrium logic, there are some fundamental di�erences. Let us summarise the relationship. First, each satisfiable EHT formula has also a WZ-EHT model; the other way round, for instance K p^:p has a WZ-EHT model but no EHT model. Second, the concept of minimality of knowledge di�ers: both K p^:p and K::p have WZ-EEMs but no EEMs in our sense; the other way round, K p^::p has an EEM in our sense, but no WZ-EEM. Third, maximisation of ignorance is not performed in the same way: K p has an AEEM, but no WZ-equilibrium view. The formulas ˆK p, ˆK p^:p, (p_q)^( ˆK q ! p) and p_K (p_:p) are other examples; ( ˆK :p_ ˆK ::p)^( ˆK p ! (p_:p)) has a WZ-equilibrium view, but no AEEM.

6 Strong equivalence

We now show that strong equivalence both in the EEM sense and in the AEEM sense can be captured in EHT. Precisely, we show that EHT validity of the equivalence

characterises that

1. for every �, �1 [� and �2 [� have the same EEMs;
2. for every �, �1 [� and �2 [� have the same AEEMs.

Our proofs are non-trivial generalisations of Lifschitz et al.'s [2001] proof for HT logic. They require the syntactical characterisation of EHT models. To that end, using Proposition 3.4, we may suppose without loss of generality that P is finite. This allows to describe possible worlds and EHT models by means of formulas.

6.1 Some characteristic formulas

Let us define the following:

where T 2 2 P and � T ; ~ � is an EHT model. The formula Total captures that the model is total. At(T) says that we are at a there-world (and not at a here-world). Given an S5 model T , Ch(~) characterises ~: it says that the here-function is either ~ or id.

Lemma 6.1. Let �� T; ~ � ; T0 � be a multipointed EHT model and let T0; T 2 T . Then:

1. � T; ~ � ; T0 j=EHT At(T) i� T0 = T = ~(T0).

1. If � T; ~ 0 � ; T0 j=EHT Ch(h) then ~ 0 = id or ~ 0 = ~.

Proof. We only prove the last item.

Let � T; ~ 0 � ; T0 j=EHT Ch(h). We use that by Lemma 6.1.3, � T ; ~ 0 � ; T j=EHT ::At(T). Suppose ~ 0 , ~. Then there are T 2 T and p 2 T such that either p 2 ~(T) and p < ~ 0 (T), or p < ~(T) and p 2 ~ 0 (T). In the former case, the hypothesis � T ; ~ 0 � ; T0 j=EHT Ch(h) implies that � T; ~ 0 � ; T0 j=EHT p, i.e., a contradiction. In the latter case, as p < ~(T) and p 2 T it implies that � T; ~ 0 � ; T j=EHT Total; then by Lemma 6.1.1 we must have ~ 0 = id. �

6.2 Strong equivalence for EEMs

Lemma 6.2. Let �� T; ~ � ; T0 � be a multipointed EHT model such that ~ is total on T n T0. Then � T; ~ � ; T0 j=EHT �1 and � T ; ~ � ; T0 6 j=EHT �2 implies that there is a theory � such that

Proof. We build two di�erent �, depending on whether T; T0 j=S5 �2 or not.

When T ; T0 6 j=S5 �2 then we define � = fTotalg and prove that T; T0 j= � �1 [ � and T; T0 6 j= � �2 [ �. The latter immediately follows from the hypothesis that T; T0 6 j=S5 �2. As to the former, T; T0 j=S5 �1 [ � is the case because T; T0 j=S5 �1 by hypothesis and heredity and because T; T0 j=S5 Total by Lemma 6.1; moreover, for every ~ 0 , id we have � T ; ~ 0 � ; T0 6 j=EHT Total, again by Lemma 6.1.

When T ; T0 j=S5 �2 then we define � = fCh(~)g and prove that T ; T0 6 j= � �1[� and T; T0 j= � �2[�. The former holds because we are in a situation where � T; ~ � ; T0 j=EHT �1 [ � for a function ~ that is total on T n T0 and that is di�erent from id (because T; T0 j=S5 �2 and � T; ~ � ; T0 6 j=EHT �2). As to the latter: first, we have T; T0 j=S5 �2 by hypothesis and T; T0 j=S5 Ch(~) by Lemma 6.1; second, consider some ~ 0 , id that is total on T n T0. On the one hand, when ~ 0 = ~ then by hypothesis � T; ~ 0 � ; T0 6 j=EHT �2; on the other hand, when ~ 0 , ~ then � T; ~ 0 � ; T0 6 j=EHT Ch(~) by Lemma 6.1. In both cases, � T; ~ 0 � ; T0 6 j=EHT �2 [ fCh(~)g. �

Theorem 6.1. Let �1 and �2 be two EHT theories. The following are equivalent:

1. For every �, �1 [ � and �2 [ � have the same EEMs;

Proof. For the right-to-left direction, suppose K �V �1 � $ K �V �2 � is EHT valid, i.e., no EHT model allows to distinguish K �V �1 � and K �V �2 � . Then � T; ~ � ; T j=EHT �1 i� � T ; ~ � ; T j=EHT �2 by Proposition 3.1. Therefore for every theory �, � T; ~ � ; T j=EHT �1 [� i� � T; ~ � ; T j=EHT �2 [�. It follows that EEM(�1 [ �) = EEM(�2 [ �).

For the left-to-right direction, suppose the equivalence K �V �1 � $ K �V �2 � is EHT invalid. Suppose w.l.o.g. that � T ; ~ � ; T0 j=EHT K �V �1 � and � T; ~ � ; T0 6 j=EHT K �V �2 � . Then � T ; ~ � ; T j=EHT �1 and � T; ~ � ; T 6 j=EHT �2 by Proposition 3.1. By Lemma 6.2 (which is applicable because ~ is trivially total on T n T = ;), we have that there must exist a � such that either T ; T 6 j= � �1[� and T; T j= � �2[�, or T; T j= � �1[� and T ; T 6 j= � �2 [�. So EEM(�1 [�) , EEM(�2 [�). �

6.3 Strong equivalence for AEEMs

We define a further formula characterising the set of all thereworlds of a EHT model � T ; ~ � by means of Jankov-Fine-like formulas [Blackburn et al., 2001]:

Lemma 6.3. Let � S; ~ � be an EHT model. Then

Theorem 6.2. Let �1 and �2 be two EHT theories. The following are equivalent:

1. For every �, �1 [� and �2 [� have the same AEEMs;
2. K �V �1 � $K �V �2 � is EHT valid.

Proof. The proof of the right-to-left direction follows the lines of that of Theorem 6.1.

The proof of the left-to-right direction also follows the lines of that of Theorem 6.1, it is only the construction of the set � of Lemma 6.2 that has to be adapted: the Jankov-Fine formula JF(T ) has to be conjoined with the �s in the proof of Lemma 6.2. Lemma 6.3 guarantees that there is exactly one EEM of �2 [ � (resp. �1 [ �). It then follows from Proposition 4.3 that there also is exactly one AEEM of �2 [ � (resp. �1 [ �). �

7 Conclusion

In this paper, we have designed a monotonic, simple and neat intuitionistic modal logic EHT: the two modal operators K and ˆK that we add to the original language of HT are interpreted in models that are straightforward combinations of the Kripke models for S5 and HT. Based on this logic, we have first defined epistemic equilibrium models (EEMs) by means of a truth-minimising criterion, and then autoepistemic equilibrium models (AEEMs) by maximising ignorance. The latter models are powerful enough to provide a new logical semantics not only for epistemic specifications, but also for programs with arbitrary nestings of K and !. We have provided a strong equivalence characterisation and have compared our semantics with the existing semantics for epistemic specifications.

We believe that EHT and the epistemic and autoepistemic equilibrium logics that we have built on it provide a good starting point for further extensions of answer-set programs by modal concepts. A first step could be the extension from single-agent epistemic logic to multi-agent epistemic logic.