Formal semantics of meta-level architectures: Temporal epistemic reflection

Formal Semantics of Meta-Level Architectures: Temporal Epistemic Reflection Wiebe van der Hoek,1,*,§ John-Jules Meyer,1,† Jan Treur2,‡ 1 Department of Computer Science, Utrecht University, P.O. Box 80.089, 3508 TB Utrecht, The Netherlands 2 Department of Artificial Intelligence, Free University Amsterdam, De Boelelaan 1081a, 1081 HV Amsterdam, The Netherlands

In this article we show how formal semantics can be given to reasoning processes in meta-level architectures that reason about (object level) knowledge states and effects changes may have on them. Especially, attention is focused on the upward and downward reflections in these architectures. Temporalized epistemic logic is used to specify meta-level reasoning processes and the outcomes of these. © 2003 Wiley Periodicals, Inc.

1.

INTRODUCTION

Meta-level architectures (cf. Ref. 1) often are used either to model dynamic control of the object level inferences (e.g., Ref. 2) or extend the inference relation of the object level (e.g., Refs. 3, 4, and 5). In Ref. 6, we introduced formal semantics for meta-level architectures of the first kind based on temporal models. It may be considered quite natural that for such a dynamic type of reasoning system the temporal element of the reasoning should be made explicit in the formal semantics. To use meta-level architectures to extend the object level inference relation, the situation looks different. In principle one may work out formal semantics in terms of (the logic behind) this extended, nonclassical inference relation, e.g., as in the literature for nonmonotonic logics. However, much discussion is possible about this case. Some studies argue that also in the case of a nonmonotonic logic the semantics have to make the inherent temporal element *Author to whom all correspondence should be addressed: e-mail: [email protected]. † e-mail: [email protected]. ‡ e-mail: [email protected]. § Current address: Department of Computer Science, University of Liverpool, Liverpool L697ZF, UK. INTERNATIONAL JOURNAL OF INTELLIGENT SYSTEMS, VOL. 18, 1293–1317 (2003) © 2003 Wiley Periodicals, Inc. Published online in Wiley InterScience (www.interscience.wiley.com). • DOI 10.1002/int.10139

1294

HOEK, MEYER, AND TREUR

explicit; approaches are described in, e.g., Refs. 7 and 8. In this study we adopt this line. In principle, a downward reflection that extends the inference relation of the object level theory disturbs the (classical) object level semantics: facts (assumptions) are added that are not logically entailed by the available object level knowledge. Adding a temporal dimension (in the spirit of Ref. 9) enables one to obtain formal semantics of downward reflection in a dynamic sense: as a transition from the current object level theory to another one (where the reflected assumption has been added). In Ref. 10 a metaphor of a meta-level architecture was exploited to define a nonmonotonic logic, called epistemic default logic (EDL). It was shown how upward reflection can be formalized by a nonmonotonic entailment relation based on epistemic states (according to Ref. 11) and the meta-level reasoning process by an (monotonic) epistemic logic. Compared with a meta-level architecture, what was still missing was a formalization of the step in which the conclusions of the meta-level actually were used to change the object level, i.e., in which formulas ␸ are added to the object level knowledge in order to be able to reason further with them at the object level. This should be achieved by the downward reflection step. In this study we introduce a formalization of this downward reflection step in the reasoning pattern as well. We formalize the semantics of the architecture by means of entailment on the basis of temporalized Kripke models. Thus, a formalization is obtained of the reasoning pattern as a whole, consisting of a process of generating possible default assumptions by meta-level reasoning and actually assuming them by downward reflection (a similar pattern as generated by the so-called biomodular system (BMS) architecture for nonmonotonic reasoning introduced in Ref. 12; for more details, see Ref. 13). The temporal epistemic meta-level architecture (TEMA) described here is a powerful tool to reason with dynamic assumptions: it enables one to introduce and retract additional assumptions during the reasoning on the basis of explicit epistemic information on the current knowledge state and meta-knowledge to determine adequate additional assumptions. This covers a whole class of reasoning patterns of meta-level architectures, which we call TEMA. In such an architecture, upward reflection is restricted to the transfer to the meta-level of epistemic information: information about what currently is known and what is not known at the object level, and downward reflection is restricted to introducing additional information (assumptions) to the object level, based on the conclusions derived at the meta-level. In this architecture a number of interesting reasoning patterns can be formalized in temporal semantics in an intuitive and transparent manner. In Refs. 14 and 15 various applications of the architecture are shown, including hypothetical reasoning, the method of indirect proof, reasoning about knowledge, and reasoning about actions integrated with executing them. The formalization of downward reflection was inspired by Ref. 6, where it is pointed out how temporal models can provide an adequate semantics of meta-level architectures for dynamic control, and Ref. 8, where similar ideas have been worked out to obtain a linear time temporal semantics for default logic. The general idea is that conclusions derived at the meta-level essentially are statements about

TEMPORAL EPISTEMIC REFLECTION

1295

the state of the object level reasoning at the next moment of time. Thus, downward reflection is a shift of time in a (reasoning) process that is described by temporal logic. To get the idea we will use the following informal description of an example of reasoning pattern involving diagnostics (of a car that can not start) by elimination of hypotheses (for a more extensive description; see Ref. 14). Later on (in Section 7.3), we will come back to this example to show how it can be formalized by our approach. Suppose at the object level we have the following (causal) knowledge about a car: ● ● ●

If the battery is empty, then the lights can not burn If the battery is empty or the spark plugs are tuned up badly, then the car does not start The car does not start

At the meta-level, we control a diagnostic reasoning process to find out whether it can be excluded that an empty battery is the cause of the problems (the only hypothesis that we fully consider in this example). To this end, we have the following (simplified) meta-knowledge that enables us to propose hypotheses for elimination and reject them if indeed they turn out to fail: ●

●

●

●

If it is known that the car does not start and it is not known whether the hypothesis “the battery is empty” holds, then “the battery is empty” is an adequate hypothesis to focus on If it is known that the car does not start and it is known that the hypothesis “the battery is empty” does not hold, and it is not known whether the hypothesis “the spark plugs are tuned up badly” holds, then “the spark plugs are tuned up badly” is an adequate hypothesis to focus on If we have focused on a hypothesis X and assuming X we have derived that the observable Y should be the case and it has been observed that Y is not the case, then our hypothesis X should be rejected It has been observed that the lights can burn

Using these two knowledge bases in a TEMA, we can perform the following dynamic reasoning pattern: 1. Draw all conclusions that are possible at the object-level 2. Reflect upward that at the object level it is not known whether the battery is empty 3. Draw the conclusion at the meta-level that “battery is empty” is an adequate hypothesis to focus on 4. Reflect this hypothesis downward; introduce it at the object level as additional information (assumption) 5. Draw the conclusion at the object level that the lights can not burn 6. Reflect upward the information that at the object level it has been found that the lights can not burn 7. Use the observation at the meta-level that the lights can burn and notice the contradictory situation 8. At the meta-level draw the conclusion that the focus hypothesis, “battery is empty,” should be rejected 9. Reflect downwards, that “battery is empty” is considered to be not true

1296

HOEK, MEYER, AND TREUR

This example shows some of the possibilities of temporal epistemic reflections. Notice especially the manner in which we treat epistemic states and additional information in a dynamic manner. This implies that during reasoning, the (states of) object level and meta-level both change in (reasoning) time; temporal logic is exploited to describe these changes in a logical manner. Our approach provides a formalization of upward reflection by a nonmonotonic entailment relation based on epistemic states and downward reflection by an entailment relation based on temporal models. As in the literature, reflections usually are either kept rather restricted (and static) or described in a procedural or syntactic manner (e.g., by means of generalized inference rules; see Ref. 4); the novelty of our approach is that it introduces a semantic formalization for reflections involving epistemic and temporal aspects. In this article in Section 2 the basic notions of epistemic logic are presented. In Section 3 we do the same for temporal logic and the notion of temporalization of a logical system. In Section 4 we show how upward reflection can be formalized based on epistemic states. In Section 5 we introduce the logic used to formalize the meta-level reasoning: S5P*. In Section 6 we define a labeled branching time temporal formalization of downward reflection. In Section 7 we show how the overall formalization can be obtained from its parts and how it works for the running example reasoning pattern. In Section 8 we draw some conclusions. 2.

BASIC NOTIONS AND PROPERTIES OF EPISTEMIC LOGIC 2.1.

Epistemic Logic

DEFINITION 1 (Epistemic Formulas). Let P be a set of propositional constants (atoms); P ⫽ {pk兩k 僆 I}, where I is either a finite or countably infinite set. The set FORM of epistemic formulas ␸, ␺, . . . is the smallest set containing P, closed under the classical propositional connectives and the epistemic operator K, where K␸ means that ␸ is known. An objective formula is a formula without any occurrences of the modal operator K. For ⌫ 債 FORM, we denote by Prop(⌫) the set of objective formulas in ⌫. DEFINITION 2 (S5-Kripke Models). An S5 model is a structure ⺝ ⫽ 具M, ␲典, where M is a nonempty set and ␲ is a truth assignment function of type M 3 (P 3 {t, f}) such that for all m1, m2 僆 M: ␲(m1) ⫽ ␲(m2) f m1 ⫽ m2. The class of S5 models is denoted by Mod(S5). The set of states in an S5 model represents a collection of alternative states that are considered (equally) possible on the basis of (lack of) knowledge. We shall use S5 models as a representations of the knowledge of agents. Remark. For any m 僆 M, the function ␲ (m): p 3 ␲ (m)( p) is a valuation. Since we have that in an S5 model it holds that

␲ 共m 1兲 ⫽ ␲ 共m 2兲 N m 1 ⫽ m 2

TEMPORAL EPISTEMIC REFLECTION

1297

we may identify states m with their valuations ␲ (m) and write m ⬅ ␲ (m) for m 僆 M. So, without loss of generality, we may consider S5 models of the form ⺝ ⫽ 具M, ␲ 典 with M 債 ⺧, the set of all valuations. DEFINITION 3 (Submodels and Union of S5 Models). We define a subset relation on S5 models by ⺝1 債 ⺝2 iff M1 債 M2. Moreover, if ⺝1 ⫽ 具M1, ␲1典 and ⺝2 ⫽ 具M2, ␲2典 are two S5 models, their union is defined as ⺝1 艛 ⺝2 ⫽ 具M, ␲典, where M ⫽ M1 艛 M2 and ␲(m) ⫽ ␲i(m) if m 僆 Mi, i ⫽ 1, 2. DEFINITION 4 (Interpretation of Epistemic Formulas). Given ⺝ ⫽ 具M, ␲典, we 兩 ␸ by induction on the structure of the epistemic define the relation (⺝, m) ⫽ formula ␸:

共⺝, m兲 兩⫽ p N ␲共m兲共p兲 ⫽ t 兩 ␸ 共⺝, m兲 兩⫽ ␸∧␺ N 共M, m兲 ⫽

for and

p僆P 兩 ␺ 共M, m兲 ⫽

兩 ␸ 共⺝, m兲 兩⫽ ¬␸ N 共M, m兲 ⫽ 兩 ␸ 共⺝, m兲 兩⫽ K␸ N ᭙ m⬘ 僆 M 共M, m⬘兲 ⫽

DEFINITION 5 (Validity).

␸ is valid in ⺝ ⫽ 具M, ␲ 典, denoted ⺝ 兩⫽ ␸, if @m 僆 M: (⺝, m) 兩⫽ ␸. 兩 ␸ for all S5 models ⺝. (ii) ␸ is valid, notation Mod(S5) 兩⫽ ␸, if ⺝ ⫽ (i)

Validity w.r.t. S5 models can be axiomatized by the system S5. DEFINITION 6 (System S5).

The logic S5 consists of the following:

Axioms: (A1) All propositional tautologies (A2) (K ␸ ∧ K( ␸ 3 ␺ )) 3 K ␺ , knowledge is closed under logical consequence known facts are true (A3) K ␸ 3 ␸ , an agent knows that he knows something (A4) K ␸ 3 KK ␸ , an agent knows that he does not know some(A5) ¬K ␸ 3 K¬K ␸ , thing Derivation rules: (R1) ⵫ ␸ , ⵫ ␸ 3 ␺ f ⵫ ␺ , modus ponens necessitation (R2) ⵫ ␸ f ⵫ K ␸ , That ␸ is a theorem derived by the system S5 is denoted by S5 ⵫ ␸. THEOREM 1 (Soundness and Completeness of S5).

兩 ␸ S5 ⵫ ␸ N Mod(S5) ⫽

HOEK, MEYER, AND TREUR

1298

2.2.

Epistemic States and Stable Sets

In this work, we simply define an epistemic state as an S5 model. DEFINITION 7. An epistemic state is an S5 model ⺝ ⫽ 具M, ␲典. The set M is the set of epistemic alternatives allowed by the epistemic state M. DEFINITION 8. Let ⺝ be an S5 model. Then K(⺝) is the set of facts known in ⺝: 兩 K␸}. We call K(⺝) the theory of ⺝ or knowledge in ⺝. K(⺝) ⫽ {␸ 兩 M ⫽ Here, we mention that the knowledge in ⺝ exactly consists of the validities in M, 兩 ␸}. i.e., we have K(⺝) ⫽ { ␸ 兩 M 兩⫽ K␸} ⫽ {␸ 兩 M ⫽ LEMMA 1. For any S5 models ⺝1 and ⺝2: (i) If ⺝ 1 債 ⺝ 2 then Prop(K(⺝ 2 )) 債 Prop(K(⺝ 1 )) (ii) If the set of atoms P is finite, then also Prop(K(⺝ 2 )) 債 Prop(K(⺝ 1 )) f ⺝1 債 ⺝2 PROPOSITION 1 (Moore16). (i) The theory ⌺ ⫽ K(⺝) of an epistemic state M is a so-called stable set, i.e., it satisfies the following properties: (St 1) All instances of propositional tautologies are elements of ⌺ (St 2) If ␸ 僆 ⌺ and ␸ 3 ␺ 僆 ⌺, then ␺ 僆 ⌺ (St 3) ␸ 僆 ⌺ N K ␸ 僆 ⌺ (St 4) ␸ ⰻ ⌺ N ¬K ␸ 僆 ⌺ (St 5) ⌺ is propositionally consistent (ii) Every stable set ⌺ of epistemic formulas determines an S5-Kripke model ⺝ ⌺ for which it holds that ⌺ ⫽ K(⺝ ⌺ ); moreover, if P is a finite set, then ⺝ ⌺ is the unique S5-Kripke model with this property. PROPOSITION 2. A stable set is uniquely determined by its objective formulas. 3.

BASIC NOTIONS AND PROPERTIES OF TEMPORAL LOGIC

We start (following Ref.9) by defining the temporalized models associated with any class of models and apply it to the classes of models as previously discussed. In contrast to the reference as mentioned we use labeled flows of time. We use one fixed set L of labels, viz., L ⫽ 2 I , the power set of some index set I. However, in most definitions, we do not use this fact but only refer to (elements ␶ of) L. 3.1.

Flows of Time

DEFINITION 9 (Discrete Labeled Flow of Time). Suppose L is a set of labels. A (discrete) labeled flow of time (or lft), labeled by L is a pair ⺤ ⫽ (T, (⬍␶)␶僆L)

TEMPORAL EPISTEMIC REFLECTION

1299

consisting of a nonempty set T of time points and a collection of binary relations ⬍␶ on T. Here, for s, t in T, and ␶ in L the expression s ⬍␶ t denotes that t is a (immediate) successor of s with respect to an arc labeled by ␶. Sometimes it is convenient to leave the indices out of consideration and use just the binary relation s ⬍ t denoting that s ⬍␶ t for some ␶ (for some label ␶ they are connected). Thus, we have that ⬍ ⫽ 艛␶ ⬍␶. We also use the (nonreflexive) transitive closure « of this binary relation: « ⫽ ⬍⫹. We will make additional assumptions on the flow of time, for instance, that it describes a discrete tree structure, with one root and where time branches in the direction of the future. DEFINITION 10 (Labeled Time Tree). An lft ⺤ ⫽ (T, (⬍␶)␶僆L) is called a labeled time tree (ltt) if the following conditions are satisfied (recall that ⬍ ⫽ 艛␶ ⬍␶): (i) The graph 具T, ⬍典 is a directed rooted tree (ii) Successor existence: time points have at least one ⬍-successor (iii) Label-deterministic: for every label ␶ there is at most one ␶ successor DEFINITION 11 (Branch and Path). (a) A branch in an lft ⺤ is an lft ⺒ ⫽ (T⬘, (⬍⬘␶ ) ␶ 僆L ) with (i) T⬘ 債 T (ii) s ⬍⬘␶ t f s ⬍ ␶ t (iii) Every s 僆 T⬘ has at most one ⬍⬘-successor t 僆 T⬘ (iv) @s, t 僆 T⬘: s ⬍ ␶ t f s ⬍⬘␶ t (v) Every element of T that is in between elements of T⬘ is itself in T⬘: @s⬘ 僆 T⬘, t 僆 T, and u⬘ 僆 T⬘ : s⬘ « t « u⬘ f t 僆 T⬘ (b) A branch in an ltt ⺤ ⫽ (T, (⬍ ␶ ) ␶ 僆L ) is maximal if it contains the root r of T (c) A path is a finite sequence of successors s 0 , . . . , s n such that s i ⬍ s i⫹1 for all 0 聿 i 聿 n ⫺ 1; we call s 0 the starting point and s n the end point of the path PROPOSITION 3. Any branch of an lft ⺤ is an ltt. DEFINITION 12 (Standard ltt, Embedding, Isomorphism). (a) The standard ltt ⺣ over L is the set of all finite sequences over L equipped with the successor relations: 共 ␶ 0, ␶ 1, . . . , ␶ k兲 ⬍␶ 共␶0 , ␶1 , . . . , ␶k , ␶兲 (b) Let ⺤ ⫽ (T, (⬍ ␶ ) ␶ 僆L ) and ⺤⬘⫽(T⬘, (⬍⬘␶ ) ␶ 僆L ) be two ltt’s. A mapping f: ⺤ 3 ⺤⬘ is an embedding if it is injective and two-sided successor-

1300

HOEK, MEYER, AND TREUR

preserving: s ⬍ ␶ t iff f(s) ⬍⬘␶ f(t). An embedding is an isomorphism if it is surjective. PROPOSITION 4. Every ltt is uniquely embeddable in ⺣. Moreover, every successor complete ltt is isomorphic to ⺣. This proposition shows that every element t in an ltt is uniquely described by the sequence of labels of a (unique) path from the root to t. PROPOSITION 5. In an ltt for every time point t, the intersection of all maximal branches containing t is the set {s 兩 s « t} 艛 {t}. DEFINITION 13 (Time Stamps). Given an ltt (T, (⬍␶)␶僆L). A mapping 兩䡠兩 : T 3 ⺞ is called a time stamp mapping if for the root r it holds that 兩r兩 ⫽ 0 and for all time points s, t it holds that s ⬍ t f 兩t兩 ⫽ 兩s兩 ⫹ 1. Note that an ltt is infinitely deep, i.e., for every k 僆 ⺞ there is a time point t 僆 T with 兩t兩 ⫽ k. This is a direct consequence of the following proposition. PROPOSITION 6. If ⺒ is a maximal branch in an ltt, then any time stamp mapping is an isomorphism between ⺒ and ⺞. 3.2.

Temporal Models

First, we define our temporal formulas. DEFINITION 14 (Temporal Formulas). Given a logic L, temporal formulas over (the language of) L are defined as follows: (i) If ␸ is a formula of L, then C ␸ is a temporal formula (also called a temporal atom) (ii) If ␸ and ␺ are temporal formulas, then so are ¬ ␸ , ␸ ∧ ␺ , ␸ 3 ␺ , X ?, ␶ ␸ , X ? ␸ , X @, ␶ ␸ , X @ ␸ , F ? ␸ , F @ ␸ , G ? ␸ , G @ ␸ . Note how the C operator acts as a kind of “separator” between the basic language for L and the actual temporal formulas; from the temporal language point of view, formulas of the form C ␸ may be conceived as a kind of “atoms”; in the truth definition, occurrences of the C enforce a “shift” in the evaluation of formulas, taking us from a temporal model ⺝ to some of it snapshots ⺝ t , which are in their turn models for L. DEFINITION 5 (Temporal Models). (a) Let MOD be a class of models, and ⺤ ⫽ (T, (⬍ ␶ ) ␶ 僆L ) be a labeled flow of time. A temporal MOD model over ⺤ is a mapping ⺝: T 3 MOD. For t 僆 T we sometimes denote ⺝(t) (the snapshot at time point t) by ⺝ t . (b) If we apply (a) to the classes of models ModSet(PC) ⫽ ⺧ or Mod(S5) we call these temporalized models temporal valuation-set models (abbre-

TEMPORAL EPISTEMIC REFLECTION

1301

viated temporal V models) and temporal S5 models over ⺤, respectively. Similar to the class of S5P* models that will be introduced in Section 5. (c) Given an lft ⺤, the temporal formulas are interpreted on MOD models as follows: (i) Conjunction and implication are defined as usual; moreover, ⺝, s 兩⫽ ¬␸ iff not ⺝, s 兩⫽ ␸; (ii) The temporal operators are interpreted as follows: (1) C ␸ means that in the current state ␸ is true, i.e., 兩 ␸ M, s 兩⫽ C␸ iff ⺝s ⫽ (2) X ?, ␶ ␸ means that ␸ is true in some ␶ -successor state, i.e., ⺝, s 兩⫽ X ?, ␶ ␸ iff there exists a time point t with s ⬍ ␶ t such that ⺝, t 兩⫽ ␸ (3) X ? ␸ means that there is a ␶ with some ␶ successor in which ␸ is true, i.e., ⺝, s 兩⫽ X ? ␸ iff there exists a time point t with s ⬍ t such that ⺝, t 兩⫽ ␸ (4) X@,␶␸, meaning that ␸ is true in all ␶ successor states, i.e., 兩 X @, ␶ ␸ iff for all time points t with s ⬍ ␶ t it holds ⺝, ⺝, s ⫽ t 兩⫽ ␸ (5) X @ ␸ means that ␸ is true in all immediate successors: ⺝, s 兩⫽ X @ ␸ iff for all time points t with s ⬍ t it holds ⺝, t 兩⫽ ␸ (6) F ? ␸ means that ␸ is true in some future state, i.e., ⺝, s 兩⫽ F ? ␸ iff there exists a time point t with s « t such that ⺝, t 兩⫽ ␸ (7) F @ ␸ , means that for all future paths there is a time point where ␸ is true: ⺝, s 兩⫽ F @ ␸ iff for all branches ⺒ starting in s there is a t in ⺒ with ⺝, t 兩⫽ ␸ (8) G ? ␸ means that ␸ is true along some future path, i.e., ⺝, s 兩⫽ G ? ␸ iff there exists a branch ⺒ starting in s, with ⺝, t 兩⫽ ␸ for all t in ⺒. (9) G @ ␸ , means that ␸ is true all future states i.e., M, s 兩⫽ G @ ␸ iff for all time points t with s « t it holds ⺝, t 兩⫽ ␸. 4.

FORMALIZING UPWARD REFLECTION USING EPISTEMIC STATES

To let the meta-level manipulate the information that is (explicitly or implicitly) encoded at the object level, somehow it has to be reflected upward what is known at the object level and what is not. The former, i.e., to reflect upward what is known, is straightforward: if an objective formula ␸ is true at the object-level, we simply reflect this as K ␸ being true. More interestingly, we also want to reflect upward those facts that are (currently) not known at the object level. Moreover, we somehow want to implement the idea that the facts that are true at the object level are all that are known at the current time point.

1302

HOEK, MEYER, AND TREUR

The converse relation of 債 on Kripke models (cf. Definition 3), will play an important role in the sequel. The expression ⺝ 1 傶 ⺝ 2 means that the model ⺝ 2 , viewed as a representation of the knowledge of an agent, involves a refinement of the knowledge associated with model ⺝ 1 . This has to be understood as follows: in the model ⺝ 2 less (or the same) states are considered possible by the agent as compared by the model ⺝ 1 . So, in the former case the agent has less doubts about the true nature of the world. It will turn out that our definitions will work in such a way that this means that with respect to model ⺝ 2 , the agent has at least the knowledge associated with model ⺝ 1 and possibly more. So, in a transition of ⺝ 1 to ⺝ 2 we may say that knowledge is gained by the agent. Thus, the relation “傶” acts as an knowledge ordering on the set of S5 models. We already noted in Section 2 that the set of states in an S5 model represents the states that are considered possible on the basis of (lack of) knowledge. We also mentioned that the validities of such a model exactly determine what was called an epistemic state. On the basis of such epistemic states, Halpern and Moses11 define 兩 with which one can infer what is known and, more an entailment relation ⬃ importantly, what is unknown in such epistemic states. DEFINITION 16. Given a set M 債 ⺧, we define the associated S5 model ⌽(M), m(p). given by ⌽(M) ⫽ 具M, ␲典, with ␲: M ⫻ P 3 {t, f} such that ␲: (m, p) DEFINITION 17. Given some objective formula ␸, we define M␸ as the set of 兩 ␸}. We denote the epistemic valuations satisfying ␸, i.e., M␸ ⫽ {m 僆 W 兩 m ⫽ state associated with M␸ by ⌽(M␸) or ⺝␸. 兩 ␸} ⫽ 艛{⺝兩⺝ ⫽ 兩 K␸}. PROPOSITION 7. ⺝␸ ⫽ 艛{⺝兩⺝ ⫽

Proof. The latter equality follows from the fact that we are in the realm of S5 models. The former equality is proved as follows: ⺝ ␸ ⫽ ⌽(M ␸ ) ⫽ 具M ␸ , ␲ M ␸, R M ␸典 with M ␸ ⫽ {m 僆 W 兩 m 兩⫽ ␸}. On the other hand, ⺝ ⫽ 具M, ␲ M , R M 典 兩⫽ ␸ N (since ␸ is objective—adopting the view that M 債 ⺧) M 兩⫽ ␸ N M 債 M␸. So, 艛{⺝兩⺝ 兩⫽ ␸} ⫽ 艛{具M, ␲M, RM典兩M 債 M␸} ⫽ {M␸, ␲M␸, RM␸典, because 艛{M兩M 債 M ␸ } ⫽ M ␸ . Thus, ⺝ ␸ ⫽ 艛{⺝兩⺝ 兩⫽ ␸}. ■ Thus, to get M ␸ , we can consider all S5 models of ␸ and take their union to obtain M ␸ by ␮ : ␮ ( ␸ ) ⫽ M ␸ . one “big”-S5 model. We denote the mapping ␸ DEFINITION 18 (Nonmonotonic Epistemic Entailment). For ␸ 僆 Prop(FORM), 兩 ␺ N ␺ 僆 K(⺝␸). and ␺ 僆 FORM: ␸ ⬃ Informally, this means that ␺ is entailed by ␸, if ␺ is contained in the theory (knowledge) of the “largest S5 model” ⺝ ␸ of ␸. Halpern and Moses showed in Ref. 11 that this “largest model” need not always be a model of ␸ itself if we allow ␸ to contain epistemic operators. However, in our case, where we only use objective formulas ␸ , ⺝ ␸ is always the largest model for ␸. Moreover, Halpern and Moses have shown that in this case the theory K(⺝ ␸ ) of this largest model is

TEMPORAL EPISTEMIC REFLECTION

1303

a stable set that contains ␸ and such that for all stable sets ⌺ containing ␸ it holds that Prop(K(⺝ ␸ )) 債 Prop(⌺); thus, K(⺝ ␸ ) is the “propositionally least” stable set 兩 also can be viewed as a preferential entailment relation that contains ␸. So, ⬃ in the sense of Shoham Ref. 17, where, in our study, the preferred models of ␸ are the largest ones, viz., ⺝ ␸ , where the least objective knowledge is available. We denote the mapping ␸ K(⺝ ␸ ) by ␬ : ␬ ( ␸ ) ⫽ K(⺝ ␸ ), the stable set 兩 closure of associated with knowing only ␸. Alternatively viewed, ␬(␸) is the ⬃ ␸. Note that because ␬ ( ␸ ) ⫽ K(⺝ ␸ ) is a stable set, it is also propositionally closed. We now give a few examples to show how the entailment 兩⬃ works: Let p and q be two distinct primitive propositions. Then,

p 兩⬃ K共p∨q兲

兩 ¬Kq p⬃

p 兩⬃ Kp ∧ ¬Kq

兩 ¬K¬q p⬃

p ∧ q 兩⬃ K共p ∧ q兲 ∧ Kp ∧ Kq

兩 ¬K共p ∧ q兲 p⬃

p∨q 兩⬃ K共p∨q兲

兩 ¬Kp ∧ ¬Kq p∨q ⬃

Obviously, the entailment relation 兩⬃ is nonmonotonic; for instance, we have p 兩⬃ ¬Kq, while not p ∧ q 兩⬃ ¬Kq; it even holds that p ∧ q 兩⬃ Kq. 兩 enables us to derive from an The nonmonotonic epistemic entailment ⬃ objective formula ␸, which characterizes the exact epistemic state of the agent (viz., technically the epistemic state ⺝ ␸ ) exactly what is known and, even more importantly, what is unknown in this epistemic state. This latter property renders the entailment relation context sensitive and nonmonotonic, so that the 兩 goes beyond an entailment expressible in ordinary epistemic logic; relation ⬃ 兩 involves a kind of epistemic closure. with respect to its premise, the relation ⬃ 5.

THE META-LEVEL: EPISTEMIC PREFERENCE LOGIC S5P*

兩 enables us to derive inforThe “upward reflection” entailment relation ⬃ mation about what is known and what is not known. In this section, we show how we can use this information to perform meta-level reasoning. To this end, we extend our language with operators that indicate that something is a possible assumption to be introduced at the object level and thus has a different epistemic status than a certain fact. In this way the proverbial “make an assumption” is not made directly in the logic, but a somewhat more cautious approach is taken. The “assuming” itself is part of the downward reflection, to be discussed in Section 6. Let I be a finite set of indexes. The logic S5P (introduced in Ref. 18 and developed further in Refs. 19, 20, and 21) is an extension of the epistemic logic S5 by means of special modal operators P i denoting possible assumption (w.r.t. situation or frame of mind i), for i 僆 I, and also generalizations P ␶ , for ␶ 債 I. Informally, P i ␸ is read as “␸ is a possible assumption (within frame of reference i).” As we shall see, a frame of reference (or mind) refers to a preferred subset of the whole set S of epistemic alternatives. This operator is very close to the PA

HOEK, MEYER, AND TREUR

1304

operator of Ref. 12 and 13 and the D operator of Ref. 22. The generalization P ␶ ␸ is then read as a possible assumption w.r.t. the (intersection of the) frames of reference occurring in ␶. Also, we have an operator K to denote what is known and an operator B to describe what is true (believed) under the hypothesis (under focus). The logic S5P* is an extension of S5P by allowing an arbitrary set A of additional symbols that denote primitive meta-level propositions; for the moment, one may think of them as a way to express that certain propositions have been observed or that a given hypothesis is “in focus.” From a logical point of view, such assertions are just atoms, in which their truth is governed by some “meta-truth assignment function.” It may well be, that on closer examination, there are some logical laws steering the truth of such atoms, but in this stage we will not investigate the inner structure of the given meta-level propositions. Formally, S5P* formulas are interpreted on Kripke structures (called S5P* models) of the form ⺝ ⫽ 具U, M, ␲ , 兵M i 兩 i 僆 I其, MV典 where: U is a collection of states (universe) and M 債 U is nonempty (the current focus), ␲ : U ⫻ P 3 {t, f} is a truth assignment to the primitive propositions per world, M i 債 M (i 僆 I) are sets (“frames”) of preferred worlds, and MV: A 3 {t, f} is a valuation for the additional primitive meta-level propositions. When writing ⺝ 1 債 ⺝ 2 , we mean that the set of states of ⺝ 1 is a subset of those of M 2 . Again, we identify states s and their truth assignments ␲ (s). We let Mod(S5P*) denote the collection of Kripke structures of the aforementioned form. Given an S5P* model ⺝ ⫽ 具U, M, ␲ , {M i 兩 i 僆 I}, MV典, we call the S5 model ⺝ M ⫽ 具M, ␲ 兩M典 the focused S5 reduct of ⺝ and ⺝ U ⫽ 具U, ␲ 兩U典 the universal or general S5-reduct of ⺝. DEFINITION 19 (Interpretation of S5P* Formulas). Given a model ⺝ ⫽ 具U, M, ␲, {Mi 兩 i 僆 I}, MV典, we give the following truth definition: let ␸ be a formula, ␣ 僆 A, and m 僆 U. The cases in which ␸ 僆 P, ␸ ⫽ (␸1 ∧ ␸2), or ␸ ⫽ ¬␺ are dealt with as in Definition 4; the other cases are as follows: (⺝, (⺝, (⺝, (⺝, 債I (⺝,

兩 ␸ m) 兩⫽ K␸ iff @m⬘ 僆 U, (⺝, m⬘) ⫽ 兩 ␸ m) 兩⫽ B␸ iff @m⬘ 僆 M, (⺝, m⬘) ⫽ 兩 ␸ m) 兩⫽ Pi␸ iff @m⬘ 僆 Mi, (⺝, m⬘) ⫽ 兩 ␸, where M␶ ⫽ 艚i僆␶Mi and ␶ m) 兩⫽ P␶␸ iff @m⬘ 僆 M␶, (⺝, m⬘) ⫽

m) 兩⫽ ␣ iff MV(␣) ⫽ t, for ␣ in A

We see that the clauses state that P i ␸ is true if ␸ is a possible assumption w.r.t. subframe M i , whereas the latter says that P ␶ ␸ is true if ␸ is a possible assumption w.r.t. the intersection of the subframes M i , i 僆 ␶ . This intersection is denoted by M ␶ . We assume that for ␶ ⫽ A, M A ⫽ 艚 i僆A M i ⫽ M. So, in this special case we get that the P ␶ modality coincides with the belief operator B. Validity and satisfiability are defined analogously as before.

TEMPORAL EPISTEMIC REFLECTION

1305

It is possible to axiomatize (the theory of) S5P* by adjusting the axiom system S5P of Ref. 21; we will not go into full details here but give some main principles. DEFINITION 20 (System S5P*). In the following, i ranges over I and ␶ ranges over subsets of I. Moreover, 䊐, 䊐1, and 䊐2 are variables over {K, B, Pi, P␶兩i 僆 I, ␶ 債 I}. (B1) All propositional tautologies (B2) (䊐 ␸ ∧ 䊐( ␸ 3 ␺ )) 3 䊐 ␺ (B3) 䊐 ␸ 3 䊐䊐 ␸ (B4) ¬䊐 ␸ 3 䊐¬䊐 ␸ (B5) K ␸ 3 ␸ (B6) K ␸ 3 䊐 ␸ (B7) ¬䊐 1 ⬜ 3 (䊐 1 䊐 2 ␸ 7 䊐 2 ␸ ) (B8) P i ␸ 7 P {i} ␸ (B9) P ␶ ␸ 3 P ␶ ␸ , ␶ 債 ␶ ⬘ (B10) P A ␸ 7 B ␸ (B11) ¬B⬜ (R1) Modus ponens (R2) Necessitation for K: ⵫ ␸ f ⵫ K ␸ Axiom B1 says that we are dealing with an extension of propositional logic; B2 says that all the operators K, B, P i , and P ␶ are “normal”; B3 and B4 express that the relations R, R i , and R ␶ (which can be conceived as U ⫻ U, U ⫻ M i and U ⫻ M ␶ , respectively, and for which the operators K, P i , P ␶ , and B can be interpreted as their respective necessity operators) are transitive and Euclidean, respectively; B5 says that R is reflexive and B6 says that all the relevant sets are subsets of the universe U; B7 helps us to get rid of nested modalities: a nested modality is always referring to the frame corresponding to the innermost one, provided that the outermost modality is not trivial (i.e., is not evaluated with respect to an empty set). Axiom B8 provides us with a bridge between the modalities with indices from I and those of P(I); it also shows that, in fact, we could do without the P i ’s. B9 says that if ␶ 債 ␶⬘, then M ␶ ⬘ 債 M ␶ . Finally, B10 is the syntactical counterpart of our definition that M A ⫽ M, and B11 mirrors the semantic requirement of M being nonempty. We call the resulting system S5P*. In the sequel we will write ⌫ ⵫S5P* ␸ or ␸ 僆 Th S5P*(⌫) to indicate that ␸ is an S5P* consequence of ⌫. We mean this in the more liberal sense: it is possible to derive ␸ from the assertions in ⌫ by means of the axioms and rules of the system S5P*, including the necessitation rule. (So, in effect we consider the assertions in ⌫ as additional axioms: ⌫ ⵫S5P* ␸ iff ⵫S5P*艛⌫␸; cf. Ref. [MH93b].) 兩 ⌫ f M ⫽ 兩 ␸). THEOREM 2. ⌫ ⵫S5P* ␸ N (@M 僆 Mod(S5P*)M ⫽

Proof. Combine the arguments given in Refs. 19 and 21.

HOEK, MEYER, AND TREUR

1306

6.

A TEMPORAL FORMALIZATION OF DOWNWARD REFLECTION

In the previous sections, it has been described how the upward reflection can be formalized by an (nonmonotonic) inference based on epistemic states, and the meta-level process by an (monotonic) epistemic logic. In this section, we will introduce a formalization of the downward reflection step in the reasoning pattern. The meta-level reasoning can be viewed as the part of the reasoning pattern where it is determined what the possibilities are for additional assumptions to be made, based on which information is available at the object level and which is not. The outcome at the meta-level concerns conclusions of the form P ␸ , where ␸ is an object level formula. What is missing still is the step in which the assumptions are actually made, i.e., where such formulas ␸ are added to the object level knowledge in order to be able to reason further with them at the object level. This is what should be achieved by the downward reflection step. Thus, the reasoning pattern as a whole consists of a process of generating possible assumptions and actually assuming them. By these downward reflections, at the object level a hypothetical world description is created (as a refinement or revision of the previous one). This means that in principle not all knowledge available at the object level can be derived already from the object level theory (OT): downward reflection creates an essential modification of the object level theory. Therefore, it is excluded to model downward reflection according to reflection rules as sometimes can be found in the literature, e.g., “If at the meta-level it is provable that provable(␸), then at the object level ␸ is provable” (cf. Ref. 5): MT ⵫ provable共␸兲 OT ⵫ ␸ A reflection rule like this can be used only in a correct manner if the meta-theory about provability gives a sincere axiomatization of the object level proof system, and in that case by downward reflection nothing can be added to the object level that was not already derivable from the object level theory. Because we essentially extend or modify the object level theory, such an approach can not serve our purposes here. In fact, a line of reasoning at the object level is modeled by inferences from subsequently chosen theories instead of inferences from one fixed theory. In principle, a downward reflection realizes a shift or transition from one theory to another. In Ref. 4 such a shift between theories is formalized by using an explicit parameter referring to the specific theory (called “context” in their terms) that is concerned and by specifying relations between theories. In their case, downward reflection rules (“bridge rules” in their terms) may have the form MT ⵫ provable共OT⬘, ␸兲 OT⬘ ⵫ ␸ or, in their notation,

TEMPORAL EPISTEMIC REFLECTION

1307

具Th共“ ␸ ”, “OT⬘”兲, MT典 具␸, OT⬘典 Here, the second element of the pair denotes the context in which the formula that is the first element holds. At the meta-level, knowledge is available to derive conclusions about provability relations concerning a variety of object level theories OT. So, if at the object level from a (current) theory OT some conclusions have been derived, and these conclusions have been transformed to the meta-level, then the meta-level may derive conclusions about provability from another object level theory OT⬘. Subsequently, one can continue the object level reasoning from this new object level theory OT⬘. The shift from OT to OT⬘ is introduced by use of the foregoing reflection rule. In the approach as adopted here, we give a temporal interpretation to these shifts between theories. This can be accomplished by formalizing downward reflection by temporal logic (as in Ref. 6). In a simplified case, where no branching is taken into account, the temporal axiom (CP ␸ 3 X ␸ ) i.e., if currently phi is a possible assumption, then next phi holds, can be used to formalize downward reflection for every objective formula ␸. In the general case, we want to take into account branching and the role to be played by an index ␶ in P ␶ ␸ . We will use this index ␶ to label branches in the set of time points. By combining S5P* with the temporal logic obtained in this manner we obtain a formalization of the whole reasoning pattern. During the reasoning process, we modify the information we have at the object level and, accordingly, change the focus set M of possible worlds. We can formulate this property as follows: DEFINITION 21. A temporal S5P* model obeys downward reflection if the following holds for any s and ␶: the cluster M␶ in ⺝s is nonempty N there is a t with s ⬍␶ t and for all such t the focus set of states M of ⺝t equals M␶. Now, we are ready to zoom in into the models we want to consider here, the TEMA models. DEFINITION 22 (TEMA Models). A TEMA model ⺝ is a temporal S5P* model over an lft ⺤ such that: (i) (ii) (iii) (iv)

⺤ is a labeled time tree For every time point s, there is exactly one t with s ⬍ A t ⺝ obeys downward reflection ⺝ is conservative; if s ⬍ t then (⺝ s ) U 傶 (⺝ t ) U

Notice that conservatism refers to the universe U. Sometimes M is shrinking during the reasoning process: in case of an accumulation of assumptions that are never retracted (e.g., see Ref. 23), but, in general, M may vary arbitrarily within U.

HOEK, MEYER, AND TREUR

1308

THEOREM 3. TEMA models have the following validities: (T0) All the operators of {X @, ␶ , X @ , F @ , G @ } satisfy the K axiom (C too) and generalization 兩 (introduction of C) (T1) ⵫S5P* ␸ f ⫽ TEMA C␸ (T2) ¬X @ ⬜ (successor existence) (T3) X ?, ␶ ␸ 7 X @, ␶ ␸ (label deterministic) (T4) X @, ␶ ␸ 7 ¬X ?, ␶ ¬ ␸ (duality) (T5) X @ ␸ 7 ¬X ? ¬ ␸ (duality) (T6) X @ ␸ 7 ⵩ ␶ 債I X @, ␶ ␸ (⬍ is union of ⬍␶) (T7) X ? ␸ 7 ⵪ ␶ 債I X ?, ␶ ␸ (dual of T6) (T8) C(¬P ␶ ⬜ ∧ P ␶ ␸ ) 7 X ?, ␶ CK ␸ , if ␸ is objective (allowing downward reflection) (T9) G @ ␸ 3 X @ ␸ (⬍ 債 «) (T10) G @ ␸ 3 X @ G @ ␸ (since « is transitive closure of ⬍) (T11) G @ ( ␸ 3 X @ ␸ ) 3 (X @ ␸ 3 G @ ␸ ) (induction) (T12) (C ␸ 3 X @ C ␸ ) ∧ (CK ␸ 3 X @ CK ␸ ), if ␸ is objective (conservativity) (T13) CK ␸ 3 G @ CK ␸ (from conservativity and induction) Remark. The foregoing theorem says that the formulas T1–T13 are at least sound; however, we have not been concerned by designing a complete logic for TEMA models.

7.

OVERALL FORMALIZATION

In this section we will show how the different parts of the reasoning pattern as described in previous sections can be combined.

7.1.

Epistemic Meta-Level Architecture Theories and Entailment

In the language of S5P*, we can express meta-knowledge. By combining the formal apparatus of S5P* with Halpern and Moses’ nonmonotonic epistemic entailment, we obtain a framework in which we can perform static epistemic reasoning: reasoning about the current epistemic state without reflecting the conclusions downward. We call this framework epistemic meta-level architecture (EMA). DEFINITION 23 (EMA Theory). An EMA theory ⌰ is a pair (W, ⌬), where W is a finite, consistent set of objective (i.e., nonmodal) formulas describing facts about the world, and ⌬ is a finite set of S5P* formulas. The sets W and ⌬ are to be considered as sets of axioms; we may apply necessitation to them.

TEMPORAL EPISTEMIC REFLECTION

1309

In principle, it would be possible to use the index i of the P operator in a completely arbitrary way, to be chosen by the knowledge engineer. However, to be able to treat the various conclusions that can be drawn at the meta-level separately from each other in the sequel, we shall assume all occurrences of P operators in a meta-theory to have distinct index. This will allow for a generic way to look at the possibilities of combining possible assumptions by using the P ␶ operators. So, e.g., rather than looking at a meta-theory with ⌬ ⫽ 兵p ∧ Mq 3 P 1q, r ∧ Ms 3 P 1s其 in which for both rules the same operator P 1 is used, we consider the set ⌬⬘ ⫽ 兵p ∧ Mq 3 P 1q, r ∧ Ms 3 P 2s其 in which both rules are represented by means of different operators P 1 and P 2 , and we consider the combined operator P {1,2} . DEFINITION 24 (EMA Entailment). Given an EMA theory ⌰ ⫽ (W, ⌬), we define 兩 ⌰ as follows. Let W* be the conjunction the nonmonotonic inference relation ⬃ of the formulas in W, and let ␸ be an objective formula. Then, we define the 兩 ⌰ w.r.t. ⌰ as follows: EMA entailment relation ⬃

␸ 兩⬃⌰␺Ndef␬共␸∧W*兲 艛 ⌬⵫S5P*␺. This definition states that ␺ is an EMA consequence of ␸ iff ␺ follows in the S5P* logic from the meta-knowledge together with what is implied by knowing only the conjunction of ␸ with the background information W. Notice that because the logic S5P* is monotonic, the following equivalence holds. 兩 ⌰ ␺ N there exists an S5-formula ␺⬘ 僆 FORM such that PROPOSITION 8. ␸ ⬃

␸ ∧W* 兩⬃␺⬘and{␺⬘}艛⌬⵫S5P*␺. This gives a modularity of the entailment relations. 兩 ⌰ ␺, we simply write ⬃ 兩 ⌰ ␺. Note that for ⌰ ⫽ (W, ⌬), Instead of true ⬃ 兩 ⌰ ␺ iff ⬃ 兩 ⌰⬘ ␺, with ⌰⬘ ⫽ (W 艛 { ␸ }, ⌬). Furthermore, if ⌫ is we have ␸ ⬃ 兩 ⌰ ␺ a finite set of epistemic formulas and ␺ is an S5P* formula, we define ⌫ ⬃ 兩 ⌰ ␺, where ⌫* stands for the conjunction of the formulas in ⌫. as ⌫* ⬃ Example (Hypothesis Elimination). We come back to our example in the introduction. Let the EMA theory ⌰ ⫽ (W, ⌬) be defined by W ⫽ 兵e 3 ¬b其 ⌬ ⫽ 兵K¬s 3 共共¬Ke ∧ ¬K¬e兲 3 P 1e兲 initially_¬s, initially_z 3 Kz} where e means “empty battery” and b means “lights can burn.” Moreover, we have used primitive meta-level propositions “initially_z” to indicate that the

HOEK, MEYER, AND TREUR

1310

information “z” is present initially, i.e., before the reasoning process starts. Now, we have the following: W* 兩⬃ ¬Ke ∧ ¬K¬e

and

⌬ 艛 兵¬Ke ∧ ¬K¬e其 ⵫S5P*P1 e

Therefore, 兩⬃⌰ P1e Example (Default Reasoning). We also show how default reasoning is covered by our approach, by the well-known Tweety example. Consider the following EMA theory ⌰ ⫽ (W, ⌬) with W ⫽ 兵p 3 ¬f其 ⌬ ⫽ 兵b ∧ Mf 3 P 1f其 representing that penguins do not fly, and that by default birds fly. Now, consider the following inferences: (i) b ∧ W* 兩⬃ b ∧ ¬K¬f ⵫S5P*b ∧ Mf ⵫ S5P*P 1 f; i.e., b 兩⬃⌰ P1f, meaning that from the mere fact that Tweety is a bird, we conclude that Tweety is 兩 assumed to fly. (Here ⬃ stands for Halpern and Moses’ nonmonotonic epistemic entailment.) This must be contrasted to the next inference. (ii) b ∧ p ∧ W* 兩⬃ Kp ⵫S5P* K¬f ⵫ S5P* ¬Mf ⵫/ S5P* P 1 f; i.e., not b ∧ p 兩⬃⌰ P1f meaning that in case Tweety is a penguin, we can not infer that Tweety is assumed to fly, but instead, we can derive that we know for certain that Tweety does not fly: b ∧ p 兩⬃⌰ K¬f. As a remark, we like to mention that in Ref. 20 it was shown how counterfactual reasoning can be implemented by means of default reasoning. For this, an additional operator was needed to indicate what holds in the actual world. Although we will not pursue this issue any further here, we think our framework of temporalizing S5P* can be adapted easily to give an account of counterfactual reasoning too. 7.2.

TEMA Models and TEMA Entailment

DEFINITION 25. Let ⌰ ⫽ (W, ⌬) be an EMA theory. Then, we define a TEMA model of ⌰ as a TEMA model ⺝⌰ such that (i) (Basis: the root) ⺝ r⌰ is an S5P* model such that (a) The universal S5 reduct of ⺝ r⌰ is the S5 model ⺝ W* (b) ⺝ r⌰ satisfies the meta-knowledge, i.e., ⺝ r⌰ 兩⫽ ⌬ (ii) (Induction step) Suppose that we are given an S5P* model at snapshot ⺝ s⌰ . Then, we have that for a (n S5P*) model ⺝ ⌰ t with s ⬍ ␶ t, it holds that ⌰ (a) (⺝ ⌰ t ) U is the S5 model M ␶ as it appeared as a cluster in ⺝ s ⌰ ⌰ (b) ⺝ t satisfies the meta-knowledge again, i.e., ⺝ t 兩⫽ ⌬

TEMPORAL EPISTEMIC REFLECTION

1311

Generally, there are multiple TEMA models of an EMA theory ⌰. Note that clause ii(a) reflects the downward reflection operation with respect to the P ␶ assumptions. Even in less trivial reasoning processes, we may be interested in some kind of final outcome (a conclusion set). In our case the universe U always shrinks, but the focus set M does not always do so. We can view U as a core of derived facts that after all survives during the reasoning pattern; this is reflected in the following definition. DEFINITION 26 (Limit Model). Suppose ⺝ is a conservative temporal V model. The intersection of the models ⺝(s) for all s in a given branch ⺒ ⫽ (T, (⬍␶)␶僆L) of the lft ⺤ is called the limit model of the branch, denoted lim⺒ ⺝. The set of limit models for all branches is called the set of limit models of ⺝. These definitions straightforwardly extend to temporal S5 and S5P models, by identifying ⺝ with its set of states, U. We might formulate definitions of entailment of objective formulas related to any model or any model based on the standard tree. But it may well happen that there are branches in such models, for instance labeled by the empty set only, that contain no additional information as compared with the background knowledge. It is not always realistic to base entailment on such informationally poor branches in a model. Thus, we have the following definition. DEFINITION 27 (Informationally Maximal). We define for branches ⺒1 and ⺒2 with the same set of time stamps of a TEMA model ⺝ that ⺒2 is informationally larger than ⺒1, denoted ⺒1 聿 ⺒2, if for all i 僆 N and s, t with 兩s兩 ⫽ 兩t兩 ⫽ i it holds ⺒2(s) 債 ⺒1(t). We call ⺒1 informationally maximal if it is itself the only branch of ⺝ that is informationally larger. DEFINITION 28 (Regular Model). A TEMA model ⺝ is called regular if all branches are informationally maximal. The submodel based on all time points t included in at least one informationally maximal branch is called the regular core of ⺝, denoted by reg(⺝). Remark. Generally, the regular core will not be label-complete, because branches will be cut off. The idea behind taking informationally complete branches is that we want to maximize the effect of applying meta-knowledge in order to obtain as much (assumptional) knowledge as possible. DEFINITION 29. (i) For k 僆 ⺞, we define ⺝ (k) ⫽ 艛 t僆reg(⺝),兩t兩⫽k ⺝(t) (ii) ⺝ ␻ ⫽ 艚 k僆⺞ ⺝ (k) THEOREM 4 (From Ref. 23). Let ⺝ be a TEMA model. Then, (i) For k 聿 k⬘, we have ⺝ (k⬘) 債 ⺝ (k)

HOEK, MEYER, AND TREUR

1312

(ii) ⺝ ␻ ⫽ 艚 ⺒ branch of reg(⺝) lim⺒ ⺝. Because (regular) TEMA models describe a reasoning process over time, it seems natural to have notions of entailment that exploit the conservativity of such models, expressing the monotonic growth of knowledge of objective formulas. The latter restriction is important, because it may be the case that initially an atom p is not known, yielding ¬Kp and hence K¬Kp, while at some later point, p has been learned, giving ¬K¬Kp, expressing that some knowledge (i.e., knowledge about ignorance!) has been lost. Therefore, in the sequel we will be interested in formulas of the form CK␸, where ␸ is an objective formula. We will call such formulas currently known objective formulas (CKO’s) and use ␣ and ␤ as variables over them. In the literature on nonmonotonic reasoning, one usually distinguishes socalled sceptical (true in all obtained models) and credulous (true in some of them) notions of entailment. Because of the fact that we have a (infinite) branching time structure, we have a great variety of combining these notions, although for the formulas that we are interested in, the current objective formulas, various of such notions do collapse as is shown in the following theorem. THEOREM 5. Let ␣ and ␤ be CKO formulas. Then, on TEMA models, we have the following equivalences: (i) (ii) (iii) (iv)

G ?␣ ␣ ⬅ G @␣ F ?␣

⬅ ␣ ( ␣ ∧ G @␣ ) ⬅ X @␣ ⬅ F ? (G @ ␣ ∧ ␣ )

DEFINITION 30 (Sceptical Entailment). Let ⺝ be a TEMA model with root r and ␣ an CKO formula. We define the sceptical entailment relation by ⺝ 兩⬇scep ␣

iff

兩 F@␣ ⺝, r ⫽

Because of the remark that we made before Definition 25, it makes the most sense to use this notion of sceptical entailment for (sub) models of type reg(⺝). PROPOSITION 9. Let ⺝ be a TEMA model with root r and ␣ a CKO formula. The following are equivalent: 兩 scep ␣ (i) reg(⺝) ⬇ (ii) lim⺒ ⺝ 兩⫽ ␣ for every maximal branch ⺒ of the regular core of ⺝

For our definition of credulous entailment, we can be less restrictive; we do not need to bother about informationally maximal branches. Especially, too little information in one branch can always be overcome by another informationally larger branch.

TEMPORAL EPISTEMIC REFLECTION

1313

DEFINITION 31 (Credulous Entailment). Let ⺝ be a TEMA model and ␣ a CKO formula. We define 兩 F ?␣ ⺝ 兩⬇cred␣ iff ⺝, r ⫽

PROPOSITION 10. Let ⺝ be a TEMA model and ␣ a CKO formula. The following are equivalent: (i) ⺝ 兩⬇cred ␣ (ii) lim⺒ ⺝ 兩⫽ ␣ for some maximal branch B We finally can give the definitions of sceptical and credulous entailment. DEFINITION 32 (Entailment from an EMA Theory). Let ⌰ ⫽ (W, ⌬) be an EMA theory and ␸ an objective formula, ⌰ 兩⬇scep ␸

兩 scep ␸ iff for all models ⺝ of ⌰ it holds reg共⺝兲 ⬇

⌰ 兩⬇cred ␸

兩 cred ␸ iff for all models ⺝ of ⌰ it holds ⺝ ⬇

PROPOSITION 11. Let ⌰ ⫽ (W, ⌬) be an EMA theory and ␸ an objective formula. Then, it holds 兩 cred ␸ ⌰ 兩⬇scep ␸ f ⌰ ⬇

7.3.

The Example Reasoning Pattern

We return to our running example and show how it obtains its natural semantics. To cover the whole reasoning pattern, we take W ⫽ {(e ∧ p) 3 ¬s, e 3 ¬b} and ⌬ as ⌬ ⫽ {K¬s 3 ((¬Ke ∧ ¬K¬e) 3 P 1 e), if ¬s is known and we do not know whether ¬e holds, we may choose e as an hypothesis (K¬s ∧ K¬e) 3 ((¬Kp ∧ ¬K¬p) 3 P 2 p), we investigate p if we know ¬s and ¬e observed_b, initially_¬s, initially_z 3 Kz, possible_hyp_e, possible_hyp_p, (possible_hyp_z ∧ P i z) 3 X ?,i focus_z, z 僆 {e, p}, i 僆 {1, 2} (focus_z ∧ observed_w ∧ B¬w) 3 bad_hyp_z, z 僆 {e, p}, w 僆 {b} z 僆 {e, p}} (bad-hyp_z ∧ focus_z) 3 G @ K¬z We denote worlds by four-tuples (w, x, y, z) 僆 {0, 1} 4 , to be interpreted as the truth values of the tuple (b, e, p, s). We construct a model that is linear.

1314

HOEK, MEYER, AND TREUR

Figure 1. Initial snapshot for the example.

*Initial snapshot (0) (0) 典 We obtain the initial model ⺝ (0) ⫽ 具U (0) , M (0) , ␲ (0) , M (0) 1 , M 2 , MV (0) (0) (Figure 1). The universe U is based on all models of W; we take M ⫽ U (0) . Furthermore, we have seen how we can derive P 1 e from (W, ⌬), defining the (0) cluster M (0) 1 . In this model M 2 ⫽ A, (cf. our remarks at the end of this section); (0) MV is to be understood as the minimal valuation on the atoms of A so that ⌬ is satisfied;

*Next snapshot Using T8, C(¬P 1 ⬜ ∧ P 1 e) 7 X ?,1 CKe, we obtain a downward reflection (1) (1) 典, where MV (1) into the next model ⺝ (1) ⫽ 具U (1) , M (1) , ␲ (1) , M (1) 1 , M 2 , MV (0) (1) is like MV , but under MV , now also focus_e is true (Figure 2). Moreover, U (1) ⫽ U (0) , and the new cluster M (1) equals the old M (0) 1 . *Further snapshots (1)

Now, the cluster M is the one that is in the current focus: at its object level theory we can derive that ¬b, since in ⺝ (1) , we have ⺝ (1) 兩⫽ B¬b. We use the

Figure 2. Next snapshot for the example.

TEMPORAL EPISTEMIC REFLECTION

1315

meta-knowledge (focus_z ∧ observed_w ∧ B¬w) 3 bad_hyp_z with e for z and b for w. Using ⌬ again this yields G @ K¬e, so that for all ⺝ (2) with ⺝ (1) ⬍ ⺝ (2) it holds that ⺝ (2) 兩⫽ ¬e; semantically, this amounts to saying that the universe U (2) of all future models ⺝ (2) is at most the set U (1) ⶿M (1) , and one may proceed and investigate the hypothesis of bad plugs ( p) for the failure of the nonstarting car. Some remarks are in order here. First, we have analyzed only some intended model for the theory ⌰ ⫽ (W, ⌬); a model that carries the assumption that the theory (W, ⌬) is all that we know; this justified for example that we took M (1) 2 to be empty. Second, since the atoms in A are rather application dependent, we decided to add all assumptions about them to ⌬; however, for classes of applications, one might consider adding some of those properties as axioms to S5P*. Finally, in this particular example, we did not exploit the fact that we have a branching time model; one may change the example in such a way that the two possible hypotheses p and e are, so to speak, investigated simultaneously. In our example, there may be specific reasons to investigate one hypothesis before the other: because one of them (i.e., e) is easier to refute, e.g.; this preference is also explicitly modeled in ⌬. 8.

CONCLUSIONS

In Ref. 20,21 an EDL was introduced inspired by the notion of meta-level architecture that also was the basis for the BMS approach introduced in Ref. 12. In EDL, drawing a default conclusion has no other semantics than that of adding a modal formula to the meta-level. No downward reflection takes place to be able to reason with the default conclusions at the object level (by means of which assumptions actually can be made). In Ref. 12, downward reflection to actually make assumptions takes place, but no logical formalization was given; it was defined only in a procedural manner. In principle, a downward reflection that enlarges the object level theory disturbs the object level semantics: facts are added that are not logically entailed by the available object level knowledge. Adding a temporal dimension (in the spirit of Ref. 9) enables one to obtain formal semantics of downward reflection in a dynamic sense: as a transition from the current object level theory to the next one (where the reflected assumption has been added). This view, also underlying the work presented in Refs. 13 and 6, turns out to be very fruitful. A number of notions can be formalized in temporal semantics in a quite intuitive and transparent manner. The temporal epistemic meta-level architecture described here is a powerful tool to reason with dynamic assumptions: it enables one to introduce and retract additional assumptions during the reasoning, on the basis of explicit meta-knowledge. In Refs. 14 and 15 various applications of this architecture are shown. For an application of this architecture as a reasoning model to analyze and simulate (empirically given) human reasoning processes, see Refs. 24 and 25. In this study we formalized the semantics of a temporal epistemic meta-level architecture by means of entailment on the basis of temporalized Kripke models.

1316

HOEK, MEYER, AND TREUR

Acknowledgments Discussions about the subject with Joeri Engelfriet have played a stimulating role for the development of the material presented here.

References 1. 2. 3.

4.

5. 6.

7. 8.

9. 10.

11. 12. 13.

14. 15. 16. 17. 18.

Maes P, Nardi D (editors). Meta-level architectures and reflection. Berlin, Germany: Elsevier Science Publishers; 1988. Davis R. Metarules: Reasoning about control. Artif Intell 1980;15:179 –222. Bowen K, Kowalski R. Amalgamating language and meta-language in logic programming. In: Clark K, Tarnlund S, editors. Logic programming. New York: Academic Press; 1982. pp 153–172. Giunchiglia E, Traverso P, Giunchiglia F. Multi-context systems as a specification framework for complex reasoning systems. In: Treur J, Wetter T, editors. Formal specification of complex reasoning systems. New York: Ellis Horwood; 1993. pp 45–72. Weyhrauch RW. Prolegomena to a theory of mechanized formal reasoning. Artif Intell J 1980;13:133–170. Treur J. Temporal semantics of meta-level architectures for dynamic control of reasoning. In: Logic Program Synthesis and Transformation-Meta-Programming in Logic, Proc 4th Int Workshop on Meta-Programming in Logic, META’94. Springer Verlag, Lecture Notes in Computer Science, vol. 883; 1994. pp 353–376. Extended version: Treur J. Formal Semantics of Meta-Level Architectures: Dynamic Control of Reasoning. Int J Intell Syst 2002;17:545–568. Gabbay DM. Intuitionistic basis for non-monotonic logic. In: 6th Conf on Automated Deduction, LNCS 138. Springer Verlag; 1982. pp 260 –273. Engelfriet J, Treur J. A temporal model theory for default logic. In: Proc ECSQARU ’93. Springer Verlag; 1993. pp 91–96. Extended version: Engelfriet J, Treur J. An interpretation of default logic in minimal temporal epistemic logic. J Logic Lang Inf 1998;7:369 –388. Finger M, Gabbay D. Adding a temporal dimension to a logic system. J Logic Lang Computat 1992;1:203–233. Meyer JJC, van der Hoek W. An epistemic logic for defeasible reasoning using a meta-level architecture metaphor. Technical Report IR-329. Amsterdam: Free University; 1993. Halpern JY, Moses YO. Towards a theory of knowledge and ignorance. In: Proc Workshop on Non-Monotonic Reasoning; 1984. pp 125–143. Tan YH, Treur J. A bi-modular approach to non-monotonic reasoning. In: Proc WOCFAI’91. Paris; 1991. pp 461– 475. Allis VE, Tan YH, Treur J. Meta-level selection techniques for the control of default reasoning. Future Gen Comput Syst; 12(2–3). In: Lopez de Mantaras R, editor. Reflection and meta-level AI architectures. 1996. pp 189 –201. Treur J. Modelling nonclassical reasoning patterns by interacting reasoning modules. Report IR-236, Amsterdam: Free University; 1990. Treur J. Interaction types and chemistry of generic task models. In: Proc EKAW’91. Bonn: GMD Studien 211; 1992. pp 390 – 414. Moore RC. Semantical considerations on nonmonotonic logic. Artif Intell 1985;25:75–94. Shoham Y. Reasoning about change. Cambridge: MIT Press; 1988. Meyer JJC, van der Hoek W. Non-monotonic reasoning by monotonic means. In: van Eijck J, editor. Logics in AI (Proc JELIA ’90), LNCS 478. Springer; 1991. pp 399 – 411.

TEMPORAL EPISTEMIC REFLECTION 19.

20.

21. 22. 23. 24.

25.

1317

Meyer JJC, van der Hoek W. A modal logic for nonmonotonic reasoning. In: van der Hoek W, Meyer JJC, Tan YH, Witteveen C, editors. Non-monotonic reasoning and partial semantics. Chichester: Ellis Horwood; 1992. pp 37–77. Meyer JJC, van der Hoek W. A default logic based on epistemic states. In: Proc ECSQARU ’93. Springer Verlag; 1993. pp 265–273. Full version in Fundamenta Informaticae 1995;23(1):33– 65. Meyer JJC, van der Hoek W. Counterfactual reasoning by (means of) defaults. Ann Math Artif Intell 1993;9(III–IV):345–360. Doherty P. NM3—A three-valued cumulative non-monotonic formalism. In: van Eijck J, editor. Logics in AI. LNCS 478. Berlin: Springer; 1991. pp 196 –211. van der Hoek W, Meyer JJC, Treur J. Temporalizing epistemic default logic. J Logic Lang Inf 1998;7:341–367. Bosse T, Jonker CM, Treur J. Reasoning by assumption: Formalisation and analysis of human reasoning traces. In: Proc of the IJCAI 2003 Workshop on Cognitive Modeling of Agents and Multi-Agent Interactions; 2003. pp 124 –129. Jonker CM, Treur J. Modelling the dynamics of reasoning processes: Reasoning by assumption. Cogn Sys Res J 2003;4:119 –136.