=Paper= {{Paper |id=Vol-136/paper-4 |storemode=property |title=Modelling Assumption-Based Reasoning Using Contexts |pdfUrl=https://ceur-ws.org/Vol-136/136.pdf |volume=Vol-136 }} ==Modelling Assumption-Based Reasoning Using Contexts== https://ceur-ws.org/Vol-136/136.pdf

Modelling Assumption-Based Reasoning
Using Contexts

Mark Jago?
School of Computer Science & Department of Philosophy
University of Nottingham
Nottingham, UK
mtw@cs.nott.ac.uk

Abstract. We propose a two-fold use of context in reasoning about agents. The
first concerns the modelling of beliefs which are entertained only within the scope
of some assumption. We illustrate this use by describing as logical model of an
agent which reasons in a natural deduction style by making assumptions to derive
new formulas. The second use of context we propose here concerns the modelling
of reasoning as a step-by-step temporal process, allowing us to model agents
whose resources are temporally bounded. In such a setting, the beliefs ascribed
to an agent need not be closed under consequence, as they are in many traditional
epistemic logics.

1 Introduction

This essay is concerned with the modelling of agents who make assumptions
and use them in their deductive reasoning. This work differs form other formal
accounts of contextual reasoning in that it deals with resource bounded agents,
namely agents which requires computational resources to deduce new beliefs
from old. We take as an illustration an agent who reasons in a natural deduction
style, but who takes time to reach its conclusions.
We treat an assumption as a sentence entertained by an agent for a particular
purpose. An assumption is not a belief, yet has the psychological effect of a
belief whilst the assumption is entertained. In assuming a formula, one reasons
and behaves as if it were the case (this is, then, something like the psychological
notion of pretence).
We use the notion of context to model this process of making assumptions.
Following [4], a context is a localised set of beliefs, connected to other con-
texts by inter-context bridge rules. Each context represents the epistemic con-
sequences of an act of pretence (i.e., of assumption making) on behalf of the
agent; for example, the context in which an agent makes the assumption that
?
This research is supported by the AHRB. Thanks to Natasha Alechina, Thorsten Altenkirch,
Brian Logan and Sieuwert van Otterloo for commenting on earlier drafts of the paper.
the moon is made of green cheese contains the sentences that the agent would
believe, were it to consider that assumption to be true.
Contexts are a suitable tool for this purpose as they can be embedded, thus
allowing one to model the making of assumptions within assumptions. In the
single agent setting of this paper, we reserve one special context, the empty
context, as a model of the agent’s actual beliefs, i.e. those sentences entertained
with no assumption whatever. In a more general multi-agent setting, we will
have a unit context for each agent i, corresponding to each agent i’s assumption-
free beliefs.
We should perhaps point out that this is a different use of the term context
from that which most frequently appears in the philosophical literature, which
denotes certain aspects of the world (an example is Kaplan’s [5] use of such
contexts in his analysis of pure indexicals). Here, contexts are comprised of
psychological entities (which may be thought of as specific concepts, sentences
of an internal language of thought or “mentalese”, . . . ).
We argue that epistemic logics which utilise traditional possible worlds
semantics are not suited to this kind of contextual reasoning. An agent may
well assume a formula which contradicts its current beliefs; indeed, this is the
essence of drawing conclusions by reductio ad absurdum. However, traditional
epistemic logics based on classical consequence relations become trivial in the
presence of such inconsistencies. This suggests a paraconsistent approach. Para-
consistent logics feature in epistemic frameworks that make use of impossible
possible worlds, such as Levesque’s logic of explicit and implicit belief.
However, we also wish to model resource bounded agents; we are particu-
larly interested in agents which take time to reach their conclusions. We should
therefore avoid what Perlis et al [3, p.1] call a “final tray approach” to mod-
elling an agent’s beliefs, which tells us what an agent will eventually believe,
given its initial beliefs and the rules it reasons with, but may not at a particular
point during that reasoning process.
While such approaches are applicable in many situations, there are cases
in which a primary point of the model is to determine whether the agent can
reach a given conclusion in a period of time. We may cite examples such as
verifying security protocols and modelling the behaviour of theorem provers. In
our example we discuss an who reasons in a natural deduction style, producing
one new formula at a time. If we were to assume the synchronous deductive
closure of an agent’s beliefs within any context then our agent would be able to
reach all conclusions that is possibly could immediately; this defeats the point
of modelling, which is to establish whether such an agent could reach a certain
conclusion in a set time.
2 Introducing Timed Reasoning Logics
We take an approach which differs from traditional possible worlds-based epis-
temic logics. We take a belief to be part of the internal state of an agent, which al-
lows it to act given the appropriate desires and intentions (i.e., goals and plans).
We represent the internal state of an agent as a finite set of sentences in some
logical language. Whilst we are primarily thinking of rule-based agents, we can
accommodate other styles of agent programming by providing a translation of
values for program variables into logical formulas, for example. We take as our
model of an agent a function which describes how the agent’s beliefs change
from one deductive cycle to the next. Given a set of initial beliefs, we get a se-
quence of sets of sentences, each set representing the internal state of the agent
at that point in time (figure 1).

beliefs inf beliefs inf beliefs inf beliefs
- - - ...
at t = 1 at t = 2 at t = 3 at t = 4

Fig. 1. Timeslices

We refer to each such set at a timeslice. In addition to modelling how the
agent’s actual beliefs evolve over a period of time, we can model the beliefs it
would come to in the hypothetical circumstance of believing some formula φ.
We term these the agent’s φ-beliefs and we say they constitute the φ-context.
We combine our model with a partitioning of the agent’s internal state (at a
moment of time) into contexts. This allows us to separate the agent’s beliefs en-
tertained under different assumptions, and thus to model multiple assumptions
concurrently. The context containing the sentences that would eventually be be-
lieved if φ were to be believed provides our model of assuming that φ is the
case. By placing a total ordering on assumptions that can be made, we can view
these contexts as a sequence. Since each context corresponds to assuming some
formula, such an ordering simply amounts to a total order on formulas. Since
assumptions can be made within assumptions, we can have contexts within con-
texts, as shown in figure 2.
We arrive at a model consisting of a grid of sets of sentences, with rows
representing assumption contexts and columns representing timeslices of those
contexts, as shown in figure 3.
We use a labelled language Ltrl whose syntax is suited to describing such
models. We make use of a set of context letters C and a set of timeslice labels
φ1 φ2 - φ2 φ3
beliefs beliefs beliefs

I
@

actual
beliefs

Fig. 2. Embedding contexts
t=1 t=2 t=3

assumption 2 - - - ...

assumption 1 - - - ...

actual beliefs - - - ...

Fig. 3. Model of an agent

T . Each context is labelled with a finite sequence c̄ = hc1 , . . . , cn i where each
ci≤n ∈ C (i.e. context labels are words whose alphabet is C). We denote the set
of all context labels by C ∗ . For convenience, we write c̄k to denote the result of
concatenating some k ∈ C to a sequence c̄ ∈ C ∗ .
Suppose the agent we are modelling derives formulas in a propositional lan-
guage L over ¬, ∧, ∨ and →. Well-formed formulas of Ltrl then consist of a
label l, which describes both a context at a timepoint and a body which is a
formula taken from the agent’s language L. A label l is written as a pair (c̄, t)
where c̄ ∈ C ∗ and t ∈ T (where c̄ is some sequence c1 , . . . , cn ). Well formed
Ltrl formulas are thus of the form (c̄, t) : φ. We assume that T is totally ordered;
for our purposes, we can take T to be the set of natural numbers. We write rules
connecting contexts and timeslices in the style of natural deduction inference
rules as follows:

(c̄, t) : φ1 . . . (c̄0 , t) : φn
(c̄00 , t + 1) : ψ
Here, c̄, c̄0 , c̄00 are variables ranging over contexts, t ranges over timeslices and
φ1 , . . . , φn , ψ range over well formed formulas of the agent’s language L. Note
that, while each φi≤n and ψ may belong to a distinct context, rules always con-
nect a timeslice t of the relevant context to the successor timeslice t + 1. Thus,
all rules conform to the step logic paradigm, i.e., the idea of modelling inference
as a step-by-step process.

3 Modelling a Natural Deduction Style Reasoner

In this section, we introduce as a working example an agent which reasons in
a natural deduction style. Such an agent is required to make and later cancel
assumptions in order to derive new formulas. Our aim is to model this process
using contexts connected by assumption rules, similar to the bridge rules of
context logic). Moreover, we model the agent’s deliberation as a step-by-step
process of rule application. We again use contexts to represent this process, this
time connected by temporal rules, similar to the rules of step logic [3].
We thus make a dual use of the notion of context to represent both temporal
and assumption information. It is important to note that contexts representing
assumptions and contexts representing temporal states are not distinct; rather,
each context represents both temporal information and information about as-
sumptions. A third use of contexts would be to use distinct contexts to represent
different agents. Although we do not pursue this interpretation here, the formal
apparatus it requires is already present in the logical framework we present in
section 5 below.
We begin by looking how temporal rules relate timeslices. Intuitively, each
timeslice label t ∈ T corresponds to a timepoint in a linear, non-branching
temporal structure and the timeslice labelled by t contains the beliefs of our
agent at that time (within some context). As a convenient shorthand, we will
often write t + 1 to denote the successor of t, although we assume no need for
arithmetical operations. Temporal rules may connect a timeslice labelled with t
to one labelled with t0 only when t < t0 . This respects the fact that causation,
as a matter of metaphysical necessity, is forwards causation and thus our agent
can only reason forwards in time.
Simple operations that our agent can perform from one timeslice to the next
include: ∧-introduction and elimination, ¬¬-elimination and ∨-introduction.
These inferences are simple as they operate on formulas in a single context.
Example temporal rules are listed below:

(c̄, t) : φ (c̄, t) : ψ (c̄, t) : φ ∧ ψ
∧int ∧
(c̄, t + 1) : φ ∧ ψ (c̄, t + 1) : φ elimL
(c̄, t) : φ ∧ ψ (c̄, t) : ¬¬φ
∧ ¬
(c̄, t + 1) : ψ elimR (c̄, t + 1) : φ elim
To illustrate how these temporal rules connect timeslices, figure 4 below shows
an agent’s beliefs evolving from φ ∧ ¬¬ψ at some time t:

t t+1 t+2

φ ∧ ¬¬ψ φ ∧ ¬¬ψ
φ ∧ ¬¬ψ - -
φ, ¬¬ψ φ, ¬¬ψ, ψ

Fig. 4. Temporal rules

It is important to note that the formulas which hold at a timeslice only do so
on the basis their appearing in the consequent of some rule. In particular, there
is nothing inherently monotonic about the Timed Reasoning framework being
described here. ∧int tells us, for example, that φ ∧ ψ will be a t + 1-formula
when φ and ψ are both t-formulas but we have not said whether φ or ψ are
themselves t + 1 formulas. It may be the case, for example, that each timeslice
(of a particular context) may only contain a fixed number of formulas, due to
an agent’s memory restrictions. Such a case would clearly be nonmonotonic;
that is, Γ ` φ would not ensure that Γ ∪ ∆ ` φ for any sets of formulas Γ, ∆
and formula φ, for formulas derived from ∆ might take up space in some future
timeslice required to store formulas of Γ . However, since we require the natural
deduction agent we present here to reason monotonically, we need to add an
extra temporal rule to ensure just that:
(c̄, t) : φ
MON
(c̄, t + 1) : φ
We now introduce assumption contexts and the corresponding bridging rules,
which we will refer to as assumption rules. We take as our examples reasoning
by reductio ad absurdum and →-introduction, as both require a reasoner to make
an assumption which is later withdrawn. To begin with, consider using reductio
ad absurdum to derive ¬(φ ∧ ¬φ); one first assumes φ ∧ ¬φ, derives each con-
junct using ∧-elimination and, on noting the contradiction, establishes that the
assumed formula cannot be the case.
We use contexts to model the making of assumptions: formulas entertained
within that context are thus those within the scope of the corresponding as-
sumption. It is therefore useful to label such contexts with the assumptions they
correspond to, i.e., the very formula assumed in making the assumption. Thus,
we take C, our set of context symbols, to be L, the internal language of our
agent. Contexts are thus labelled with sequences of well formed formulas of L.
We denote the empty context by ·.
We must ensure that, when a formula φ features in a context label c̄, that φ
also appears as a formula in that context. In addition, we must make sure that
c̄ formulas are also c̄0 formulas whenever c̄ is a subsequence of c̄0 . This is so
we respect the fact that we may use the formulas holding in a context c̄ in any
context which we opened from within c̄:
(c̄1 , t) : φ
(where φ ∈ c̄) CON INHERIT
(c̄, t) : φ (c̄2 c̄1 c̄3 , t + 1) : φ
Embedded contexts are represented as sequences read left-to-right, thus if
the sequence hφ, (ψ ∨ χ)i were used to label a context, that context would rep-
resent the agent as having assumed φ and then, within the scope of that assump-
tion, assuming ψ ∨χ as well. As mentioned above, c̄φ denotes the concatenation
to the right of φ to c̄ (where c̄ is some context label). Thus, c̄φ can be used to
label the context which represents the agent assuming φ from the c̄-context. We
may then write a rule for reduction ad absurdum as follows:

(c̄φ, t) : χ, (c̄φ, t) : ¬χ
¬int
(c̄, t + 1) : ¬φ

We may read this rule as saying: having assumed φ from a context c̄ and having
derived a contradiction (i.e., some formula χ and its negation) in c̄φ, we may
infer ¬φ in c̄ at the next timeslice. Figure 5 shows how we model an agent using
reductio ad absurdum to derive ¬(φ ∧ ¬φ).
An agent derives an implication in much the same way. Having assumed φ
in a context c̄ and having then derived ψ, one may infer φ → ψ in the original
context c̄ at the next timeslice:

(c̄φ, t) : ψ
→
(c̄, t + 1) : φ → ψ int

Figure 6 below shows a model of an agent deriving φ → (ψ → φ) (formulas of
the form φ ∧ φ have been left out of the diagram to save space).

4 Adequacy of the Model

We now show that our framework is adequate as a model of the natural deduc-
tion agent we have described in that, for any propositional formula derivable in
standard natural deduction, there is a corresponding labelled formula derivable
using our labelled logic. Recall that “·” is a context label which denotes the
φ∧¬φ, φ∧¬φ,
hφ∧¬φi φ ∧ ¬φ - -
φ, ¬φ φ, ¬φ
@
R
@
h·i - - ¬(φ∧¬φ)

Fig. 5. Reductio ad absurdum

φ, ψ φ, ψ
hφψi φ, ψ - -
φ∧ψ φ∧ψ
Q
s
Q
ψ → φ, φ
hφi φ - ψ → φ, φ -
(ψ → φ)∧φ
Q
s
Q
h·i - - φ → (ψ → φ)

Fig. 6. → introduction

empty context and that the formulas appearing in a context label represent as-
sumptions used to derive the formulas which hold in that context. Thus, formu-
las which hold in · at some timepoint t hold with no assumptions being made. If
we think of formulas holding in a context c̄ to be what the agent’s beliefs would
be, were it to believe the formulas in c̄, then we may think of the formulas hold-
ing in · as the agent’s actual beliefs.
In this section, we will show that, for any (unlabelled) propositional formula
φ of the agent’s internal language L derivable from a set of (unlabelled) proposi-
tional formulas Γ using standard natural deduction rules, it is possible to derive
a labelled formula (·, t) : φ, for some timepoint t, from a labelled version of Γ .
We concentrate on an agent with an internal language L¬,∧ over ¬, ∧ and a set
of propositional letters P only (of course, the other connectives could be intro-
duced by definition in the usual way). We will refer to the set of bridge rules we
have introduced for these connectives, namely ∧int , ∧elimL , ∧elimR , ¬int and
¬elim , as well as the rules MON, INHERIT and CON, as R.

Definition 1 (Derivation). A labelled formula (c̄, t) : φ is derivable from a set
of labelled formulas Γ l using the rules in R, written Γ l `R (i, t) : φ, if there is
a sequence of labelled formulas (c̄1 , t1 ) : φ1 , . . . , (c̄m , tn ) : φk such that:
1. each formula in the sequence is either a member of Γ l , or is obtained from
Γ l by applying one of the bridge rules in R; and
2. the last labelled formula in the sequence is (c̄, t) : φ.

Let Γ be a set of unlabelled formulas and φ an unlabelled formula; we write
Γ `mp φ when φ can be derived from Γ using the usual rules of natural deduc-
tion. We now form a set of labelled formulas Γ l = {(·, 1) : φ | φ ∈ Γ } which
correspond to placing each φ ∈ Γ in the empty (i.e., assumption-free) context
at time 1.

Theorem 1. Let Γ be a set of unlabelled propositional formulas and φ be an
unlabelled propositional formula in the agent’s language L¬,∧ . Then Γ `nd φ
iff for some t, Γ l `R (·, t) : φ, where Γ l = {(·, 1) : ψ | ψ ∈ Γ }.

The proof can be found in [6]. a

Corollary 1. For any finite set of labelled formulas Γ l and a labelled formula
φl , it is decidable whether Γ l `R φl .

5 Semantics

In this section, we introduce a semantics with respect to which the rules R pre-
sented above are sound and complete. To establish completeness, we introduce
the notions of a sufficient model and of a minimal model. To keep notation uni-
form, we use φ, ψ to denote arbitrary unlabelled formulas and Γ to denote a set
thereof; the superscript l denotes labelled versions, e.g., φl and Γ l denote an
arbitrary labelled formula and a set thereof, labelled as described above.

Definition 2 (Models). Let Σ ⊂ L∗ be a finite set of finite sequences of formu-
las over L and inf be a function of type Σ −→ N −→ ℘(L). A model M is a
tuple hΣ, inf , {mc̄t | c̄ ∈ C ∗ , t ∈ N}i where:
1. each mc̄t is a finite set of formulas in L such that mc̄t+1 = inf (c̄, t)
2. inf satisfies:
φ1 ∧ φ2 ∈ mc̄t =⇒ φ1 , φ2 ∈ inf (c̄, t)
¬¬φ ∈ mc̄t =⇒ φ ∈ inf (c̄, t)
φ ∈ mc̄t =⇒ φ ∈ inf (c̄, t)
φ, ¬φ ∈ mc̄ψ t =⇒ ¬ψ ∈ inf (c̄, t)
φ ∈ c̄ =⇒ φ ∈ inf (c̄, t)
φ ∈ mc̄t =⇒ φ ∈ inf (c̄0 , t) where c̄0 = · · · c̄ · · ·
When a model M minimally (w.r.t. ⊆) satisfies these conditions, we say that it
is a minimal model.
Intuitively, inf (c̄, t) looks at a timeslice t and infers which formulas should be
in the context c̄ at the next timeslice.

Definition 3 (Satisfaction). We say a labelled formula of the form (c̄, t) : φ is
satisfied by a model M , written M |= (c̄, t) : φ, iff φ ∈ mc̄t .

Definition 4 (Validity and Entailment). A labelled formula φl is (i) Σ-valid,
written |=Σ φl iff M |= φl for all models M over Σ and (ii) a Σ-consequence
of a set of labelled formulas Γ l , written Γ l |=Σ φl , whenever φl is satisfied by
all models M over Σ which also satisfy every ψ l ∈ Γ l .

Since different derivations may rely on making different sequences of as-
sumptions, there is a special class of model, comprising only those that ensure
all such assumptions are represented. We call such models sufficient that par-
ticular derivation. Note that we could not simply assume that Σ contains all
possible sequences over L in models in this class, for this would allow the pos-
sibility of infinitely many formulas being introduced to a local state by the inf
condition, which would violate the definition of each mc̄t as a finite set. Instead,
we use the following definition of sufficiency:

Definition 5 (Sufficient Models). A model M is sufficient for a pair hΓ l , φl i
if either Γ l 0R φl or else there exists a derivation Γ l `R φl containing a
sequence of labelled formulas (c̄1 , t1 ) : φ1 , . . . , (c̄m , tn ) : φk and each c̄i≤m ∈
Σ ∈ M . Given a semantic sequent Γ l |=Σ φl , we say that Σ is sufficient (for
that sequent) iff every model M over Σ is sufficient for hΓ l , φl .i.

We can now establish that the rules R are sound and complete w.r.t. the seman-
tics just proposed. We begin by preparing the following lemma:

Lemma 1. Let M be minimal for Γ l and sufficient for hΓ l , (c̄, t) : φi. Then for
every formula φ, φ ∈ mc̄t iff Γ l `R (c̄, t) : φ.

Again, the proof can be found in [6]. a

Theorem 2 (Soundness & Completeness). There is a sufficient Σ such that
Γ l `R φl iff Γ l |=Σ φl .

Proof. Soundness is standard: clearly, the rules in R preserve validity. For com-
pleteness, suppose Γ l |=Σ φl . By definitions 2 and 5, there is a minimal model
M over Σ of Γ l such that M |= φl . By Lemma 1, Γ l `R φl . a

Corollary 2. φ is a classical consequence of Γ iff Γ l |=Σ (·, t) : φ for some t.

Corollary 3. It is decidable whether Γ l |=Σ φl .
6 Reasoning with Goals
Before we conclude, we briefly look at how the framework presented here can
incorporate goal-centered behaviour to avoid some of the indeterminacy re-
quired in choosing assumptions. The agent we have described so far is non-
deterministic in the sense that it begins by guessing which assumptions to make;
our model begins with the corresponding contexts and derives the consequences.
In this sense, we have a model of the consequences of making some assumption,
rather than a model of the reasons an agent may have for doing so.
To incorporate this latter notion, we can add goal contexts to our framework.
In the setting of our natural deduction reasoner, a goal context contains the for-
mula or formulas which the agent would like to try to derive. For example, if a
goal is to derive φ → ψ, one can begin by assuming φ. Within the φ-context,
one’s subgoal is to derive ψ. Thus, each context will have a goal context asso-
ciated with it. We can refine the behaviour of our model by introducing bridge
rules between goal contexts, labelled with a sequence ending in a unique goal
symbol G, and assumption contexts:
(c̄G, t) : φ → ψ (c̄G, t) : φ → ψ
(φ, t+1) : φ (c̄φG, t + 1) : ψ

(Note that the former replaces the earlier rule (c̄, t) : φ for φ ∈ c̄ and that the
INHERIT rule (section 3) must now only apply when neither context is a goal
context.)
We should stress, however, that this section is not intended as a full account
of a deterministic natural deduction theorem prover. It is offered as a demonstra-
tion of how propositional attitudes other than beliefs, such as desires (goals) and
intentions (plans) may be included within the Timed Reasoning Logics frame-
work. Figure 7 below shows a model of an agent incorporating these rules. Goal
contexts are represented as the smaller rectangles below the assumption contexts
they correspond to — we have left out formulas such as (φ ∧ φ) ∧ φ.
Semantically, a model will still contain a set mc̄t for each context in Σ at
each timeslice t, but we may now calculate which contexts are required in Σ
for a sufficient model M , independently of the rules in R. Given a goal α, we
set Σ = σ(α), where σ : Ltrl −→ ℘(Ltrl ) satisfies the following recursive
equations:

σ(p) = ∅ (1)
σ(φ → ψ) = {φ} ∪ σ(ψ) (2)
A full specification of the semantics for goal–assumption interaction is left for
future work.
t=1 t=2 t=3 t=4 t=5

hφψi φ ψ ··· ···

hφψ Gi φ

hφi φ φ, φ∧φ φ, ψ → φ ···

hφGi ψ→φ ψ→φ ψ→φ

h·i φ→φ φ→φ φ → (ψ → φ)

h·Gi φ → (ψ → φ) φ → (ψ → φ) φ → (ψ → φ) φ → (ψ → φ) φ → (ψ → φ)

Fig. 7. Reasoning with goal contexts

7 Summary
We have argued that contexts are suitable tools for reasoning about agents in at
least two ways. Firstly, they can be used to model assumptions, thus providing
a finer grained account than those in which a formula is either believed or dis-
believed. Secondly, contexts can represent temporal stages, or timeslices, of an
agent’s reasoning process. This is a crucial notion if we aim to model resource
bounded agents. A further application of context is to model multiple agents,
each agent being modelled in its own context. Such an approach is explored in
[1] and [2].
Future work aims to explore a full semantics for interaction between be-
liefs (including assumptions), goals/desires and plans/intentions and to look at
real-world applications of assumption-making in reasoning, with games such as
Cluedo as a test case.

References
1. N. Alechina, B. Logan, and M. Whitsey (now Jago). A complete and decidable logic for
resource-bounded agents. In Proc. Third International Joint Conference on Autonomous
Agents and Multi-Agent Systems (AAMAS 2004). ACM Press, July 2004.
2. Natasha Alechina, Brian Logan, and Mark Whitsey (now Jago). Modelling communicating
agents in timed reasoning logics. In José Júlio Alferes and João Alexandre Leite, editors,
JELIA, volume 3229 of Lecture Notes in Computer Science, pages 95–107. Springer, 2004.
3. J. Drapkin and D. Perlis. A preliminary excursion into Step-Logics. Proceedings of the
SIGART International Symposium on Methodologies for Intelligent Systems, pages 262–269,
1986.
4. C. Ghidini and F. Giunchiglia. Local models semantics, or contextual reasoning = locality +
compatability. Artificial Intelligence, 127(2):221–259, 2001.
5. David Kaplan. Demonstratives. In J. Almog, J. Perry, and H. Wettstein, editors, Themes from
Kaplan, chapter 17, pages 481–563. Oxford University Press, New York, 1989.
6. M. Whitsey (now Jago). Timed reasoning logics: An example. In Proc. of the Logic and
Communication in Multi-Agent Systems workshop (LCMAS 2004). Loria, 2004.