Temporalizing Epistemic Default Logic.
We present an epistemic default logic, based on the metaphore of a meta-level architecture. Upward reflection is formalized by a nonmonotonic entailment relation, based on the objective facts that are either known or unknown at the object level. Then, the meta (monotonic) reasoning process generates a number of default-beliefs of object-level formulas. We extend this framework by proposing a mechanism to reflect these defaults down. Such a reflection is seen as essentially having a temporal flavour: defaults derived at the meta-level are projected as facts in a next object level state. In this way, we obtain temporal models for default reasoning in meta-level formalisms which can be conceived as labeled branching trees. Thus, descending the tree corresponds to shifts in time that model downward reflection, whereas the branching of the tree corresponds to ways of combining possible defaults. All together, this yields an operational or procedural semantics of reasoning by default, which admits one to reason about it by means of branching-time temporal logic. Finally, we define sceptical and credulous entailment relations based on these temporal models and we characterize Reiter extensions in our semantics.
Introduction
In [MH93a,b] a nonmonotonic logic was introduced, called Epistemic Default Logic (EDL). It
is based on the metaphor of a meta-level architecture. It already has been established in
how upward reflection can be formalized by a nonmonotonic entailment based on
states, and the meta-level process by a (monotonic) epistemic logic. The meta-level
reasoning can be viewed as the part of the reasoning pattern where it is determined what the
possibilities are for default assumptions to be made, based on which information is available
and (especially) which is not. The outcome at the meta-level concerns conclusions of the form
Pj, where j is an object-level formula. In EDL, default conclusions are kept separate from the
object level knowledge (they remain at the meta-level), by means of this explicit default
operator (just like in NML3, see [Doh91]). If one wants to draw further conclusions from
them using object level knowledge this should be done at the meta-level. Compared to a meta-level
architecture, what was still missing was the step where the default assumptions are
actually made, i.e., where such formulas j are added to the object level knowledge, in order to
be able to reason further with them at the object level. Here we actually "jump (down) to
conclusions". This is what should be achieved by the downward reflection step. In the current
paper we will introduce a formalization of the downward reflection step in the reasoning pattern
as well. Thus a formalization is obtained of the reasoning pattern as a whole consisting of a
process of generating possible default assumptions and actually assuming them (a similar
pattern as generated by the so-called BMS-architecture introduced in [TT91]).
The formalization of downward reflection is inspired by [Tre94, HMT94], where it is pointed
out how temporal models can provide an adequate semantics for meta-level architectures in
general, and [ET93, ET94] where these 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-
This work is partially supported by ESPRIT III Basic Research Action No. 6156 (DRUMS II).
a Utrecht University, Dept. of Computer Science, P.O. Box 80.089, 3508 Utrecht. Email: wiebe@cs.ruu.nl.
Also partially supported by the Free University of Amsterdam.
b Like footnote a, but also partially supported by the University of Nijmegen. Email: jj@cs.ruu.nl.
c Free University of Amsterdam, Dept. of Mathematics and Computer Science, De Boelelaan 1081a, 1081 HV
Amsterdam, The Netherlands. Email: treur@cs.vu.nl.
level essentially are statements about the state of the object level reasoning at the next moment
of time. So we can define downward reflection as a shift of time in a (reasoning) process that is
described by temporal logic.
In this paper in the Sections 2 to 6 the logic EDL is presented. As compared with earlier
publications ([MH91a, MH92a, MH93a,b]), the logic is slightly extended in order to cater for
downward reflection in subsequent sections. In Section 7 we define a labeled branching time
temporalization of this logic, in spirit of the approach of [FG92]. In Section 8 we define
sceptical and credulous entailment relations based on temporal models.
2. Epistemic logic
To start with, our language consists of objective formulas together with epistemic formulas.
2.1. DEFINITION (objective and epistemic formulas). Let P be a set of propositional constants
I is either a finite or countably infinite set. The set OBJ of
objective formulas is the smallest set containing P and closed under the classical propositional
connecitves. The formula - is shorthand for (p k . -p k ), for an arbitrary p k - P . The set
FORM of epistemic formulas j, y,. is the smallest set containing OBJ, closed under the
operator K , where Kj means that j is known. Moreover, we use Mj as an
abbreviation for -K-j, meaning that j is epistemically possible. For G - FORM, we denote
by Prop(G) the set of objective formulas in G.
Objective formulas are interpreted on ordinary valuations:
2.2. DEFINITION (propositional models, classical consequence). A valuation is a function s
from P to {t, f}. The set of all valuations is denoted Mod(PC). By determining s' behaviour
under the Boolean connectives, such a valuation is straightforwardly extended to a truth
function on arbitrary objective formulas a (cf. Definition 2.5): we then say that s is a
(propositional model) for a. For any set of valuations M and objective formula a, we write M
. a if any s - M is a model for a.
To interpret the whole set FORM of epistemic formulas, we need richer structures:
2.3. DEFINITION (simple S5-Kripke models). A (simple) S5-model M is a non-empty subset of
Mod(PC). The elements of M are called worlds. We denote the class of simple S5-models by
Mod(S5). Note that for any M # Mod(PC) we may interpret arbitrary objective formulas, but
in order to interpret epistemic formulas (cf. Definition 2.5) we have to conceive M as an S5-
model M.
The more general definition of an S5-model requires M to be of the format
where, for each w - W, p(w) is a valuation (thus, different elements of W may verify the same
objective formulas) and R is an equivalence relation (needed to interpret the operator K), but for
our purposes we will assume S5-models to be simple in the sense as we defined above. One
can show that our assumption does not change the validities of the logic (cf. Definition 2.6
below), but it facilitates a number of technical issues such as the definition of submodels and
union of models. However, some caution is in order here: although the restriction to simple S5-
models does not affect the notion of validity, some of the propositions on S5-models below do
depend on the simplicity of the models, and do not hold for general S5-models.
The set of worlds in an S5-model represents a collection of alternative worlds that are considered
(equally) possible on the basis of (lack of) knowledge. In the next section we shall use S5-
models as representations of the reasoner's objective knowledge and epistemic meta-knowledge
(i.e., what he knows that he knows or does not know).
2.4. REMARK (submodels and union of S5-models). Note that under our notion of S5-models,
which are just sets of valuations, one easily defines a subset relation on S5-models, and an
operation of union upon them.
2.5. DEFINITION (interpretation of epistemic formulas). Given the S5-model M # Mod(PC),
we define the relation (M, s) . j , with s -M by induction on the structure of the epistemic
(M, s) . p -
(M, s) . y
(M, s) . -y - (M, s) - y
(M, s) . Ky - (M, s') . y for all s' - M
(M, s) . My - (M, s') . y for some s' - M.
Note, that the definition of the K-operator states that j is known precisely when j holds in the
whole set of epistemic alternatives; that for the M-operator states that j is considered
epistemically possible iff there is at least one epistemic alternative that satisfies j. In the sequel,
when we write M # Mod(PC) we want to interpret it as a collection of propositional formulas,
whereas, if we write M for the same collection, we intend that M -Mod(S5), on which the
formula Kj has an interpretation. We then say that M is based on M.
2.6. DEFINITION (validity and satisfiability).
(i) j is valid in an S5-model M - Mod(S5), denoted M . j, if for all m - M: (M, m) . j.
(ii) j is valid, notation Mod(S5) . j, if M . j for all S5-models M.
(iii) j is satisfiable if there is an S5-model M and a world m - M such that (M, m) . j.
w.r.t. S5-models can be axiomatized by the system S5:
2.7. DEFINITION (system S5). The logic S5 consists of the following:
Axioms:
propositional tautologies
Knowledge is closed under logical consequence.
Known facts are true.
One knows that one knows something.
One knows that one does not know something.
Derivation rules:
(R1) y
Modus Ponens
(R2)
Kj
Necessitation
That j is a theorem derived by the system S5 is denoted by S5 - j.
2.8. THEOREM (Soundness and completeness of S5). S5 - j - Mod(S5) . j
2.9. DEFINITION. We say a formula y is in normal form if it is a disjunction of conjunctions of
the form d = a . Kb 1 . Kb 2 . Kb n . Mg 1 . Mg 2 . Mg k , where a, b i and g j (i - n,
- are all objective formulas.
The following holds for the logic S5;
2.10. THEOREM ([HC68]) In S5 every formula j is equivalent to a formula y in normal form.
In particular, this theorem implies that every epistemic formula can be represented equivalently
without nested epistemic modalities. In S5 one thus can do without nestings.
3. Epistemic states and stable sets
In this paper we simply define an epistemic state as an S5-model. The idea behind this was
already touched upon after Definition 2.3. The worlds in an S5-model represent the states of
the (real) world that the reasoner considers possible. Thus the S5-model as a whole delimits the
ways the real world is like as far as the reasoner is concerned. In other words, it determines
what he knows about the world and what he does not (what he has doubts about by
considering contradictory possibilities). Therefore, an S5-model represents truly the epistemic
state of the reasoner.
3.1. DEFINITION. An epistemic state is an S5-model M - Mod(S5). The set M of worlds in M
is the set of epistemic alternatives allowed by the epistemic state M. For such a model M, we
define K(M) as the set of facts known in M: . Kj}. We call K(M) the theory
of M or knowledge in M.
We mention here that the knowledge in M are exactly the validities in M:
3.2. LEMMA. For any S5-models M 1 and
3.3. REMARK. The converse relation of - on Kripke models (Cf. Definition 2.4), will play an
important role in the sequel. M 1 - M 2 means that the model M 2 , viewed as a representation of
the knowledge of a reasoner, involves a refinement of the knowledge associated with model
. This has to be understood as follows: in the model M 2 less (or the same) worlds are
considered possible by the reasoner as compared by the model M 1 . So, in the former case the
reasoner has less doubts about the true nature of the world. By Lemma 3.2 it turns out that this
means that with respect to model M 2 the reasoner has at least the objective knowledge
associated with model M 1 , and possibly more. So in a transition of M 1 to M 2 we may say that
objective knowledge is gained by the reasoner. Thus the relation '-' acts as an information
ordering on the set of S5-models. Finally we remark that Lemma 3.2 is a typical example of a
property that holds for simple S5-models only; with respect to general S5-models we would
only have the 'only if' part of the Lemma (cf. the discussion following Def. 2.3).
3.4. PROPOSITION (Moore [Moo85]).
(i) The theory of an epistemic state M is a so-called stable set, i.e., satisfies the
following properties:
(St 1) all instances of propositional tautologies are elements of
(St
(St 5) S is propositionally consistent.
(ii) Every stable set S of epistemic formulas determines an S5-Kripke model M S for which it
holds that is a finite set, then M S is the unique S5-Kripke
model with this property.
The (proof of) the following proposition, which determines stable sets in the realm of classical
propositional logic (cf. St 1 & 5), is also to be found in [Moo85].
3.5. PROPOSITION. A stable set is uniquely determined by the objective formulas it contains.
3.6. REMARK. Thus stable sets act as the epistemic contents of an epistemic state (viz. an S5-
model): a stable set describes exactly the formulas known by the reasoner when he is
is in epistemic state M. From Proposition 3.4(i) we see that this knowledge is closed under
classical propositional reasoning and under positive and negative introspection: if some formula
is known also the fact that this is known is in its turn known by the reasoner, and if some
formula is not known, the fact that it is not known is known itself. This reflects the (perhaps
rather strong notion of) rationality of the reasoner. On the other hand, 3.4(ii) says that a stable
set of epistemic formulas determines an S5-model, the epistemic state associated with
(knowing) this stable set. Proposition 3.5 states that a stable set, and thus the associated
state, is completely determined if one specifies exactly what objective knowledge is
present at the reasoner. The rest of the known set of formulas (the stable set) then follows.
4. Entailment based on epistemic states: upward reflection
On the basis of epistemic states, Halpern & Moses define an entailment relation |~ with which
one can infer what is known, and, more importantly, what is unknown in such epistemic states.
Recall that with every set of valuations M we can associate its epistemic state M in a
straightforward way (cf. Definition 2.5). Intuitively, M associates with M the epistemic state
given by considering (only) the set M of classical propositional models to be the possible states
of the world: this set, so to speak, gives a partial description of the real world. In general, more
than just one classical model is considered possible so that only those facts are known that are
true in all of them. We can exploit this idea further and define an entailment relation based on
the premise that we only know some objective formula j. To this end we need some additional
4.1. DEFINITION. Given some objective formula j, we define M j as the set of valuations
satisfying j}. The epistemic state that is associated with
M j is denoted by M j .
We have the following alternative characterizations of
4.2. PROPOSITION. M
Proposition 4.2 says that in order to get M j , we can also consider all S5-models of j and take
their union to obtain one 'big' S5-model. The result immediately follows from the fact that we
have simple S5-models, and from the fact that, for objective formulas j and arbitrary M -
Mod(S5), M . j - (since j is objective-adopting the view that M - Mod(PC)) M . j -
Now we are ready to define an entailment relation based on this "big" model. Keeping in mind
that '#' acts as an information order on models (Cf. 3.3), we define what are the consequences
of knowing only the objective formula j as those formulas that hold in the "big" model
4.3. DEFINITION (Nonmonotonic epistemic entailment). For
FORM:
Informally, this means that y is entailed by j, if y is contained in the theory (knowledge) of the
"largest S5-model" M j of j. Halpern & Moses showed in [HM84] that this "largest model"
need not always be a model of j itself if we allow j to contain epistemic operators. However,
in our case where we only use objective formulas j, M j is always the largest model for j. This
is obvious from our construction of M j , since M j . j and therefore M j . j (since j is
objective). Moreover, in this case the theory K(M j ) of this largest model is a stable set that
contains j and such that for all stable sets S containing j it holds that
(by Lemma 3.2 and Proposition 3.4), thus K(M j ) is the "propositionally least" stable set that
contains j. So |~ can also be viewed as a preferential entailment relation in the sense of Shoham
[Sho87, 88], where the preferred models of j are the largest ones, viz. M j , where the least
objective knowledge is available.
We denote the mapping j - K(M j ) by k: the stable set associated with
knowing only j. Alternatively viewed, k(j) is the |~-closure of j. Note that since
stable set, it is also propositionally closed.
We give a few examples to show how the entailment |~ works: Let p and q be two distinct
primitive propositions. Then:
Obviously, the entailment relation |~ is nonmonotonic, justifying the name we have given it.
(For instance, we have p |~ M-q, while not p - q |~ M-q; it even holds that p - q |~ -M-q . )
The nonmonotonic epistemic entailment |~ enables us to derive from an objective formula j,
characterizing the exact epistemic state of the reasoner (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 relation |~ goes beyond an entailment expressible in ordinary epistemic logic: with
respect to its premise the relation |~ involves a kind of epistemic closure.
Finally we state a property of that we shall need in the sequel:
4.4. PROPOSITION. The entailment relation |~ enjoys the property:
PROOF. Directly from Definition 4.3 and the fact that the stable set K(M j ) is closed under
conjunction (which in its turn follows from the fact that a stable set is closed under
propositional reasoning and contains the tautology y
5. The epistemic preference logic S5P
The "upward reflection" entailment relation |~ enables us to derive information about what is
known and what is not known. In this section we show how we can use this information to
perform default reasoning. To this end we extend our language with operators that indicate that
something is a default belief and thus has a different epistemic status than a certain fact. In this
way the proverbial "jump to conclusions" is not made directly in the logic, but a somewhat
more cautious approach is taken. The "jump" itself will be part of a next operation, the
"downward reflection", which will be discussed in the next section when we incorporate a
temporal element into our approach.
Let I be a finite set of indexes. The logic S5P of epistemic default logic is an extension of the
logic S5 by means of special modal operators P i denoting default belief (w.r.t.
situation or frame of mind i), for i - I, and also generalisations P t , for t - I.
Informally, read as "j is a default belief (within frame of reference i)". As we shall see
below, a frame of reference (or mind) refers to a preferred subset of the whole set S of
alternatives. This operator is very close to the PA (possible assumption) of [TT91]
and the D (default) operator of [Doh91]. The generalisation P t j is then read as a default belief
with respect to the (intersection of the) frames of reference occurring in t.
Formally, S5P-formulas are interpreted on Kripke-structures (called S5P-models) of the form
is a collection of worlds, M i # M (i - I) are sets
('frames') of preferred worlds, and R
mean that the set of worlds of M 1 is a subset of those of M 2 . Again we have identified worlds
s and their truth assignments. We let Mod(S5P) denote the collection of Kripke-structures of
the above form. Given an S5P-model M we call the S5-
model M based on M the S5-reduct of M'.
5.1. DEFINITION (interpretation of S5P-formulas). Given a model
we extend the truth definition on S5-models by the following clauses for the P i - and
(M, m) . P
(M, m) . P t j iff (M, m') . j for all m' with R t (m, m'), where R
Thus the former clause states that P i j is true if j is a default belief w.r.t. subframe M i ,
whereas the latter says that P t j is true if j is a default belief w.r.t. the intersection of the
subframes t. We will sometimes denote this intersection by M t . In the clause for P t ,
we assume that, for M. So in this special case we get that the P t
modality coincides with the knowledge operator K . Validity and satisfiability is defined
analogously as before.
It is possible to axiomatise (the theory of) Mod(S5P) as follows (cf. [MH91a, MH93a]): take
the S5 system for the modality K (and dual M) and use K45 for the P-modalities (both the P i
and the P t ), together with relating axioms, resulting in the system:
5.2. DEFINITION (system S5P). In the following, i ranges over I, and t over subsets of I .
Moreover, - is a variable over {K, P
propositional tautologies;
(R1) Modus Ponens
(R2) Necessitation for K: - j - Kj.
Axiom (B1) says that we are dealing with an extension of propositional logic; (B2) says that all
the operators K, P i , and P t are 'normal'; (B3 and B4) express that the relations R, R i and R t
are transitive and Euclidean, respectively; (B5) says that R is reflexive; (B6) and (B7) help us
to get rid of nested modalities: a nested modality is always referring to the frame corresponding
to the innermost one. (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 t #
t', then R t' # R t . Finally, (B10) is the syntactical counterpart of our definition that
We call the resulting system S5P. In the sequel we will write G - S5P j or j - Th S5P (G) to
indicate that j is an S5P-consequence of G. We mean this in the more liberal sense: it is
allowed to derive j from the assertions in G by means of the axioms and rules of the system
S5P , including the necessitation rule. (So, in effect we consider the assertions in G as
additional axioms: G - S5P j iff - S5P-G j.)
As for S5, one can again prove a normal form theorem for S5P implying that all formulas can
be represented equivalently as formulas without nestings.
5.3. THEOREM G - S5P j - (for all M - Mod(S5P): M . G - M .
PROOF. In the Appendix.
6. Epistemic Default Logic (EDL)
In the language of S5P we express defaults of the (using Reiter's notation, Cf.
are objective formulas. The
reading of such a formula is "if j is true and y is (considered) possible, then c is preferred
(within frame M i )". Usually we consider cases where y is syntactically equal to c (the so-called
normal defaults).
By combining the formal apparatus of S5P with Halpern & Moses' nonmonotonic epistemic
entailment we obtain a framework in which we can perform default reasoning. In this paper we
call this framework Epistemic Default Logic (EDL).
6.1. DEFINITION (default theory). A default theory Q is a pair (W, D), where W is a finite,
consistent set of objective (i.e. non-modal) formulas describing (necessary) facts about the
world, and D is a finite set of defaults of the form j - My- R i c, where j , y and c are again
objective formulas, and i - I. The sets W and D are to be considered as sets of axioms, and we
may apply necessitation to the formulas in them.
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, in order to be able to treat the various
defaults in a default theory separately from each other, in the sequel we shall assume all P-
operators in a default theory to be distinct. This will allow for a generic way to look at the
possibilities of combining default beliefs by using the P t -operators. So, for example rather
than to look at a default theory with in which for both
defaults the same operator P 1 is used, we consider the set D
R 2 s}, in which both defaults are represented by means of different operators P 1 and P 2 , and
consider the combined operator P {1, 2} .
6.2. DEFINITION (default entailment). Let a default theory D) be given. Let W* be the
conjunction of the formulas in W. Note that W is a finite set, and moreover that W only
consists of objective formulas. Furthermore, let j be an objective formula. Then we define the
entailment relation |~ Q w.r.t. default theory Q as follows: (Recall that k(j) stands for
the |~-closure of j, where |~ is the nonmonotonic epistemic entailment of section 4.)
y.
This definition states that, given a default theory Q, y is a default consequence of j iff y
follows in the S5P-logic from the defaults together with what is implied by knowing only the
conjunction of j with the background information W.
Notice that the following equivalence holds, which states something about a modularity of the
entailment relations.
6.3 PROPOSITION
there exists a S5-formula y' - FORM such that
j-W* |~ y' and {y'} - D - S5P y
PROOF. This follows directly from the definition of |~ Q and Proposition 4.4, as is seen as
follows. Suppose we have j |~ Q y, i.e, k(j-W*) - D - S5P y. The logic S5P is compact,
hence there are a 1 , ., a k -k(j-W*) and d 1 , ., d n -D such that a 1 , . a k , d 1 , ., d n
y. By definition of k, since for each i - k, a i - k(j-W*) we have j-W* |~ a i for all i
by Proposition 4.4, y' satisfies the right-hand side of 6.3. -
Instead of true |~ Q y, we simply write |~ Q y. Note that, for
y, with Furthermore, if G is a finite set of epistemic formulas, and y
an S5P-formula, then we define G |~ Q y as G* |~ Q y, where G* stands for the conjunction of
the formulas in G.
6.4. EXAMPLE (Tweety). Consider the following default theory
-f} and representing that penguins do not fly, and that by default birds
fly. (For convenience we omit the subscript of the P-operator.) Now consider the following
(i). b |~ b -K-f (1)
meaning that from the mere fact that Tweety is a bird, we conclude that Tweety is assumed to
fly. (Here |~ stands for Halpern & Moses' nonmonotonic epistemic entailment.) This must be
contrasted to the inference:
(ii). b - p |~ Kp - S5P K-f (1)
i.e, not b - p |~ Q Pf,
meaning that in case Tweety is a penguin, we cannot infer that Tweety is assumed to fly, but
instead we can derive that we know for certain that Tweety does not fly: b - p |~ Q K-f .
7. A temporal formalization of downward reflection
In the previous section it has been described how upward reflection can be formalized by a
nonmonotonic inference based on epistemic states, and the meta-level process by a (monotonic)
logic. In the current 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 default assumptions to
be made, based on which information is available and (especially) which is not. The outcome at
the meta-level concerns conclusions of the form Pj, where j is an object-level formula. What
is still missing is the step where the default assumptions are actually made, i.e., where such
are added to the object level knowledge, in order to be able to reason further with
them at the object level. Here we actually "jump (down) to conclusions". 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 default assumptions and actually assuming them.
By these downward reflections at the object level a hypothetical world description is created and
refined. This means that in principle not all knowledge available at the object level can be
derived from the object level theory W: downward reflection creates an essential extension to
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(j) then at the object level j is provable" (e.g., see [Wey80]):
A reflection rule like this can only be used in a correct manner if the meta-theory about
provability gives a sincere axiomatisation 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. In the above rule the meta-theory is only concerned with one fixed
object level theory. Since we essentially extend the object level theory, and consequently want
to move to another object level theory, an approach as taken in the rule above cannot serve our
purposes here.
In fact, in our case a line of reasoning at the object level is modelled by inferences from
subsequently chosen theories instead of inferences from one fixed theory, where in the choice
of the next object-level theory the upward and downward reflections play a role. Another
difference with the above "traditional" approach to meta-level reasoning is that we shall treat
these reflection steps model-theoretically instead of proof-theoretically, as shifts from one
model to another, which results in a temporal "super"-model indicating how these shifts may
take place over time. Actually, to keep in perfect line with the above, we should explain by
means of these models how object knowledge (modelled by a set M of valuations) is reflected
upwards to get a model for epistemic meta-knowledge (modelled by an S5-model M), how this
meta-knowledge is then extended with meta-knowledge about default beliefs (modelled by S5P-
models), and how, subsequently, this meta-knowledge is reflected downwards to object
knowledge (modelled by a new set M' of valuations) again. However, representing such shifts
in a temporal model would involve (sequences of) three different models (sets of valuations,
S5-models and S5P-models), which would be quite involved and cumbersome. Therefore, in
order not to complicate our temporal models too much, in our present setting we shall not
represent the above three steps separately, but treat them "in one blow", so to speak, i.e., as
one "super"-step. Now we are able to represent these "super"-steps as shifts from S5P-models
to S5P-models, so that our temporal "super"-model only involves sequences of one kind of
model, viz. S5P-models, of which the S5-reducts represent the reasoner's objective knowledge
and epistemic meta-knowledge, and the frames ('P-') parts represent meta-knowledge in the
form of default (or preferred) beliefs. We shall still refer to these supersteps as downward
reflection, although as we stated above, apart from a reflection of the "meta-knowledge" in the
form of default beliefs contained in the S5P-model at hand to the object level by converting
some of these beliefs into object knowledge, it also includes an immediate upward reflection
from the next object level theory (or rather model) resulting from this to the next meta-level
theory as represented by an S5P-model again.
In [GTG93] 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 reflection rules ('bridge rules' in their terms) may have
the form:
Here it is assumed that 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 above reflection rule.
As we said above, 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 [Tre94]). In a simplified case, where no branching is taken into account,
the following temporal axioms can be used to formalize downward reflection:
for every objective formula j. Here X is the temporal operator asserting that in the next
(epistemic) state its argument is true.
In the general case we want to take into account branching and the role to be played by an index
t in P t j. We will use this index t to label branches in the set of time points. By combining
EDL with the temporal logic obtained in this manner we obtain a formalization of the whole
reasoning pattern.
We start (following [FG92]) by defining the temporalized models associated to 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. I , the powerset of the index set I. However, in most definitions we do not
use this fact, but only refer to (elements t of) L.
7.1 Flows of time
7.1. DEFINITION (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
consisting of a nonempty (countable) set T of time points and a collection of
binary relations < t on T. Here for s, t in T and t in L the expression s < t t denotes that t is a
(immediate) successor of s with respect to an arc labeled by t. Sometimes it is convenient to
leave the indices out of consideration and use just the binary relation s < t denoting that s < t t
for some t (for some label t 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 in which time branches in the direction of the future.
7.2. DEFINITION (labeled time tree)
An called a labeled time tree (ltt) if the following additional conditions
are satisfied (recall that
(i) the graph (T, <) is a directed rooted tree.
(ii) (successor existence)
Every time point has at least one successor:
for all s - T there exists a t and a t - T such that s < t t
(iii) (label-deterministic)
For every label t there is at most one t-successor:
for all s, t, t' - T it holds: s < t t, s < t t' -
There are still some additional properties that sometimes are required.
7.3. DEFINITION (sub-lft and (maximal) branch)
a) An lft (T', (<' t called a sub-lft of an lft (T, (< t
holds It is also called the sub-lft of (T, (< t defined by T', or
the restriction of (T, (< t
b) A branch in an lft T is a sub-lft
(i) - T' x T' is a total ordering on T' x T'
(ii) Every t' in T' with a <-successor in T also has a <-successor in T':
for all t' - T', t there is a s' - T' : t' < s'
(iii) Every element of T that is in between elements of T' is itself in T':
for all s' - T', t - T, u'
c) A branch is called maximal if every t' in T' with a t-predecessor in T also has a t ' -
predecessor in T' for some t': for all t - T, t' there is a t ' and an s' - T' :
s' < t' t'. (Note that if T is a labeled time tree, this condition can be simplified to: the root r
of T is also the root of T'.)
We now immediately have the following:
7.4. PROPOSITION Any branch of an ltt T is an ltt.
7.5. DEFINITION
a) An lft is called successor-complete if for every label t every time point has at least one t-
successor: for all s and t there exists a t such that s < t t.
b) A path is a finite sequence of successors: s 0 , ., s n such
We call s 0 the starting point and s n the end point of the path.
7.6. DEFINITION (time stamps). Given an ltt (T, (< t is called a
time stamp mapping if for the root r it holds that and for all time points s, t it holds s < t
1. (Note that this time stamp mapping is unique.)
Note that an ltt is infinitely deep, i.e., for every k - N there is a time point t - T with
This is a direct consequence of the following proposition:
7.7. PROPOSITION
If B is a maximal branch in an ltt, then any time stamp mapping is an isomorphism between B
and N.
7.2 Temporal models
We first define our temporal formulas:
7.8. DEFINITION (temporal formulas).
a) Given a logic L, temporal formulas over (the language of) L are defined as follows:
of L then Cj is a temporal formula (also called a temporal atom)
ii if j and y are temporal formulas, then so are:
-j, j . y, j ' y, X $,t j, X
b) Below, our main concern will be temporal formulas over S5P; we will also refer to them
as TEDL-formulas (temporal epistemic default logic formulas).
The above temporal operators are fairly standard in branching-time temporal logic: X refers to
next-time, F to sometimes in the future and G to always in the future; the subscripts refer to
whether one considers only some ($) possible path (possibly with a fixed label t) or all (") of
these. The C-operator is the least standard: it means 'currently'. Usually in temporal logic this
operator is not really useful, since it just states that its argument, say j, holds in the current
state, which is normally represented by the formula j itself, without a C in front. Here,
however, we have a logic where we mix temporal and epistemic logic, and the C-operator acts
as a kind of separator between the epistemic and temporal part: in Cj, its argument j is an
itself is a temporal formula. This also facilitates the semantic
definition below.
7.9. DEFINITION (temporal models)
a) Let MOD be a class of models, and labeled flow of time.
A temporal MOD-model over T is a mapping M: T - MOD. If M is a temporal MOD-
model for any class MOD we call M a temporal model.
For (the snapshot at time point t) by M t . The temporal
model can alternatively be denoted by (M t ) t-T .
b) If we apply a) to the classes of models Mod(PC), Mod(S5) and Mod(S5P), we call
these temporalized models temporal PC-models, temporal S5-models and temporal S5P-
models over T, respectively.
c) Given an lft T, the temporal formulas are interpreted on MOD-models over T as follows:
conjunction and implication are defined as expected; moreover
M, s . -j iff not M, s . j;
ii The temporal operators are interpreted as follows:
means that in the current state j is true, i.e.
M, s . Cj iff M s . j
means that j is true in some t-successor state i.e.,
M, s . X $,t j iff there exists a time point t with s < t t such that M, t . j
means that there is a t with some t-successor in which j is true.
there exists a time point t with s < t such that M, t . j
meaning that j is true in all t-successor states, i.e.,
M, s . X ",t j iff for all time points t with s < t t it holds M, t . j
means that j is true in all immediate successors:
means that j is true in some future state, i.e.,
there exists a time point t with s - t such that M, t . j
means that for all future paths there is a time point where j is true, i.e.,
starting in s there is a t in B with M, t . j.
means that j is true along some future path, i.e.,
there exists a branch B starting in s with M, t . j for all t in B.
means that j is true all future states i.e.
M, s . G " j iff for all time points t with s - t it holds M, t . j.
Note that the operator C enforces a shift in the evaluation of formulas; taking us from a
temporal model M and a time point t to an S5P-model M t .
During the reasoning process we assume to gradually extend the information we have at the
object level, and consequently to shrink the set of possible worlds by means of reflecting
default beliefs downwards to object knowledge. In terms of temporal S5-models we can
formulate this property as follows:
7.10. DEFINITION. A temporal S5P-model obeys downward reflection, if the following holds
for any s and
the frame M t in M s is non-empty - there is a t with s < t t and for all such t
the set of worlds of M t equals M t
The above property expresses that the possible worlds in frame M t (representing the P t -default
beliefs) are taken to be the whole set of possible worlds (representing the objective knowledge)
in some (t-) successor epistemic state (or, rather, S5P-model).
Finally, we are ready to zoom in into the models we like to consider here, the temporal
models.
7.11. DEFINITION (TEDL-models)
TEDL-model M is a temporal S5P-model over an lft T such that:
1) T is a labeled time tree;
For every time point s, there is exactly one t with s <- t;
reflection.
The following notion is a crucial one for the sequel:
7.12. DEFINITION (conservativity and limit models). Let labeled flow of
time. A temporal PC-model M over T is conservative if for every two time points s and t with s
< t it holds that M(s) # M(t).
Suppose M is a conservative temporal PC-model. The intersection of the models M(s) for all s
in a given (maximal) branch of the lft T is called the limit model of the
branch, denoted lim B M. The set of limit models for all (maximal) branches is called the set of
limit models of M. These definitions straightforwardly extend to S5- and S5P-models, by
identifying M with its set of worlds, M.
7.13. THEOREM. TEDL-models are conservative.
PROOF. Suppose s < t, that is, for some label t, s < t t. Since TEDL-models obey downward
reflection and the underlying lft is an ltt, this means that the (now unique) set of worlds M t of
M t is the frame M t of M s . Since M t # M s , the set of worlds of M s , this gives M t # M s ,
which proves the theorem. -
Since we know that TEDL-models are conservative, we have that once we have obtained that
somewhere in a time point s along some path of such a model some objective formula is
known, it remains known in all successor points of s. (This is in fact the rational behind the
name "conservative models".) We can make this more precise if we introduce so-called cko-
formulas, which are formulas of the form CKj, where j is objective. In the sequel we will
denote cko-formulas by a. Then we have that:
7.14. PROPOSITION. Let M be a TEDL-model, and a a cko-formula.
If, for some s, M, s . a, then M, t . a for all t with s - t.
PROOF. Suppose M, s . a, for a = CKj. We show that for t with s < t we have that M, t .
a. (Then we can finish the proof by induction on the number of time point between s and t.)
By Theorem 7.13, we have that M t # M s . This yields: M, s . a - M, s . CKj - M s .
is objective and M t # M s we then must have M t ,
. j for all m in M t and hence M t . Kj. Finally, we have the equivalences M t . Kj -
Furthermore, TEDL-models enjoy a number of properties that can be expressed as validities in
our logic:
7.15. THEOREM. TEDL-models satisfy the following validities:
T0 All the operators of {X ",t , X" , F" , G" } satisfy the K-axiom (C too) and generalisation;
(introduction of C)
existence & label-deterministic)
is union of < t )
(dual of T6)
objective (allowing downward reflection)
objective (trivial downward reflection)
objective (conservativity)
transitive closure of <)
(from conservativity and induction)
7.17. REMARK. The Theorem above says that the formulas are at least sound; until
now we have not been concerned by designing a logic that is complete for TEDL-models.
8. TEDL models of default theories and entailment relations
We could formulate definitions of entailment of objective formulae 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 to the background knowledge. It is not realistic to base entailment on such
informationally poor branches in a model. Therefore we define:
8.1. DEFINITION (informationally maximal)
We define for TEDL-models M 1 and M 2 over the same flow of time that M 2 is informationally
larger
We call M 1 informationally maximal in a class M of models if it is itself the only model that is
informationally larger.
For a given model M we will apply this definition to the set B of all maximal branches, with T
flow of time.
8.2. DEFINITION (regular model)
TEDL-model M is called regular if all maximal branches are informationally maximal in the
class of maximal branches. The submodel based on all time points t included in at least one
maximal, informationally maximal branch is called the regular core of M, denoted by reg(M) .
8.3. REMARK.
In general the regular core will not be label-complete, because branches may be cut off. The
idea behind taking informationally complete branches is that we want to maximalise the effect of
applying defaults in order to obtain as much (default) knowledge as possible.
8.4. DEFINITION.
Let M be a TEDL-model over
We define for k - N
where M'(t) stands for the S5-reduct of the S5P-model M(t).
8.5. PROPOSITION.
Let M be a TEDL-model.
a) For k - k' it holds M (k') # M (k)
branch of reg(M
PROOF. a) follows directly from Theorem 7.13, b) follows from the distributivity of
intersection over union (and vice versa). -
8.6. DEFINITION (sceptical entailment)
Let M be a TEDL-model and a a cko-formula. We define the sceptical entailment relation by:
M | - scep a - for every maximal branch B in reg( M) there is a t in B such that M, t . a.
An immediate consequence of this definition is:
8.7. PROPOSITION.
If, for some k - N, M (k) . Kj, then M | - scep CKj.
PROOF. Suppose M (k) . Kj, for some k - N. This means that M'(t) . Kj for all S5-reducts
M'(t) with t in reg(M) and k. So for every maximal branch B in reg( M) we can find a t in
B such that M, t . Kj (viz. take t in B such that |t| = k. By Proposition 7.7 we can always do
this). Hence, M | - scep CKj. -
8.8. PROPOSITION.
Let M be a TEDL-model with root r. Let a = CKj be a cko-formula.
The following are equivalent:
reg(M), r . F " a
. Kj for every maximal branch B of the regular core of M.
PROOF. Clearly (i) and (ii) are equivalent.By Prop. 8.5 also (iii) and (iv) are equivalent. We
now show the equivalence of (i) and (iv). First we prove (i) - (iv): Suppose M | - scep CKj,
i.e. for every maximal branch B in reg( M) there is a t in B such that M, t . CKj. Now
consider a maximal branch B in reg( M). Then there is a t in B with M, t . CKj, i.e. M(t) .
Kj. By the conservativity of M we have that M(u) . Kj for all u - t, i.e., all worlds of the
models M(u) with u - t satisfy j. But then also all worlds of the models M(u) with u - t and u
in B satisfy j. Consequently, lim B
Next we prove (iv) - (i): Suppose lim B M . Kj for every maximal branch B of the regular
core of M. We have to prove that for every maximal branch B in reg( M) there is a t in B such
that M, t . CKj. Take some maximal branch B in reg( M). Then we know that lim B M . Kj,
i.e., - u in B M(u) . Kj. By the conservativity of the model M (Theorem 7.13) we know
that the sequence <M(u) | u in B> is monotonically decreasing (with respect to -). Let P
the set of propositional atoms occurring in the formula a (or j). Clearly, P 0 is finite. Now, for
any S5-model M with set S of worlds (truth assignment functions) we let M 0 denote the model
with set S 0 of worlds: S
for some s - S}. Clearly, M . Kj iff M 0 . Kj.
Now consider the sequence <M(u) 0 | u in B>. This is a monotonically decreasing sequence
with intersection - u in B M(u) 0 . Since P 0 is finite, and we identified worlds with truth
assignment functions, we have that all the models M(u) 0 contain only a finite number of
worlds. Together with the fact that the sequence is monotonically decreasing this yields that the
sequence must be stable from some point s in B on: M(u)
obviously the intersection - u in B M(u) . So now M(s) 0 . Kj, and thus M(s) .
Kj, i.e. M, s . CKj. -
For our definition of credulous entailment we can be less restrictive. Especially, too less
information in one branch can always be overcome by another, informationally larger branch.
8.9. DEFINITION (credulous entailment)
Let M be a TEDL-model. We define:
cred CKj - there exists an s with
M | - cred CKj - there exists an s with M(s) . Kj
8.10. PROPOSITION.
Let M be a TEDL-model, and a = CKj a cko-formula.
The following are equivalent:
cred a
cred a for some k - N.
. Kj for some maximal branch B
PROOF. Since clearly (i), (ii) and (iii) are equivalent, we concentrate on the equivalence of (ii)
and (iv): we first prove (ii) - (iv): Let M | - k cred CKj for some k - N. This means that there
exists an s with and M(s) . Kj, i.e., M, s . CKj. By Prop. 7.14, we then have that
M, t . CKj for all t with s - t. Now consider any maximal branch B through s. Clearly, this
branch has the property that the models M(t) with s - t all satisfy Kj, i.e., j holds in every
world of every model M(t). But then j holds in the intersection of these models as well. This
proves . Kj.
Next we prove (iv) - (ii): Suppose that lim B M . Kj for some maximal branch B . This
means that Kj holds in the intersection of the models M(t) along B . By the conservativity of
the model M (Theorem 7.13) we know that the sequence <M(t) | t in B> is monotonically
decreasing (with respect to -). Let P the set of propositional atoms occurring in the
formula a (or j). Clearly, P 0 is finite. As above, we denote, for any S5-model M with set S of
worlds (truth assignment functions), the model with set S 0 of worlds by M 0 where S
for some s - S}. Again, M . Kj iff M 0 . Kj. Now consider the sequence <M(u) 0 | u
in B>. This is a monotonically decreasing sequence with intersection - u in B M(u) 0 . Since P 0
is finite, and we identified worlds with truth assignment functions, we have that all the models
only a finite number of worlds. Together with the fact that the sequence is
monotonically decreasing this yields that the sequence must be stable from some point s on:
obviously the intersection - t in B M(t)
the intersection satisfies Kj, we obtain that M(s) 0 . Kj, and thus M(s) . Kj. Hence M | - cred
CKj. -
We can now associate TEDL-models with default theories as follows.
8.11. DEFINITION (TEDL-model of a default theory).
D) be a default theory. Then we define a TEDL-model of Q as a TEDL-model M Q
such
(i) (basis: the root) M Q r is an S5P-model such that (a) the S5-reduct of M Q r is the S5-model
W* , as defined in Section 4, and (b) M Q r satisfies the set of defaults, i.e., M Q r . D.
(ii) (induction step) Suppose that we are given an S5P-model at snapshot M Q s . Then we have
that for a(n S5P-) model M Q t with s < t t, it holds that: (a) the S5-reduct of M Q t is the S5-
model M t as it appeared as a frame in M Q s , and (b) M Q t satisfies the set of defaults again, i.e.,
. D.
Note that, in general, there are multiple TEDL-models of a default theory Q. Furthermore, note
that clause (ii)(a) reflects the downward reflection operation with respect to the P t -defaults.
This definition enables us to finally give the definitions of sceptical and credulous entailment
from a default theory.
8.12. DEFINITION (entailment from a default theory).
D) be a default theory, and j an objective formula. Then:
models M of Q it holds M | - scep CKj
cred j iff for all models M of Q it holds M | - cred CKj
Of course, we have that what is entailed sceptically, also is entailed credulously:
8.13. PROPOSITION. For default theory Q and objective formula j: Q | - scep j - Q | - cred j
Sceptical and credulous entailment are not the only approaches to define semantics for default
logic. Sceptical entailment can be considered a lower bound of the conclusions that can be
drawn, credulous entailment as an upper bound. A more differentiated approach bases
semantics of the default theory on the set of all alternative extensions that actually can be
constructed out of a default theory using the defaults as (non-monotonic, context-dependent)
inference rules. The original approach by Reiter [Rei80] defines the extensions of a default
theory by means of a pseudo-construction or fixed point definition; we will call these
extensions Reiter extensions.
In Constructive Default Logic, introduced in [TT92], the notion of Reiter extension is replaced
by the weaker notion of constructive extension. In [TT92] it was proven that the Reiter
extensions of a default theory are among the constructive extensions and they were
characterised. Constructive extensions give a broader perspective on the semantics of a default
theory. The formalisation in terms of branching time models introduced in the current paper, in
the first place is the temporal formalisation of the construction process of a constructive
extension. Just like in the case of Constructive Default Logic, in the applicability condition of a
point s, the justification My only refers to the current state of
information (and not to the whole (future) context of the reasoning pattern as in Reiter's case is
required). Because of this similarity for every (maximal) branch B in a TEDL-model M of a
default theory D), the theory of its limit Th(lim B M) is a constructive extension of Q
and the branch itself represents a construction chain of this constructive extension.
As the Reiter extensions are among the constructive extensions, a natural question is how in a
TEDL-model of a default theory the branches that lead to a Reiter extension can be
characterised. Based on variants of the notions self-defeatingness and exhaustiveness
introduced in [TT92], it is not difficult to find such a characterisation.
8.14. DEFINITION
Let M be a TEDL-model of the default theory branch in M.
The branch B is called self-defeating if there is a time point s in B and a default
in D such that the following holds:
for all time points t, t' in B and labels t with t < t t' and every default j ' - My ' - R j c in
D with j in t, there is some time point u in B with B u . o/oo y '.
Otherwise the branch B is called non-self-defeating.
The notion of non-self-defeatingness quarantees that any default conclusion that is drawn will
remain justified in the strong Reiter sense during the whole process. However, this is only one
side of the characterisation. It may well be the case that the defaults applied in branch B are
justified in the strong sense, but not all applicable defaults actually have been applied in B .
Therefore the notion of exhaustiveness is required:
8.15. DEFINITION
Let M be a TEDL-model of the default theory branch in M.
The branch B is called exhaustive if for every time point s in B and every default
in D such that B s . j and for all time points t in B it holds y,
then there is a time point s' in B and a label t with s< t s' and i is in t.
Based on these two conditions we can characterise the branches leading to Reiter extensions:
8.16. THEOREM
Let M be a TEDL-model of the default theory D). The following are equivalent:
(i) E is a Reiter extension of Q
(ii) there exists a non-self-defeating and exhaustive branch B in M with
The proof is similar to the proof of the main result in [TT92]. The following example default
theory illustrates our
a
r1: a - Mc - R 1 b
r3: a - Mo/oo c - R 3 o/oo c
In

Figure

1 the different reasoning paths are depicted. At each node the literals that are true at
the object level are depicted, and, between [.], the applicable default rules. At each arc the
label is depicted and, between (.), the justification it is based on.
a
[r1, r3]
a a, b a, o/oo c a, b, o/oo c
[r1, r3] [r2, r3]
a, b a, b, o/oo c
[r2, r3]
(c) ( o/oo c) (c, o/oo c)
(c) ( o/oo c)

Figure

Reasoning paths for an example default theory
The branch leading to a, b, c is non-self defeating and exhaustive, so it leads to the Reiter
extension Cn({a, b, c}). The same holds for the branch leading to a, o/oo c. The two branches
leading to a, b, o/oo c, however, are self-defeating: the occurrence of o/oo c leads to the defeat of
the earlier justification c. Therefore Cn({a, b, o/oo c}) is a constructive extension, but not a
Reiter extension.
9. Conclusions
In [MH93a,b] an Epistemic Default Logic (EDL) was introduced inspired by the notion of
meta-level architecture that also was the basis for the approach introduced in [TT91]. 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 default assumptions actually can be made).
In [TT91] downward reflection takes place, but no semantical formalization was given: it was
defined only in a procedural manner.
In principle downward reflection disturbs the object level semantics, since facts are added
that are not logically entailed by the available knowledge. Adding a temporal dimension (in the
spirit of [FG92]) to EDL enabled us to obtain formal semantics of drawing a default
conclusion in a dynamic sense: as a transition from the current object level theory to a next one
(where the default conclusion has been added).
The approach as developed provides a formalisation of default reasoning using labeled
branching time temporal models. Within these models various types of semantics can be
defined: semantics based on sceptical or credulous entailment, and semantics based on
constructive extensions or Reiter extensions.
[TT92] Y.H. Tan, J. Treur, Constructive Default Logic and the Control of Defeasible
Reasoning, in: B. Neumann (ed.), Proc. of the European Conference on Artificial
Intelligence, ECAI'92, Wiley & Sons, 1992, pp. 299-303.

Acknowledgements

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


Appendix


In this appendix, we provide a proof for theorem 5.3. First, we introduce an alternative class
of Kripke models.
Definition A1. We define the class A(S5P) of alternative models for S5P . Elements M of
A(S5P) are tuples



--R


A Temporal Model Theory for Default Logic
Adding a temporal dimension to a logic system

An Introduction to Modal logic
Towards a Theory of Knowledge and Ignorance
Formal Semantics of Temporal Epistemic Reflection

A. Modal Logic for
An Epistemic Logic for Defeasible Reasoning using a Meta-Level Architecture Metaphor
A Default Logic Based on Epistemic States.
Epistemic Logic for AI and Computer Science
Semantical Considerations on Nonmonotonic Logic
A Logic for Default Reasoning
Annual Reviews of Computer Science 2
A Semantical Approach to Nonmonotonic Logics


Constructive Default Logic and the Control of Defeasible Reasoning
Temporal Semantics of Meta-level Architectures for the Control of Reasoning
Prolegomena to a Theory of Mechanized Formal Reasoning
--TR
default reasoning;temporal models;meta-level architectures;epistemic states