# Executable Temporal Logic for Nonmonotonic Reasoning

发布时间:2021-11-29 07:14:59

J. Symbolic Computation

(1996)

22, 615{625

Executable Temporal Logic y for Nonmonotonic Reasoning

Free University Amsterdam, Department of Mathematics and Computer Science De Boelelaan 1081a, 1081 HV Amsterdam, The Netherlands tel. +31 20 4447756, fax. +31 20 4447653 email: fjoeri, treurgcs.vu.nl (Received 22 May 1996)

In this paper we view nonmonotonic reasoning as a (special kind of) process. As temporal logic is a common formalism to specify and derive properties of processes, we introduce a variant of temporal logic as a general speci cation language for reasoning processes. We show that it is possible to execute nite speci cations in this language, which leads to executability of a large class of nite nonmonotonic reasoning processes.

JOERI ENGELFRIET AND JAN TREUR

Nonmonotonic reasoning is used when an agent wants to draw conclusions about the world based on its partial knowledge of the world. Classical logic usually permits too few conclusions for the agent to base its actions upon. Using nonmonotonic reasoning the agent can extend its partial knowledge to a set of hypothetical beliefs. In general there will be more than one set of beliefs which is a reasonable extension of the (sure) knowledge. Starting from the set of initial facts the agent can construct all or one of the possible belief sets using nonmonotonic inference rules. It may then commit to one of these views (and, if needed, change its commitment later), or it may focus on the intersection of these views. The construction of a belief set is a stepwise process. The reasoning agent starts with a set of initial facts to which it applies a number of nonmonotonic inference rules to obtain a larger set of beliefs or conclusions. To this set it may again apply nonmonotonic rules to arrive at a next set of beliefs. Viewed in this way, a nonmonotonic reasoning process is (just) a special kind of process. Temporal logic is recognized as a valuable tool for specifying processes and reasoning about their properties. For each class of processes, a di erent version of temporal logic might be most appropriate. As we are interested in specifying reasoning processes, we will introduce a version of temporal logic suited to describe reasoning processes. In particular, since a state in a reasoning process should contain the beliefs or conclusions the reasoning agent has arrived at in that state, we

Part of this work has been supported by the ESPRIT III Basic Research project 6156 DRUMS II c 1997 Academic Press Limited 0747{7171/90/000000 + 00 $03.00/0

y

1. Introduction

2

J. Engelfriet and J. Treur

propose a temporal epistemic logic as a general speci cation language for nonmonotonic reasoning processes. Using temporal logic for specifying processes allows veri cation and validation of a process. The bene t of using an executable temporal logic is that processes speci ed in this logic can also be directly executed, so that reasoning about a process and actually executing it, can be done in the same language. It will be shown that speci cations in our version of temporal logic can be executed, leading to a general algorithm for executing nonmonotonic reasoning processes. Although there are similarities with existing executable temporal logics (see (Gabbay, 1989), (Fisher, 1994), (Fisher and Owens, 1995), (Orgun and Ma, 1994)), there are some di erences as well. The complexity of this algorithm is complete in the complexity class where many nonmonotonic formalisms reside. In Section two we will formalize the reasoning processes we want to specify using reasoning frames and in Section three we introduce our temporal speci cation language for these reasoning frames. In Section four we will show that any nite speci cation is executable, leading to executability of nite (nonmonotonic) reasoning processes. Section ve contains conclusions and suggestions for further research. We will start by describing semantically the reasoning processes we would like to specify, reason about, and execute. Classical (propositional) logic lies at the base of most nonmonotonic formalisms, so we will assume we have a propositional language, L, its corresponding set of models, Mod, and the (semantic) consequence relation j= Mod L. Furthermore, for a set X L, we de ne the models of X : Mod(X ) = fm 2 Mod j m j= for all 2 X g; the consequences of a set X L are de ned by Cn(X ) = f 2 L j Mod(X ) Mod( )g. For a subset K of Mod, the theory of K is de ned by Th(K ) = f j m j= for all m 2 K g. A set of models K is called closed if K = Mod(Th(K )), or equivalently, if K is the set of models of a theory. Intuitively, the path from initial set of formulae to nal conclusions can be seen as the behavior of a reasoning process which starts with the initial formulae, then makes some nonmonotonic inferences to arrive at a new state, again makes some inferences, et cetera, possibly ad in nitum. The nal conclusions of such a process can be seen as the union of all conclusions drawn at all stages. A formalization of such reasoning behavior would have to describe which formulae have been derived at each stage. We will formalize the notion of state in a reasoning process semantically by the notion of an information state, which should describe the formulae which the agent has concluded (or which the agent believes) in that state:

Definition 2.1. (Information State)

2. Reasoning Frames

1 An information state M over the language L is a non-empty closed set of propositional models for L, that is, there is a consistent theory of which it is the model class. The truth of a propositional formula in such a state is de ned by: M j= , m j= for each m 2 M 2 The theory of an information state M is de ned by: Th(M ) = f j is a propositional formula and M j= g 3 The re nement ordering on information states is de ned by: 4 The set of all information states is denoted by IS .

M1 M2 , M2 M1

Executable Temporal Logic for Nonmonotonic Reasoning

3

So the theory of an information state contains the formulae the agent believes in that state. It is important to note that an information state models the partial information the agent has about the world. Thus it may be the case that a formula is not true in an information state, and its negation is not true either (this happens when the information state contains a propositional model in which is false, and one in which it is true). Using these notions we can now de ne a reasoning trace as a speci c type of sequence of such information states. We assume that the reasoning at least is conservative: conclusions constructed in earlier stages will be persistent during the reasoning trace. Although many reasoning processes are nite (after a while, no new nonmonotonic inferences can be made), for simplicity we will only consider in nite traces. A process which is nite will give rise to a trace which is constant after a certain point. In particular, if the propositional signature is nite, all traces will be constant eventually.

Definition 2.2. (Reasoning Trace and Limit Model)

2 3 4 5

1 A reasoning trace M is a function from the set of natural numbers (IN) to IS such that for all i 2 IN: (a) Mi Mi+1 (b) Mi = Mi+1 ) Mi = Mj for all j i. The re nement ordering on reasoning traces is de ned by: M N , Mi Ni for all i 2 IN. T The limit model , lim M of a reasoning trace M is de ned by lim M = 1 Mi . i=0 A reasoning trace M is sometimes denoted by (Mi )i2IN . A reasoning trace is called nitely generated if each Th(Mi) is nitely generated over Th(M0), i.e., if Th(Mi) = Cn(Th(M0 ) f i g) for some formulae i .

Since we assume a countable language L, each theory can be approximated by a chain of nitely generated theories. Therefore:

Proposition 2.1.

1 For any reasoning trace its limit is an information state (in particular, it is non-empty). 2 Any information state is the limit model of a nitely generated reasoning trace.

A (nonmonotonic) type of reasoning can now be described by giving its intended reasoning traces. Given a set of initial formulae, there may of course be several traces leading to di erent conclusion sets. We do, however, assume that the reasoning is deterministic in the sense that given the set of initial formulae and the nal conclusion set, the trace between them is uniquely determined. This can be explained in the sense that at each stage of the reasoning process all conclusions that possibly can be drawn, actually are drawn in the next step. Moreover, we do not allow two distinct traces leading to limit models of which one is a re nement of the other (non-inclusiveness of traces).

Definition 2.3. (Reasoning Frame)

1 A reasoning frame is a tuple (L; Mod; j=; T ) with T a set of reasoning traces such that for all M and N in T : if M0 = N0 and lim M lim N then M = N . For shortness, sometimes we also call T by itself a reasoning frame. 2 If for all sets of formulae X there exists a trace M in T such that Th(M0) = Cn(X ) then T is called a complete reasoning frame. Otherwise it is called partial. In the complete case the mapping sending every X L to the set of traces fM 2 T j

4

J. Engelfriet and J. Treur

Th(M0) = Cn(X )g is called the reasoning trace operator related to the reasoning

frame T .

The requirements of conservativity, determinism and non-inclusiveness only talk about the traces from a given set of initial facts. This certainly does not rule out nonmonotonicity: if the set of initial facts grows, the limit models of the traces that start with these initial facts need not increase (and may even decrease). So any form of nonmonotonic reasoning in which conclusion sets are constructed by stepwise increasing the initial facts, conclusion sets for a given set of initial facts are non-inclusive, and given the initial facts and a conclusion set there is only one possible trace, can be modelled by a reasoning frame. As an example we consider default logic:

Example 2.1. (Default Logic) Let D be a set of defaults. For X

L let E (hX; Di) denote the set of (Reiter) extensions of the default theory hX; Di. For a given X and E 2 E (hX; Di) the following reasoning trace M can be associated in a canonical manner: Mi = Mod(Ei ) with E0 = Cn(X ), and for all i 0, Ei+1 = Cn(Ei f! j ( : )=! 2 D is applicable at level i g), where a default ( : )=! 2 D is applicable at level i if 2 Ei and : 62 E . Note that this is a trace de nition based on the given set of defaults D. If we take the set of all these reasoning traces for E 2 E (hX; Di) we get a partial reasoning frame associated to hX; Di. Taking the union of these frames for all X L we get a complete reasoning frame associated with the set of defaults D.

A simple observation allows us to nd a natural description language for reasoning traces: the steps in a reasoning trace can be viewed as temporal steps. This means that the transition from an information state to the next one (as the result of a number of inference steps) can be seen as a temporal one. In this view a trace is a temporal model based on the set of natural numbers as the ow of time. An obvious candidate for describing these models is (some variant of) temporal epistemic logic. However, the full (tense) logic will turn out to be not completely appropriate: on the one hand it can describe models which are not traces but on the other hand it is not powerful enough. Therefore we will introduce a limited fragment of in nitary tense epistemic logic.

Definition 3.1. (Temporal Epistemic Model)

3. A Temporal Speci cation Language for Reasoning Frames

2 3 4 5

1 A temporal epistemic model is a function M : IN ! IS . A temporal epistemic model M is conservative if Mi Mi+1 for all i 2 IN. The re nement ordering on temporal epistemic models is de ned by: M N , M0 = N0 and for all i : Mi Ni : The limit model, limT , of a temporal epistemic model M is the information state M de ned by lim M = 1 Mi i=0 A temporal epistemic model M is sometimes denoted by (Mi )i2IN .

Note that the notion of a temporal epistemic model as such is close to the notion of a reasoning trace: any reasoning trace can be considered a conservative temporal model with the property that if it stabilizes one step, then it stabilizes forever. However, in a temporal epistemic model temporal operators and temporal formulae are interpreted. The temporal language we will use is a modal propositional language with the operators

Executable Temporal Logic for Nonmonotonic Reasoning

5

the agent believes (has derived) ". The truth of a formula in a temporal epistemic model M at time point i, denoted as (M; i) j= is de ned inductively:

Definition 3.2. (Temporal Interpretation)

F , G, C , H0 and in nite conjunctions and disjunctions. An epistemic operator is implicit in these temporal operators: for instance F means that sometimes in the future the reasoning agent will believe (or have derived) . Furthermore, C stands for \currently

1 For a propositional formula : (M; i) j= , Mi j= For a formula : (M; i) j= F , there exists j 2 IN; j > i such that (M; j ) j= (M; i) j= G , for all j 2 IN with j > i : (M; j ) j= (M; i) j= C , (M; i) j= (M; i) j= H0 , (M; 0) j= For a temporal formula : (M; i) j= : , it is not the case that (M; i) j= For a set V of temporal formula: A (M; i) j= A , for all 2 A : (M; i) j= A formula is true in a model M, denoted M j= , if for all i 2 IN: (M; i) j= A set of formulae T is true in a model M, denoted M j= T , if for all 2 T; M j= . We call M a model of T .

2

3 4 5 6

Furthermore the connectives _ and ! are introduced as the usual abbreviations. Note that for a propositional formula , C : is not equivalent to :C : C : means that the agent currently believes : , whereas :C means that the agent currently does not believe . The C -operator acts like the K -operator in epistemic logic: neither nor : needs to be true, but always either C or :C is true. The temporal language we have just introduced is still too powerful: we want to use only a fragment to describe models which can be seen as reasoning traces. So the question is: which fragment is appropriate for nonmonotonic reasoning? As steps in a reasoning process are taken whenever a number of (nonmonotonic) inference steps is used, it seems that temporal rules should prescribe taking the equivalent of (nonmonotonic) inference steps in the temporal model. So the next question is what the nature is of a generalized nonmonotonic inference step that a reasoning process can execute. A general format of (temporal) inference rules is ! G where is a condition for the inference, and is its conclusion: if the condition is ful lled, the conclusion can be drawn, and will be believed henceforth. The condition may of course include reference to the initial facts and the facts which have been derived earlier (and therefore are still true at the present moment). But in nonmonotonic reasoning there is often also a kind of global consistency check. In default logic for instance, a rule is applicable if certain formulae, called the justi cations, are consistent with the nal outcome of the reasoning process (called an extension), which means they should be consistent throughout the entire reasoning process. Consistency of a formula usually means that its negation should not be true. Therefore we also allow conditions which state that a certain formula should never (in the future of the reasoning process) be true.

Definition 3.3. (Reasoning Theories)

1 A formula is called a (nonmonotonic) reasoning formula if it is of the form ^ ^ ^ ! G ; where V = fH0 j 2 Ag for a set of propositional formulae A:

6

J. Engelfriet and J. Treur

= Vf:H0 j 2 B g for a set of propositional formulae B: = Vf:F j 2 Dg for a set of propositional formulae D: = fC j 2 F g for a set of propositional formulae F: is a propositional formula: A reasoning formula is called nitary if all sets of formulae involved are nite; otherwise it is called in nitary. 2 A set Th of reasoning formulae is called a theory of reasoning. It is called nitary if all its elements are; otherwise it is called in nitary. So a reasoning formula prescribes the truth of a formula in the future based on knowledge of initial facts, truth of current facts and consistency of facts in the future (if :F is true, then is never believed in the future, so : remains consistent with the agent's beliefs throughout the future).

Definition 3.4. (Conservativity) The theory Cons = fC ! G j a propositional formula g is a theory of reasoning expressing conservativity of temporal models.

V

A theory of reasoning prescribes that certain formulae have to be believed (derived) in the future, analogously to inference steps. But what about facts which become known at a point in time spontaneously, that is without any inference rule prescribing their truth? We should have a way to make sure that this does not happen: we want the models to have minimal information in the sense that nothing becomes known if there are no rules saying so (see also (Shoham, 1988), (Kraus, Lehmann and Magidor, 1990)). This leads to the following notion of minimal models:

Definition 3.5. (Minimal Temporal Models) A temporal epistemic model

M is called a minimal model of a theory Th if it is a model of Th and for any model N of Th, if N M then N = M.

A minimal model of a theory is a model for which there are no smaller models of the theory, so they contain a minimum of information. Given the fragment of temporal logic we have de ned, a natural property to investigate is whether this fragment is suited for describing reasoning traces. From now on we will assume that any theory includes the theory Cons described in De nition 3.4. The rst result is that all minimal models of any theory are reasoning traces. On the other hand, any reasoning frame is the set of minimal models of a theory of reasoning:

Theorem 3.1.

1 For any theory of reasoning Th its minimal models constitute a (partial) reasoning frame. 2 For any (partial) reasoning frame T there exists a theory of reasoning whose minimal models are exactly T . If there is only a nite number of atomic proposition symbols, then this theory of reasoning can be taken nite and nitary.

Now we give an explicit theory of reasoning for the reasoning frame associated with a default theory as described in Example 2.1 (see (Engelfriet and Treur, 1993)):

Example 3.1. (Default Logic) Given a default theory

= hX; Di, de ne its theory of reasoning T ( ) by: T ( ) = fC ^ :F : ! G j ( ; )= 2 Dg fC j 2

Executable Temporal Logic for Nonmonotonic Reasoning

7

X g Cons. Then the minimal models of T ( ) constitute the partial reasoning frame associated to . Each minimal model of T ( ) corresponds with an extension of .

Any form of nonmonotonic reasoning which can be modeled by a reasoning frame (thus any form satisfying conservativity, determinism and non-inclusiveness), can be described by a theory of reasoning. The question arises whether this theory can always be chosen nite. For deafult logic, this is the case if the default theory is nite. In order to execute a theory of reasoning we interpret its temporal rules as inference rules. If the condition of such a rule is met, we introduce its conclusion at the next step. The condition of the rule pertaining to the initial facts and the present can be checked in a straightforward manner. The only problem are the consistency checks. The way to deal with them is to: a) either assume they will be met and add the conclusion. In this case we will have to check at all later steps that they are still met. b) Otherwise we assume they are not met and do not add the conclusion. In this case the consistency must be violated at some later time. If this does not happen than the execution is not correct. If the theory of reasoning is in nite, it is in general not possible at any point in time to be sure we are executing correctly. Notice that a reasoning formula is not of the form \PAST implies FUTURE", a form used often for executable temporal logic (see (Gabbay, 1989)). Of course we could move the consistency checks to the right of the implication. Using the notation of De nition 3.3 W we would obtain a rule ^ ^ ! G _ fF j 2 Dg, which is clearly in the desired format. To execute this rule if the conditions are met, we could either introduce at the next moment in time, or introduce one of the elements of D at any future time point. But this is not the correct way of executing such a formula, since the consistency checks are meant to be declarative and not imperative. So instead of the slogan \declarative past implies imperative future" (Gabbay, 1989) we use the slogan \declarative past and future imply imperative future". We will now informally describe the general algorithm for executing a theory of reasoning Th. We assume that we have a set of initial facts.

Algorithm 4.1.

4. Executing Theories of Reasoning

1 Mark all rules as unused, set t to 0. 2 If the current facts are contradictory, backtrack to the previous time point. 3 Check all constraints never true( ). If is entailed by the current facts, backtrack to the previous time point. 4 For each unused rule ^ ^ ^ ! G ; where V = VfH0 j 2 Ag for a set of propositional formulae A; = Vf:H0 j 2 B g for a set of propositional formulae B ; = Vf:F j 2 Dg for a set of propositional formulae D; = fC j 2 F g for a set of propositional formulae F ; is a propositional formula; do: If all formulae in F are entailed by the current facts, and all formulae in A are entailed by the initial facts, and all formulae in B are not entailed by the initial facts then this rule is applicable: mark this rule as used and do either of:

8

J. Engelfriet and J. Treur

introduce next( ) and constraints never true( ) for each 2 D, or introduce constraints sometimes true(D). If we backtracked to this time point, make a choice for all the applicable rules at this time point which has not been made before. If this is not possible, backtrack one more step. If this is not possible (t = 0) then abort. 5 t := t + 1; for each formula next( ), introduce and delete next( ); If there are no formulae next( ), check for each constraint sometimes true(D) whether some 2 D is entailed by the current facts; if not, backtrack one step; Goto 2. If for all constraints sometimes true(D), some 2 D is entailed by the facts at some point in time, the execution of the algorithm is called correct.

As mentioned before, if at each step new formulae are added, we can never be sure during execution, if the execution will be correct. However in case the theory of reasoning is nite, there will be a point in time when no new facts are added: then the execution will always be correct. This is always the case when the propositional language contains a nite number of atoms: then there is a nite number of non-equivalent propositional formulae; if this number is n, then after n steps of the algorithm, no new facts can be added. For correct executions we have the following:

for Th, let Ti denote the set of propositional formulae derived at time t = i. De ne a reasoning trace (Mi )i2IN by Mi = Mod(Ti ). Let T be the set of these traces for all possible correct executions of the algorithm for Th. Then T is exactly the set of minimal models of Th.

Theorem 4.1. Let a theory of reasoning Th be given. For an execution of the algorithm

So in the case of a nite theory of reasoning, our algorithm can construct precisely its minimal models. Since any reasoning process described by a reasoning frame has a theory of reasoning describing it, which can be executed by our algorithm, we have a general algorithm for executing these processes. Applying this algorithm to the theory of reasoning of a default theory, we obtain an algorithm very similar to the ones meant especially for default logic: it picks a subset of so-called generating defaults, and checks whether it indeed induces an extension. Using this algorithm to obtain either one or all of the minimal models of a theory of reasoning, one can verify various properties of the reasoning process described by the theory of reasoning. For instance it can be checked whether a certain formula is derived in one or in all possible runs. Thus for nonmonotonic reasoning processes, sceptical and credulous entailment can be calculated. It can be shown (using the above algorithm) that the complexity of sceptical entailment using theories of reasoning is complete in QP . This is the complexity of sceptical entailment of many nonmonotonic formalisms 2 like autoepistemic logic, McDermott and Doyle's nonmonotonic logic and nonmonotonic logic N (see (Engelfriet, 1995)). A special class of theories of reasoning is obtained when we do not allow consistency checks (the set D in De nition 3.3 is empty). The induced reasoning process will then be monotonic, and the algorithm will be much more e cient. In speci c instances of theories of reasoning one would like to make the algorithm more e cient. This can be done by using heuristic knowledge to make smart choices at each point in time. In particular, if at the current point in time one of the 2 D is already

Executable Temporal Logic for Nonmonotonic Reasoning

9

entailed by the facts, only the second choice in the algorithm makes sense. In the case of default logic, one could use priorities between default rules or speci city of rules to restrict the number of possible choices (see (Brewka, 1994)). The set of possible runs of our algorithm can be parameterized by selection functions. Such functions describe the choices which have to be made at each point in time (in a similar fashion as in (Tan and Treur, 1992)). Then the \good" selection functions make use of heuristic knowledge to guide the reasoning process.

The formalism of temporal logic is used to specify and verify processes in general. If a class of processes can be speci ed accurately by a form of temporal logic which can be executed, we have a general execution mechanism for this class. In this paper we studied the class of nonmonotonic reasoning processes (see also (Engelfriet, Herre and Treur, 1995), (Engelfriet and Treur, 1996)). These processes can be described semantically by the reasoning traces they produce. Viewing these traces as temporal models, they can be speci ed by temporal rules. We have shown that a fragment of in nitary temporal epistemic logic is suitable for describing any set of traces (see (Engelfriet and Treur, 1993) and (Engelfriet and Treur, 1994) for speci cations of a number of speci c types of nonmonotonic reasoning). In the (important) case when the signature is nite we have given an algorithm which can execute any speci cation of reasoning. Although the execution of temporal rules is similar to existing executable temporal logics, the consistency checks are treated di erently. They are treated as declarative tests in the future, not as imperative commands for the future. The most important di erence between our framework for nonmonotonic reasoning and the framework developed by Shoham, Kraus, Lehmann, Magidor, Makinson and others (see e.g. (Kraus, Lehmann and Magidor, 1990), (Shoham, 1988)) is that we explicitly also want to model the dynamics of reasoning, whereas the other approaches only focus on the static aspects, namely the initial facts and the conclusions. As our speci cation language describes reasoning processes, a natural question to investigate is whether it is possible to nd a generic meta-level architecture capable of executing speci cations of reasoning. In such an architecture, the meta-level should check the rules for applicability and select the conclusions to be added at the object-level. Heuristic knowledge at the meta-level can be used to control the selection of conclusions. There should be an easy and natural way to translate speci cations of reasoning into rules to be used by this architecture, thus instantiating the generic architecture. Speci cation languages for such meta-level architectures can be found in the research on formal speci cation languages for complex reasoning systems (see (Treur and Wetter, 1993)). One of these languages is DESIRE (see also (Langevelde, Philipsen and Treur, 1992), (Gavrila and Treur, 1994)); in (Tan and Treur, 1992) it is shown how DESIRE can be used to specify a reasoning system creating nonmonotonic reasoning patterns. Here explicit control knowledge is (required to be) added at the meta-level; this control knowledge speci es a selection function on (possible) default conclusions. The software environment supporting DESIRE provides (automatically generated) implementation code (PROLOG code that can be executed).

5. Conclusions and Further Research

10

J. Engelfriet and J. Treur

Part of this work has been supported by the ESPRIT III Basic Research project 6156 DRUMS II. Discussions with Heinrich Herre have played a stimulating role in developing part of the material in this paper.

Gabbay, D. (1989). The Declarative Past and Imperative Future: Executable Temporal Logic for Interactive Systems. In: B. Banieqbal, H. Barringer, A. Pnueli (eds.), Temporal Logic in Speci cation, Lecture Notes in Computer Science, Vol. 398, Springer-Verlag, 409{448. Brewka, G. (1994). Adding Priorities and Speci city to Default Logic. In: C. MacNish, D. Pearce, L.M. Pereira (eds.), Logics in Arti cial Intelligence, Proceedings of the 4th European Workshop on Logics in Arti cial Intelligence, JELIA'94, Lecture Notes in Arti cial Intelligence, Vol. 838, Springer-Verlag, 247{ 260. Engelfriet, J., Herre, H., Treur, J. (1995). Nonmonotonic Belief State Frames and Reasoning Frames (extended abstract). In: C. Froidevaux, J. Kohlas (eds.), Symbolic and Quantitative Approaches to Reasoning and Uncertainty, Proc. ECSQARU'95, Lecture Notes in Arti cial Intelligence, Vol. 946, Springer-Verlag, 189{196. Engelfriet, J. (1995). Minimal Temporal Epistemic Logic. Technical Report IR-388, Department of Mathematics and Computer Science, Vrije Universiteit Amsterdam. To appear in Notre Dame Journal of Formal Logic. Engelfriet, J., Treur, J. (1993). A Temporal Model Theory for Default Logic. In: M. Clarke, R. Kruse, S. Moral (eds.), Proc. 2nd European Conference on Symbolic and Quantitative Approaches to Reasoning and Uncertainty, ECSQARU '93, Lecture Notes in Computer Science, Vol. 747, Springer-Verlag, 91{96. Extended version: Report IR-334, Vrije Universiteit Amsterdam, Department of Mathematics and Computer Science, 1993. Engelfriet, J., Treur, J. (1994). Temporal Theories of Reasoning. In: C. MacNish, D. Pearce, L.M. Pereira (eds.), Logics in Arti cial Intelligence, Proceedings of the 4th European Workshop on Logics in Arti cial Intelligence, JELIA'94, Lecture Notes in Arti cial Intelligence, Vol. 838, Springer-Verlag, 279{ 299. Also in: Journal of Applied Non-Classical Logics 5(2), 1995, 239{261. Engelfriet, J., Treur, J. (1996). Speci cation of Nonmonotonic Reasoning. To appear in: Proceedings of the First International Conference on Formal and Applied Practical Reasoning, FAPR'96, SpringerVerlag. Fisher, M. (1994). A Survey of Concurrent METATEM - The Language and its Applications. In: D.M. Gabbay, H.J. Ohlbach (eds.), Temporal Logic, Proceedings ICTL'94, Lecture Notes in Arti cial Intelligence, Vol. 827, Springer-Verlag, 480{505. Fisher, M., Owens, R. (eds.) (1995). Executable Modal and Temporal Logics, Proceedings of the IJCAI'93 workshop, Lecture Notes in Arti cial Intelligence, Vol. 897, Springer-Verlag. Gavrila, I.S., Treur, J. (1994). A formal model for the dynamics of compositional reasoning systems. In: A.G. Cohn (ed.), Proc. 11th European Conference on Arti cial Intelligence, ECAI'94, Wiley and Sons, 307{311. Kraus, S., Lehmann, D., Magidor, M. (1990). Nonmonotonic Reasoning, Preferential models and cumulative logics. Arti cial Intelligence 44, 167 { 207. Langevelde, I.A. van , Philipsen, A.W., Treur, J. (1992). Formal Speci cation of Compositional Architectures. In: B. Neumann (ed.), Proceedings of the 10th European Conference on Arti cial Intelligence, ECAI'92, John Wiley & Sons, Chichester, 272{ 276. Marek, V., Truszczynski, M. (1993). Nonmonotonic Logic, Springer-Verlag. Orgun, M.A., Ma, W. (1994) An Overview of Temporal and Modal Logic Programming. In: D.M. Gabbay, H.J. Ohlbach (eds.), Temporal Logic, Proceedings ICTL'94, Lecture Notes in Arti cial Intelligence, Vol. 827, Springer-Verlag, 445{479. Shoham, Y. (1988). Reasoning about Change, MIT Press. Tan, Y.H., Treur, J. (1992). Constructive Default Logic and the Control of Defeasible Reasoning. In: B. Neumann (ed.), Proc. 10th European Conference on Arti cial Intelligence, ECAI-92, Wiley & Sons, 299{303. Treur, J., Wetter, Th. (eds.) (1993). Formal Speci cation of Complex Reasoning Systems, Ellis Horwood. Voorbraak, F. (1993). Preference-based Semantics for Nonmonotonic Logics. In: Bajcsy, R. (ed.), Proc. 13th International Joint Conference on Arti cial Intelligence, IJCAI-93, Morgan Kaufmann, 584{ 589.

Acknowledgments

References