# Temporal Logic

*First published Mon Nov 29, 1999; substantive revision Thu Feb 7, 2008*

The term Temporal Logic has been broadly used to cover all approaches to the representation of temporal information within a logical framework, and also more narrowly to refer specifically to the modal-logic type of approach introduced around 1960 by Arthur Prior under the name of Tense Logic and subsequently developed further by logicians and computer scientists.

Applications of Temporal Logic include its use as a formalism for clarifying philosophical issues about time, as a framework within which to define the semantics of temporal expressions in natural language, as a language for encoding temporal knowledge in artificial intelligence, and as a tool for handling the temporal aspects of the execution of computer programs.

## 1. Modal-logic approaches to temporal logic

### 1.1 Tense Logic

Tense Logic was introduced by Arthur Prior (1957, 1967, 1969) as a result of an interest in the relationship between tense and modality attributed to the Megarian philosopher Diodorus Cronus (ca. 340-280 BCE). For the historical context leading up to the introduction of Tense Logic, as well as its subsequent developments, see Øhrstrøm and Hasle, 1995.

The logical language of Tense Logic contains, in addition to the usual truth-functional operators, four modal operators with intended meanings as follows:

P“It has at some time been the case that …” F“It will at some time be the case that …” H“It has always been the case that …” G“It will always be the case that …”

*P* and *F* are known as the *weak tense operators*, while *H* and
*G* are known as the *strong tense operators*. The two pairs are
generally regarded as interdefinable by way of the equivalences

Pp≡ ¬ H¬pFp≡ ¬ G¬p

On the basis of these intended meanings, Prior used the operators to build formulae expressing various philosophical theses about time, which might be taken as axioms of a formal system if so desired. Some examples of such formulae, with Prior's own glosses (from Prior 1967), are:

Gp→Fp |
“What will always be, will be” |

G(p→q)→(Gp→Gq) |
“If p will always imply q, then if p will always be the case, so
will q” |

Fp→FFp |
“If it will be the case that p, it will be — in between
— that it will be” |

¬Fp→F¬Fp |
“If it will never be that p then it will be that it will never be
that p” |

Prior (1967) reports on the extensive early work on various systems
of Tense Logic obtained by postulating different combination of axioms,
and in particular he considered in some detail what light a logical
treatment of time can throw on classic problems concerning time,
necessity and existence; for example, “deterministic” arguments that
have been advanced over the ages to the effect that “what will be, will
necessarily be”, corresponding to the modal tense-logical formula
*F**p*→□*F**p*.

Of particular significance is the system of *Minimal Tense
Logic* *K*_{t}, which is generated by the four axioms

p→HFp |
“What is, has always been going to be” |

p→GPp |
“What is, will always have been” |

H(p→q)→(Hp→Hq) |
“Whatever has always followed from what always has been, always has been” |

G(p→q)→(Gp→Gq) |
“Whatever will always follow from what always will be, always will be” |

together with the two rules of temporal inference:

RH:From a proof of p, derive a proof ofHpRG:From a proof of p, derive a proof ofGp

and, of course, all the rules of ordinary Propositional Logic. The
theorems of *K*_{t} express, essentially, those properties of the
tense operators which do not depend on any specific assumptions about
the temporal order. This characterisation is made more precise below.

Tense Logic is obtained by adding the tense operators to an existing
logic; above this was tacitly assumed to be the classical Propositional
Calculus. Other tense-logical systems are obtained by taking different
logical bases. Of obvious interest is tensed predicate logic, where the
tense operators are added to classical First-order Predicate Calculus.
This enables us to express important distinctions concerning the logic
of time and existence. For example, the statement *A philosopher
will be a king* can be interpreted in several different ways, such
as

∃x(Philosopher(x) & F King(x)) |
Someone who is now a philosopher will be a king at some future time |

∃xF(Philosopher(x) & King(x)) |
There now exists someone who will at some future time be both a philosopher and a king |

F∃x(Philosopher(x) & F King(x)) |
There will exist someone who is a philosopher and later will be a king |

F∃x(Philosopher(x) & King(x)) |
There will exist someone who is at the same time both a philosopher and a king |

The interpretation of such formulae is not unproblematic, however. The
problem concerns the domain of quantification. For the second two
formulae above to bear the interpretations given to them, it is
necessary that the domain of quantification is always relative to a
time: thus in the semantics it will be necessary to introduce a domain
of quantification *D*(*t*) for each time *t*. But this can lead to problems
if we want to establish relations between objects existing at different
times, as for example in the statement “One of my friends is descended
from a follower of William the Conqueror”.

These problems are related to the so-called *Barcan formulae*
of modal logic, a temporal analogue of which is

F∃xp(x)→∃xFp(x) (“If there will be something that isp, then there is now something that will bep”)

This formula can only be guaranteed to be true if there is a constant domain that holds for all points in time; under this assumption, bare existence (as expressed by the existential quantifier) will need to be supplemented by a temporally restricted existence predicate (which might be read 'is extant') in order to refer to different objects existing at different times. For more on this and related matters, see van Benthem, 1995, Section 7.

### 1.2 Extensions to Tense Logic

Soon after its introduction, the basic “PFGH” syntax of Tense Logic was extended in various ways, and such extensions have continued to this day. Some important examples are the following:

**The binary temporal operators S and U (“since” and
“until”)**. These were introduced by Kamp (1968). The intended
meanings are

Spq“ qhas been true since a time whenpwas true”Upq“ qwill be true until a time whenpis true”

It is possible to define the one-place tense operators in terms of *S*
and *U* as follows:

Pp≡ Sp(p∨¬p)Fp≡ Up(p∨¬p)

The importance of the *S* and *U* operators is that they are
expressively complete with respect to first-order temporal properties
on continuous, strictly linear temporal orders (which is not true for
the one-place operators on their own).

**Metric tense logic**. Prior introduced the notation
Fnp to mean “It will be the case the interval *n* hence that *p*”. We do
not need a separate notation Pnp since we can write *F*(-*n*)*p* for “It was
the case the interval *n* ago that *P*”. The case *n*=0 gives us the present
tense. We can define the general, non-metric operators by

Pp≡ ∃ n(n<0 &Fnp)Fp≡ ∃ n(n>0 &Fnp)Hp≡ ∀ n(n<0→Fnp)Gp≡ ∀ n(n>0→Fnp)

**The “next time” operator O**. This operator assumes
that the time series consists of a discrete sequence of atomic times.
The formula *O**p* is then intended to mean that *p* is true at the
immediately succeeding time step. Given that time is discrete, it can
be defined in terms of the “until” operator *U* by

Op≡Up(p&¬p)

which says that *p* will be true at some future time, between which
and the present time nothing is true. This can only mean the time
immediately following the present in a discrete temporal order.

In discrete time, the future-tense operator *F* is related to the
next-time operator by the equivalence

Fp≡Op∨OFp.

Indeed, *F* can here be *defined* as the least fixed point of the
transformation which maps an arbitrary propositional operator *X* onto
the operator
λ*p*.*O**p*∨*O**X**p*.

One could similarly define a past-time version of *O*; but since the
main usefulness of this particular operator has been in relation to the
logic of computer programming, where one is mainly interested in
execution sequences of programs extending into the future, this has not
so often been done.

### 1.3 Semantics of Tense Logic

The standard model-theoretic semantics of Tense Logic is closely
modelled on that of Modal Logic. A *temporal frame* consists of
a set *T* of entities called times together with an ordering relation
< on *T*. This defines the “flow of time” over which the meanings of
the tense operators are to be defined. An interpretation of the
tense-logical language assigns a truth value to each atomic formula at
each time in the temporal frame. Given such an interpretation, the
meanings of the weak tense operators can be defined using the rules

Ppis true attif and only if pis true at some timet′ such thatt′<tFpis true attif and only if pis true at some timet′ such thatt<t′

from which it follows that the meanings of the strong operators are given by

Hpis true attif and only if pis true at all timest′ such thatt′<tGpis true attif and only if pis true at all timest′ such thatt<t′

We can now provide a precise characterisation of system
*K*_{t} of Minimal Tense Logic. The theorems of *K*_{t} are
precisely those formulae which are true at all times under all
interpretations over all temporal frames.

Many tense-logical axioms have been suggested as expressing this or
that property of the flow of time, and the semantics gives us a precise
way of defining this correspondence between tense-logical formulae and
properties of temporal frames. A formula *p* is said to
*characterise* a set of frames *F* if

*p*is true at all times under all interpretations over any frame in*F*.- For any frame not in
*F*, there is an interpretation which makes*p*false at some time.

Thus any theorem of *K*_{t} characterises the class of all
frames.

A first-order formula in < determines a class of frames, namely
those in which the formula is true. A tense-logical formula *p*
corresponds to a first-order formula *q* just so long as *p* characterises
the class of frames for which *q* is true. Some well-known examples of
such pairs of formulae are:

Hp→Pp |
∀t∃t′(t′<t) |
(unbounded in the past) |

Gp→Fp |
∀t∃t′(t<t′) |
(unbounded in the future) |

Fp→FFp |
∀t, t′(t<t′ →
∃t″(t<t″<t′)) |
(dense ordering) |

FFp→Fp |
∀t, t′(∃t″(t<t″<t′)
→ t<t′) |
(transitive ordering) |

FPp →
Pp∨p∨Fp |
∀t, t′, t″((t<t″ &
t′<t″) → ( t<t′
∨
t=t′
∨
t′<t)) |
(linear in the past) |

PFp →
Pp∨p∨Fp |
∀t, t′, t″((t″<t &
t″<t′) → ( t<t′
∨
t=t′
∨
t′<t)) |
(linear in the future) |

However, there are tense-logical formulae (such as *G**F**p*→*F**G**p*) which
do not correspond to any first-order temporal frame properties, and
there are first-order temporal frame properties (such as
*irreflexivity*, expressed by ∀*t*¬(*t*<*t*)) which do
not correspond to any tense-logical formula. For details, see van
Benthem (1983).

## 2. Predicate-logic approaches to temporal logic

### 2.1 The method of temporal arguments

In this method, the temporal dimension is captured by augmenting each time-variable proposition or predicate with an extra argument-place, to be filled by an expression designating a time, as for example

Kill(Brutus, Caesar, 44BCE).

If we introduce into the first-order language a binary infix predicate
< denoting the temporal ordering relation “earlier than”, and a
constant “now” denoting the present moment, then the tense operators
can be readily simulated by means of the following correspondences,
which not surprisingly bear more than a passing resemblance to the
formal semantics for Tense Logic given above. Where *p*(*t*) represents the
result of introducing an extra temporal argument place to the
time-variable predicates occurring in *p*, we have:

Pp∃ t(t<now &p(t))Fp∃ t(now<t&p(t))Hp∀ t(t<now →p(t))Gp∀ t(now<t→p(t))

Before the advent of Tense Logic, the method of temporal arguments was the natural choice of formalism for the logical expression of temporal information.

### 2.2 Hybrid approaches

The reification of time instants implied by the method of temporal
arguments may be regarded as philosophically suspect, instants being
rather artificial constructs unsuited to playing a foundational role in
temporal discourse. Following a suggestion of Prior (1968, Chapter XI),
one might equate an instant with ‘the conjunction of all those
propositions which would ordinarily be said to be true at that
instant’. Instants are thus replaced by propositions which uniquely
characterise them. A statement of the form “True(*p*, *t*)”, saying that
proposition *p* is true at instant *t*, can then be paraphrased as “□
(*t*→ *p*)”, i.e., the instant-proposition *t* necessarily implies *p*.

This kind of manoeuvre lies at the heart of hybrid temporal logics in which the standard apparatus of propositions and tense operators is supplemented by propositions which are true at unique instants, thereby effectively naming those instants without invoking philosophically dubious reification. This can give one some of the expressive power of a predicate-logic approach while retaining the modal character of the logic. (See Areces and Ten Cate, 2006)

### 2.3 State and event-type reification

The method of temporal arguments encounters difficulties if it is
desired to model *aspectual* distinctions between, for example,
states, events and processes. Propositions reporting states (such as
“Mary is asleep”) have *homogeneous* temporal incidence, in that
they must hold over any subintervals of an interval over which they
hold (e.g., if Mary is asleep from 1 o'clock to 6 o'clock then she is
asleep from 1 o'clock to 2 o'clock, from 2 o'clock to 3 o'clock, and so
on). By contrast, propositions reporting events (such as “John walks to
the station”) have inhomogeneous temporal incidence; more precisely,
such a proposition is not true of *any* proper subinterval of an
interval of which it is true (e.g., if John walks to the station over
the interval from 1 o'clock to a quarter past one, then it is not the
case that he walks to the station over the interval from 1 o'clock to
five past one — rather, over that interval he walks part of the
way to the station).

The method of state and event-type reification was introduced to cater for distinctions of this kind. It is an approach that has been especially popular in Artificial Intelligence, where it is particularly associated with the name of James Allen, whose influential paper (Allen 1984) is often cited in this connection. In this approach, state and event types are denoted by terms in a first-order theory; their temporal incidence is expressed using relational predicates “Holds” and “Occurs”, as for example,

Holds(Asleep(Mary), (1pm, 6pm))

Occurs(Walk-to(John, Station), (1pm, 1.15pm))

where terms of the form (*t*, *t*′) denote time intervals in the
obvious way.

The homogeneity of states and inhomogeneity of events is secured by axioms such as

∀s,i,i′(Holds(s,i) & In(i′,i) → Holds(s,i′))

∀e,i,i′(Occurs(e,i) & In(i′,i) → ¬Occurs(e,i′))

where “In” expresses the proper subinterval relation.

### 2.4 Event-token reification

The method of event-token reification was proposed by Donald Davidson (1967) as a solution to the so-called “variable polyadicity” problem. The problem is to give a formal account of the validity of such inferences as

John saw Mary in London on Tuesday. Therefore, John saw Mary on Tuesday.

The key idea is that each event-forming predicate is endowed with an extra argument-place to be filled with a variable ranging over event-tokens, that is, particular dated occurrences. The inference above is then cast in logical form as

∃ e(See(John, Mary,e) & Place(e, London) & Time(e, Tuesday)),Therefore, ∃ e(See(John, Mary,e) & Time(e, Tuesday)).

In this form, the inference does not require any additional logical apparatus over and above standard first-order predicate logic; on that basis, the validity of the inference is considered to be explained. This approach has also been used in a computational context in the Event Calculus of Kowalski and Sergot (1986).

## 3. Philosophical issues

Prior's motivation for inventing Tense Logic was largely philosophical, his idea being that the precision and clarity afforded by a formal logical notation was indispensible for the careful formulation and resolution of philosophical issues concerning time. See the article on Arthur Prior for a discussion of some of these.

### 3.1 Realist vs reductionist approaches to tense

The rivalry between the modal and first-order approaches to
formalising the logic of time reflects an important set of underlying
philosophical issues related to the work of McTaggart. This work is
especially well-known, in the context of temporal logic, for
introducing the distinction between the “*A*-series” and the “*B*-series”.
By the “*A*-series” is meant, essentially, the characterisation of events
as Past, Present, or Future. By contrast, the “*B*-series” involves their
characterisation as relatively “Earlier” or “Later”. A-series
representations of time inescapably single out some particular moment
as present; of course, at different times, different moments are
present — a circumstance which, followed to what appeared to be
its logical conclusion, led McTaggart to assert that time itself was
unreal (see Mellor, 1981). *B*-series representations have no place for a
concept of the present, instead taking the form of a synoptic view of
all time and the (timeless) interrelations between its parts.

There is a clear affinity between the *A*-series and the modal
approach and between the *B*-series and the first-order approach. In the
terminology of Massey (1969), adherents of the former approach are
called “tensers” while adherents of the latter are called “detensers”.
This issue is related in turn to the question of how seriously to take
the representation of space-time as a single four-dimensional entity in
which the four dimensions are at least in some respects on a similar
footing. In view of the Theory of Relativity, it might be argued that
this issue is not so much a matter for Philosophy as for Physics.

### 3.2 Determinism vs non-determinism

The choice of flow of time can be of philosophical significance. For
example, one way of capturing the distinction between deterministic and
non-deterministic theories is to model the former using a strictly
linear flow of time, and the latter with a temporal structure which
allows branching into the future. If we adopt the latter approach, then
it is helpful in describing the semantics of tense and other operators
to introduce the idea of a *history*, which is a maximal
linearly-ordered set of instants. The branching future model will then
stipulate that for any two histories there is an instant such that both
histories share all the times up to and including that instant, but do
not share any times after it. For each history containing a given
instant, the times in that history which are later than the instant
constitute a “possible future” for that instant.

In branching time semantics it is natural to evaluate formulae with
respect to an instant and a history, rather than just an instant. With
respect to the pair (*h*, *t*), we might interpret
“*F**p*” to be true so long as
“*p*” is true at some time in the future of
*t* as determined by the history *h*. A separate
operator ◊ can be introduced to allow, in effect, quantification
over histories: “◊*p*” is true at (*h*,
*t*) so long as there is some history *h*’ such
that “*p*” is true at (*h*’,
*t*). Then “◊*F**p*” says that
“*p*” holds in some possible future, and
“□*F**p*” (where “□”
is the strong modal operator dual to “◊”) says that
“*p*” is inevitable (i.e., holds in all possible
futures). Prior calls this kind of interpretation
“Ockhamist”.

Another interpretation (called “Peircean” by Prior) takes
“*F**p*” to be equivalent to the Ockhamist
“□*F**p*”, i.e., “*p*” is true at some time
in *every* possible future. Under this interpretation there is
no formula equivalent to the Ockhamist “*F**p*”; hence
Peircean tense logic is a proper fragment of Ockhamist tense logic. It
was favoured by Prior on the grounds that future contingent
propositions really do lack truth value: only if a future-tense
proposition is inevitable (all possible futures) or impossible (no
possible futures) can we ascribe a truth value to it now. For Prior's
discussion of these issues, see Prior 1967, Chapter VII. Further
discussion can be found in Øhrstrøm, and Hasle 1995,
chapters 2.6 and 3.2.

The non-determinism implicit in branching time frames has led to their
being used to support theories of action and choice. An important
example is the STIT logics of Belnap and Perloff (1988), with many
subsequent variants (see Xu, 1995). The primitive expression of agency
in STIT theories is that an agent *a* “sees to it that” some
proposition *P* holds, written [*a* stit: *P*]. The
meaning of this construction is specified in relation to a branching
time structure, in which the choices made by agents are representated
by means of sets of possible futures branching forward from the choice
point. The precise interpretation of [*a* stit: *P*] varies
from one system to another, but typically it is specified to be true
at a particular moment if *P* holds in all histories selected by
the agent's choice function at that moment, with the further condition
usually added that *P* fails to hold in at least one history not
so selected (this is in order to avoid the unwelcome conclusion that
an agent sees to it that some tautology holds).

## 4. Applications of Temporal Logic

### 4.1 Applications to natural language

Prior (1967) lists amongst the precursors of Tense Logic Hans
Reichenbach's (1947) analysis of the tenses of English, according to
which the function of each tense is to specify the temporal
relationships amongst a set of three times related to the utterance,
namely *S*, the speech time, *R*, the reference time, and *E*, the event
time. In this way Reichenbach was neatly able to distinguish between
the simple past “I saw John”, for which *R*=*E*<*S*, and the present
perfect “I have seen John”, for which *E*<*R*=*S*, the former statement
referring to a past time coincident with the event of my seeing John,
the latter referring to the present time, relative to which my seeing
John is past.

Prior notes that Reichenbach's analysis is inadequate to account for
the full range of tense usage in natural language. Subsequently much
work has been done to refine the analysis, not only of tenses but also
other temporal expressions in language such as the temporal
prepositions and connectives (“before”, “after”, “since”, “during”,
“until”), using the many varieties of temporal logic. For some
examples, see Dowty (1979), Galton (1984), Taylor (1985), Richards
*et al.* (1989). A useful collection of landmark papers in this area is Mani *et al.* (2005).

### 4.2 Applications in artificial intelligence

We have already mentioned the work of Allen (1984), which is concerned
with finding a general framework adequate for all the temporal
representations required by AI programs. The Event Calculus of Kowalski
and Sergot (1986) is pursued more specifically within the framework of
logic programming, but is otherwise similarly general in character. A
useful survey of issues involving time and temporal reasoning in AI is
Galton (1995), and a comprehensive recent coverage of the area is Fisher *et al.* (2005).

Much of the work on temporal reasoning in AI has been closely tied
up with the notorious *frame problem*, which arises from the
necessity for any automated reasoner to know, or be able to deduce, not
only those properties of the world which *do* change as the
result of any event or action, but also those properties which do
*not* change. In everyday life, we normally handle such facts
fluently without consciously adverting to them: we take for granted
without thinking about it, for example, that the colour of a car does
not normally change when one changes gear. The frame problem is
concerned with how to formalise the logic of actions and events in such
a way that indefinitely many inferences of this kind are made available
without our having to encode them all explicitly. A seminal work in
this area is McCarthy and Hayes (1969). A useful recent reference for
the frame problem is Shanahan, 1997.

### 4.3 Applications in computer science

Following Pnueli (1977), the modal style of Temporal Logic has found
extensive application in the area of Computer Science concerned with
the specification and verification of programs, especially concurrent
programs in which the computation is performed by two or more
processors working in parallel. In order to ensure correct behaviour of
such a program it is necessary to specify the way in which the actions
of the various processors are interrelated. The relative timing of the
actions must be carefully co-ordinated so as to ensure that integrity
of the information shared amongst the processors is maintained. Amongst
the key notions here is the distinction between “liveness” properties
of the tense-logical form *F**p*, which ensure that desirable states will
obtain in the course of the computation, and “safety” properties of the
form *G**p*, which ensure that undesirable states will never obtain.

Non-determinism is an important issue in computer science applications, and hence much use has been made of branching time models. Two important such systems are CTL (Computation Tree Logic) and a more expressive system CTL*; these correspond very nearly to the Ockhamist and Peircean semantics discussed above.

Further information may be found in Galton (1987), Goldblatt (1987), Kroger (1987), Bolc and Szalas (1995).

## Bibliography

- Allen, J. F., 1984,“Towards a general theory of action and time”,
*Artificial Intelligence*, volume 23, pages 123-154. - Areces, C., and ten Cate, B., 2006, “Hybrid Logics”, in Blackburn
*et al.*, 2006. - Belnap, N. and Perloff, M., 1988, “Seeing to it that: A canonical
form for agentives”,
*Theoria*, volume 54, pages 175-199, reprinted with corrections in H. E. Kyberg*et al.*(eds.),*Knowledge Representation and Defeasible Reasoning*, Dordrecht: Kluwer, 1990, pages 167-190. - van Benthem, J., 1983,
*The Logic of Time*, Dordrecht, Boston and London: Kluwer Academic Publishers, first edition (second edition, 1991). - van Benthem, J., 1995, “Temporal Logic”, in D. M. Gabbay, C. J.
Hogger, and J. A. Robinson,
*Handbook of Logic in Artificial Intelligence and Logic Programming*, Volume 4, Oxford: Clarendon Press, pages 241-350. - Blackburn, P., van Benthem, J, and Wolter, F., 2006,
*Handbook of Modal Logics*, Elsevier. - L. Bolc and A. Szalas (eds.), 1995,
*Time and Logic: A Computational Approach*, London: UCL Press. - Davidson, D., 1967, “The Logical Form of Action Sentences”, in N.
Rescher (ed.),
*The Logic of Decision and Action*, University of Pittsburgh Press, 1967, pages 81-95. Reprinted in D. Davidson,*Essays on Actions and Events*, Oxford: Clarendon Press, 1990, pages 105-122. - Dowty, D., 1979,
*Word Meaning and Montague Grammar*, Dordrecht: D. Reidel. - Fisher, M., Gabbay, D., and Vila, L., 2005,
*Handbook of Temporal Reasoning in Artificial Intelligence*, Amsterdam: Elsevier. - Gabbay, D. M., Hodkinson, I., and Reynolds, M., 1994,
*Temporal Logic: Mathematical Foundations and Computational Aspects*, Volume 1,. Oxford: Clarendon Press. - Galton, A. P., 1984,
*The Logic of Aspect*, Oxford: Clarendon Press. - Galton, A. P., 1987,
*Temporal Logics and their Applications*, London: Academic Press. - Galton, A. P., 1995, “Time and Change for AI”, in D. M. Gabbay, C.
J. Hogger, and J. A. Robinson,
*Handbook of Logic in Artificial Intelligence and Logic Programming*, Volume 4, Oxford: Clarendon Press, pages 175-240. - Goldblatt, R., 1987,
*Logics of Time and Computation*, Center for the Study of Language and Information, CSLI Lecture Notes 7. - Hodkinson, I. and Reynolds, M., 2006, “Temporal Logic”, in
Blackburn
*et al.*, 2006. - Kamp, J. A. W., 1968.
*Tense Logic and the Theory of Linear Order*, Ph.D. thesis, University of California, Los Angeles. - Kowalski, R. A. and Sergot, M. J., 1986, “A Logic-Based Calculus of
Events”,
*New Generation Computing*, volume 4, pages 67-95. - Kroger, F., 1987, “Temporal Logic of Programs”, Springer-Verlag.
- Mani, I., Pustejovsky, J., and Gaizauskas, R., 2005,
*The Language of Time: A Reader*, Oxford: Oxford University Press. - Massey, G., 1969, “Tense Logic! Why Bother?”,
*Noûs*, volume 3, pages 17-32. - McCarthy, J. and Hayes, P. J., 1969, “Some Philosophical Problems
from the Standpoint of Artificial Intelligence”, in D. Michie and B.
Meltzer (eds.),
*Machine Intelligence 4*, Edinburgh University Press, pages 463-502. - Mellor, D. H., 1981,
*Real Time*, Cambridge: Cambridge University Press. (Chapter 6 reprinted with revisions as “The Unreality of Tense” in R. Le Poidevin and M. MacBeath (eds.),*The Philosophy of Time*, Oxford University Press, 1993.) - Øhrstrøm, P. and Hasle, P., 1995,
*Temporal Logic: From Ancient Ideas to Artificial Intelligence*, Dordrecht, Boston and London: Kluwer Academic Publishers. - Pnueli, A., 1977, “The temporal logic of programs”,
*Proceedings of the 18th IEEE Symposium on Foundations of Computer Science*, pages 46-67. - Prior, A. N., 1957,
*Time and Modality*, Oxford: Clarendon Press. - Prior, A. N., 1967,
*Past, Present and Future*, Oxford: Clarendon Press. - Prior, A. N., 1969,
*Papers on Time and Tense*, Oxford: Clarendon Press. - Reichenbach, H., 1947,
*Elements of Symbolic Logic*, New York: Macmillan - Rescher, N. and Urquhart, A., 1971,
*Temporal Logic*, Springer-Verlag. - Richards, B., Bethke, I., van der Does, J., and Oberlander, J.,
1989,
*Temporal Representation and Inference*, London: Academic Press. - Shanahan, M., 1997,
*Solving the Frame Problem*, Cambridge MA and London: The MIT Press. - Taylor, B., 1985,
*Modes of Occurrence*, Aristotelian Society Series, Volume 2, Oxford: Basil Blackwell. - Xu, M., 1995, “On the basic logic of
*STIT*with a single agent”,*Journal of Symbolic Logic*, volume 60, pages 459-483.

## Academic Tools

How to cite this entry. Preview the PDF version of this entry at the Friends of the SEP Society. Look up this entry topic at the Indiana Philosophy Ontology Project (InPhO). Enhanced bibliography for this entry at PhilPapers, with links to its database.

## Other Internet Resources

- A.N. Prior: The Founding Father of Temporal Logic, Danish Centre for Philosophy and Science Studies.

## Related Entries

artificial intelligence: logic and | frame problem | logic: hybrid | logic: modal | Prior, Arthur | time