Temporal Logic (Stanford Encyclopedia of Philosophy) Cite this entry Search the SEP • Advanced Search • Tools • RSS FeedTable of Contents• What's New• Archives• Projected ContentsEditorial Information• About the SEP• Editorial Board• How to Cite the SEP• Special CharactersSupport the SEPContact the SEP ©Metaphysics Research Lab,CSLI,Stanford University  Open access to the SEP is made possible by a world-wide funding initiative. Please Read How You Can Help Keep the Encyclopedia FreeTemporal LogicFirst published Mon Nov 29, 1999; substantive revision Thu Feb 7, 2008The term Temporal Logic has been broadly used to cover all approachesto the representation of temporal information within a logicalframework, and also more narrowly to refer specifically to themodal-logic type of approach introduced around 1960 by Arthur Priorunder the name of Tense Logic and subsequently developed further bylogicians and computer scientists.Applications of Temporal Logic include its use as a formalism forclarifying philosophical issues about time, as a framework within whichto define the semantics of temporal expressions in natural language, asa language for encoding temporal knowledge in artificial intelligence,and as a tool for handling the temporal aspects of the execution ofcomputer programs.1. Modal-logic approaches to temporal logic2. Predicate-logic approaches to temporal logic3. Philosophical issues4. ApplicationsBibliographyOther Internet ResourcesRelated Entries1. Modal-logic approaches to temporal logic1.1 Tense LogicTense Logic was introduced by Arthur Prior (1957, 1967, 1969) as aresult of an interest in the relationship between tense and modalityattributed to the Megarian philosopher Diodorus Cronus (ca. 340-280BCE). For the historical context leading up to the introduction ofTense Logic, as well as its subsequent developments, seeØhrstrøm and Hasle, 1995. The logical language of Tense Logic contains, in addition to theusual truth-functional operators, four modal operators with intendedmeanings 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 andG are known as the strong tense operators. The two pairs aregenerally regarded as interdefinable by way of the equivalencesPp≡¬H¬pFp≡¬G¬pOn the basis of these intended meanings, Prior used the operators tobuild formulae expressing various philosophical theses about time,which might be taken as axioms of a formal system if so desired. Someexamples 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, sowill 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 bethat p”Prior (1967) reports on the extensive early work on various systemsof Tense Logic obtained by postulating different combination of axioms,and in particular he considered in some detail what light a logicaltreatment of time can throw on classic problems concerning time,necessity and existence; for example, “deterministic” arguments thathave been advanced over the ages to the effect that “what will be, willnecessarily be”, corresponding to the modal tense-logical formulaFp→□Fp.Of particular significance is the system of Minimal TenseLogic Kt, which is generated by the four axiomsp→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 hasbeen”G(p→q)→(Gp→Gq)“Whatever will always follow from what always will be, always willbe”together with the two rules of temporal inference: RH:From a proof of p, derive a proof of HpRG:From a proof of p, derive a proof of Gpand, of course, all the rules of ordinary Propositional Logic. Thetheorems of Kt express, essentially, those properties of thetense operators which do not depend on any specific assumptions aboutthe temporal order. This characterisation is made more precise below. Tense Logic is obtained by adding the tense operators to an existinglogic; above this was tacitly assumed to be the classical PropositionalCalculus. Other tense-logical systems are obtained by taking differentlogical bases. Of obvious interest is tensed predicate logic, where thetense operators are added to classical First-order Predicate Calculus.This enables us to express important distinctions concerning the logicof time and existence. For example, the statement A philosopherwill be a king can be interpreted in several different ways, suchas∃x(Philosopher(x) & F King(x))Someone who is now a philosopher will be a king at some futuretime∃xF(Philosopher(x) & King(x))There now exists someone who will at some future time be both aphilosopher and a kingF∃x(Philosopher(x) & F King(x))There will exist someone who is a philosopher and later will be akingF∃x(Philosopher(x) & King(x))There will exist someone who is at the same time both a philosopherand a kingThe interpretation of such formulae is not unproblematic, however. Theproblem concerns the domain of quantification. For the second twoformulae above to bear the interpretations given to them, it isnecessary that the domain of quantification is always relative to atime: thus in the semantics it will be necessary to introduce a domainof quantification D(t) for each time t. But this can lead to problemsif we want to establish relations between objects existing at differenttimes, as for example in the statement “One of my friends is descendedfrom a follower of William the Conqueror”. These problems are related to the so-called Barcan formulaeof modal logic, a temporal analogue of which isF∃xp(x)→∃xFp(x) (“If there will besomething that is p, then there is now something that will bep”)This formula can only be guaranteed to be true if there is a constantdomain that holds for all points in time; under this assumption, bareexistence (as expressed by the existential quantifier) will need to besupplemented by a temporally restricted existence predicate (whichmight be read 'is extant') in order to refer to different objectsexisting at different times. For more on this and related matters, seevan Benthem, 1995, Section 7.1.2 Extensions to Tense LogicSoon after its introduction, the basic “PFGH” syntax of Tense Logic wasextended in various ways, and such extensions have continued to thisday. Some important examples are the following: The binary temporal operators S and U (“since” and“until”). These were introduced by Kamp (1968). The intendedmeanings areSpq“q has been true since a time when p was true”Upq“q will be true until a time when p is true”It is possible to define the one-place tense operators in terms of Sand U as follows: Pp≡Sp(p∨¬p)Fp≡Up(p∨¬p)The importance of the S and U operators is that they areexpressively complete with respect to first-order temporal propertieson continuous, strictly linear temporal orders (which is not true forthe one-place operators on their own).Metric tense logic. Prior introduced the notationFnp to mean “It will be the case the interval n hence that p”. We donot need a separate notation Pnp since we can write F(-n)p for “It wasthe case the interval n ago that P”. The case n=0 gives us the presenttense. We can define the general, non-metric operators byPp≡∃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 assumesthat the time series consists of a discrete sequence of atomic times.The formula Op is then intended to mean that p is true at theimmediately succeeding time step. Given that time is discrete, it canbe defined in terms of the “until” operator U byOp ≡ Up(p&¬p)which says that p will be true at some future time, between whichand the present time nothing is true. This can only mean the timeimmediately following the present in a discrete temporal order.In discrete time, the future-tense operator F is related to thenext-time operator by the equivalenceFp ≡ Op ∨ OFp.Indeed, F can here be defined as the least fixed point of thetransformation which maps an arbitrary propositional operator X ontothe operator λp.Op∨OXp. One could similarly define a past-time version of O; but since themain usefulness of this particular operator has been in relation to thelogic of computer programming, where one is mainly interested inexecution sequences of programs extending into the future, this has notso often been done.1.3 Semantics of Tense LogicThe standard model-theoretic semantics of Tense Logic is closelymodelled on that of Modal Logic. A temporal frame consists ofa set T of entities called times together with an ordering relation< on T. This defines the “flow of time” over which the meanings ofthe tense operators are to be defined. An interpretation of thetense-logical language assigns a truth value to each atomic formula ateach time in the temporal frame. Given such an interpretation, themeanings of the weak tense operators can be defined using the rules Pp is true at tif and only ifp is true at some time t′ such that t′<tFp is true at tif and only ifp is true at some time t′ such that t<t′from which it follows that the meanings of the strong operators aregiven by Hp is true at tif and only ifp is true at all times t′ such that t′<tGp is true at tif and only ifp is true at all times t′ such that t<t′We can now provide a precise characterisation of systemKt of Minimal Tense Logic. The theorems of Kt areprecisely those formulae which are true at all times under allinterpretations over all temporal frames.Many tense-logical axioms have been suggested as expressing this orthat property of the flow of time, and the semantics gives us a preciseway of defining this correspondence between tense-logical formulae andproperties of temporal frames. A formula p is said tocharacterise a set of frames F ifp is true at all times under all interpretations over any frame inF.For any frame not in F, there is an interpretation which makes pfalse at some time.Thus any theorem of Kt characterises the class of allframes. A first-order formula in < determines a class of frames, namelythose in which the formula is true. A tense-logical formula pcorresponds to a first-order formula q just so long as p characterisesthe class of frames for which q is true. Some well-known examples ofsuch 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 GFp→FGp) whichdo not correspond to any first-order temporal frame properties, andthere are first-order temporal frame properties (such asirreflexivity, expressed by ∀t¬(t<t)) which donot correspond to any tense-logical formula. For details, see vanBenthem (1983). 2. Predicate-logic approaches to temporal logic2.1 The method of temporal argumentsIn this method, the temporal dimension is captured by augmenting eachtime-variable proposition or predicate with an extra argument-place, tobe 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 aconstant “now” denoting the present moment, then the tense operatorscan be readily simulated by means of the following correspondences,which not surprisingly bear more than a passing resemblance to theformal semantics for Tense Logic given above. Where p(t) represents theresult of introducing an extra temporal argument place to thetime-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 wasthe natural choice of formalism for the logical expression of temporalinformation. 2.2 Hybrid approachesThe reification of time instants implied by the method of temporalarguments may be regarded as philosophically suspect, instants beingrather artificial constructs unsuited to playing a foundational role intemporal discourse. Following a suggestion of Prior (1968, Chapter XI),one might equate an instant with ‘the conjunction of all thosepropositions which would ordinarily be said to be true at thatinstant’. Instants are thus replaced by propositions which uniquelycharacterise them. A statement of the form “True(p, t)”, saying thatproposition 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 thestandard apparatus of propositions and tense operators is supplementedby propositions which are true at unique instants, thereby effectivelynaming those instants without invoking philosophically dubiousreification. This can give one some of the expressive power of apredicate-logic approach while retaining the modal character of thelogic. (See Areces and Ten Cate, 2006) 2.3 State and event-type reificationThe method of temporal arguments encounters difficulties if it isdesired to model aspectual distinctions between, for example,states, events and processes. Propositions reporting states (such as“Mary is asleep”) have homogeneous temporal incidence, in thatthey must hold over any subintervals of an interval over which theyhold (e.g., if Mary is asleep from 1 o'clock to 6 o'clock then she isasleep from 1 o'clock to 2 o'clock, from 2 o'clock to 3 o'clock, and soon). By contrast, propositions reporting events (such as “John walks tothe station”) have inhomogeneous temporal incidence; more precisely,such a proposition is not true of any proper subinterval of aninterval of which it is true (e.g., if John walks to the station overthe interval from 1 o'clock to a quarter past one, then it is not thecase that he walks to the station over the interval from 1 o'clock tofive past one — rather, over that interval he walks part of theway to the station). The method of state and event-type reification was introduced tocater for distinctions of this kind. It is an approach that has beenespecially popular in Artificial Intelligence, where it is particularlyassociated with the name of James Allen, whose influential paper (Allen1984) is often cited in this connection. In this approach, state andevent types are denoted by terms in a first-order theory; theirtemporal 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 theobvious way. The homogeneity of states and inhomogeneity of events is secured byaxioms 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 reificationThe 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 suchinferences 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 anextra argument-place to be filled with a variable ranging overevent-tokens, that is, particular dated occurrences. The inferenceabove 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 logicalapparatus over and above standard first-order predicate logic; on thatbasis, the validity of the inference is considered to be explained.This approach has also been used in a computational context in theEvent Calculus of Kowalski and Sergot (1986). 3. Philosophical issuesPrior's motivation for inventing Tense Logic was largely philosophical,his idea being that the precision and clarity afforded by a formallogical notation was indispensible for the careful formulation andresolution of philosophical issues concerning time. See the article onArthur Prior for a discussion of some of these. 3.1 Realist vs reductionist approaches to tenseThe rivalry between the modal and first-order approaches toformalising the logic of time reflects an important set of underlyingphilosophical issues related to the work of McTaggart. This work isespecially well-known, in the context of temporal logic, forintroducing the distinction between the “A-series” and the “B-series”.By the “A-series” is meant, essentially, the characterisation of eventsas Past, Present, or Future. By contrast, the “B-series” involves theircharacterisation as relatively “Earlier” or “Later”. A-seriesrepresentations of time inescapably single out some particular momentas present; of course, at different times, different moments arepresent — a circumstance which, followed to what appeared to beits logical conclusion, led McTaggart to assert that time itself wasunreal (see Mellor, 1981). B-series representations have no place for aconcept of the present, instead taking the form of a synoptic view ofall time and the (timeless) interrelations between its parts.There is a clear affinity between the A-series and the modalapproach and between the B-series and the first-order approach. In theterminology of Massey (1969), adherents of the former approach arecalled “tensers” while adherents of the latter are called “detensers”.This issue is related in turn to the question of how seriously to takethe representation of space-time as a single four-dimensional entity inwhich the four dimensions are at least in some respects on a similarfooting. In view of the Theory of Relativity, it might be argued thatthis issue is not so much a matter for Philosophy as for Physics.3.2 Determinism vs non-determinismThe choice of flow of time can be of philosophical significance. Forexample, one way of capturing the distinction between deterministic andnon-deterministic theories is to model the former using a strictlylinear flow of time, and the latter with a temporal structure whichallows branching into the future. If we adopt the latter approach, thenit is helpful in describing the semantics of tense and other operatorsto introduce the idea of a history, which is a maximallinearly-ordered set of instants. The branching future model will thenstipulate that for any two histories there is an instant such that bothhistories share all the times up to and including that instant, but donot share any times after it. For each history containing a giveninstant, the times in that history which are later than the instantconstitute a “possible future” for that instant.In branching time semantics it is natural to evaluate formulae withrespect to an instant and a history, rather than just an instant. Withrespect to the pair (h, t), we might interpret“Fp” to be true so long as“p” is true at some time in the future oft as determined by the history h. A separateoperator ◊ can be introduced to allow, in effect, quantificationover histories: “◊p” is true at (h,t) so long as there is some history h’ suchthat “p” is true at (h’,t). Then “◊Fp” says that“p” holds in some possible future, and“□Fp” (where “□”is the strong modal operator dual to “◊”) says that“p” is inevitable (i.e., holds in all possiblefutures). Prior calls this kind of interpretation“Ockhamist”.Another interpretation (called “Peircean” by Prior) takes“Fp” to be equivalent to the Ockhamist“□Fp”, i.e., “p” is true at some timein every possible future. Under this interpretation there isno formula equivalent to the Ockhamist “Fp”; hencePeircean tense logic is a proper fragment of Ockhamist tense logic. Itwas favoured by Prior on the grounds that future contingentpropositions really do lack truth value: only if a future-tenseproposition is inevitable (all possible futures) or impossible (nopossible futures) can we ascribe a truth value to it now. For Prior'sdiscussion of these issues, see Prior 1967, Chapter VII. Furtherdiscussion 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 theirbeing used to support theories of action and choice. An importantexample is the STIT logics of Belnap and Perloff (1988), with manysubsequent variants (see Xu, 1995). The primitive expression of agencyin STIT theories is that an agent a “sees to it that” someproposition P holds, written [a stit: P]. Themeaning of this construction is specified in relation to a branchingtime structure, in which the choices made by agents are representatedby means of sets of possible futures branching forward from the choicepoint. The precise interpretation of [a stit: P] variesfrom one system to another, but typically it is specified to be trueat a particular moment if P holds in all histories selected bythe agent's choice function at that moment, with the further conditionusually added that P fails to hold in at least one history notso selected (this is in order to avoid the unwelcome conclusion thatan agent sees to it that some tautology holds).4. Applications of Temporal Logic4.1 Applications to natural languagePrior (1967) lists amongst the precursors of Tense Logic HansReichenbach's (1947) analysis of the tenses of English, according towhich the function of each tense is to specify the temporalrelationships amongst a set of three times related to the utterance,namely S, the speech time, R, the reference time, and E, the eventtime. In this way Reichenbach was neatly able to distinguish betweenthe simple past “I saw John”, for which R=E<S, and the presentperfect “I have seen John”, for which E<R=S, the former statementreferring to a past time coincident with the event of my seeing John,the latter referring to the present time, relative to which my seeingJohn is past. Prior notes that Reichenbach's analysis is inadequate to account forthe full range of tense usage in natural language. Subsequently muchwork has been done to refine the analysis, not only of tenses but alsoother temporal expressions in language such as the temporalprepositions and connectives (“before”, “after”, “since”, “during”,“until”), using the many varieties of temporal logic. For someexamples, see Dowty (1979), Galton (1984), Taylor (1985), Richardset al. (1989). A useful collection of landmark papers in this area is Mani et al. (2005).4.2 Applications in artificial intelligenceWe have already mentioned the work of Allen (1984), which is concernedwith finding a general framework adequate for all the temporalrepresentations required by AI programs. The Event Calculus of Kowalskiand Sergot (1986) is pursued more specifically within the framework oflogic programming, but is otherwise similarly general in character. Auseful survey of issues involving time and temporal reasoning in AI isGalton (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 tiedup with the notorious frame problem, which arises from thenecessity for any automated reasoner to know, or be able to deduce, notonly those properties of the world which do change as theresult of any event or action, but also those properties which donot change. In everyday life, we normally handle such factsfluently without consciously adverting to them: we take for grantedwithout thinking about it, for example, that the colour of a car doesnot normally change when one changes gear. The frame problem isconcerned with how to formalise the logic of actions and events in sucha way that indefinitely many inferences of this kind are made availablewithout our having to encode them all explicitly. A seminal work inthis area is McCarthy and Hayes (1969). A useful recent reference forthe frame problem is Shanahan, 1997.4.3 Applications in computer scienceFollowing Pnueli (1977), the modal style of Temporal Logic has foundextensive application in the area of Computer Science concerned withthe specification and verification of programs, especially concurrentprograms in which the computation is performed by two or moreprocessors working in parallel. In order to ensure correct behaviour ofsuch a program it is necessary to specify the way in which the actionsof the various processors are interrelated. The relative timing of theactions must be carefully co-ordinated so as to ensure that integrityof the information shared amongst the processors is maintained. Amongstthe key notions here is the distinction between “liveness” propertiesof the tense-logical form Fp, which ensure that desirable states willobtain in the course of the computation, and “safety” properties of theform Gp, which ensure that undesirable states will never obtain. Non-determinism is an important issue in computer scienceapplications, and hence much use has been made of branching timemodels. Two important such systems are CTL (Computation Tree Logic) anda more expressive system CTL*; these correspond very nearly to theOckhamist and Peircean semantics discussed above.Further information may be found in Galton (1987), Goldblatt (1987),Kroger (1987), Bolc and Szalas (1995).BibliographyAllen, 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 Blackburnet al., 2006.Belnap, N. and Perloff, M., 1988, “Seeing to it that: A canonicalform 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 (secondedition, 1991).van Benthem, J., 1995, “Temporal Logic”, in D. M. Gabbay, C. J.Hogger, and J. A. Robinson, Handbook of Logic in ArtificialIntelligence and Logic Programming, Volume 4, Oxford: ClarendonPress, pages 241-350.Blackburn, P., van Benthem, J, and Wolter, F., 2006, Handbookof Modal Logics, Elsevier.L. Bolc and A. Szalas (eds.), 1995, Time and Logic: AComputational Approach, London: UCL Press.Davidson, D., 1967, “The Logical Form of Action Sentences”, in N.Rescher (ed.), The Logic of Decision and Action, University ofPittsburgh 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 ofTemporal Reasoning in Artificial Intelligence, Amsterdam:Elsevier.Gabbay, D. M., Hodkinson, I., and Reynolds, M., 1994, TemporalLogic: Mathematical Foundations and Computational Aspects, Volume1,. Oxford: Clarendon Press.Galton, A. P., 1984, The Logic of Aspect, Oxford:Clarendon Press.Galton, A. P., 1987, Temporal Logics and theirApplications, 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 ArtificialIntelligence and Logic Programming, Volume 4, Oxford: ClarendonPress, pages 175-240.Goldblatt, R., 1987, Logics of Time and Computation,Center for the Study of Language and Information, CSLI Lecture Notes7.Hodkinson, I. and Reynolds, M., 2006, “Temporal Logic”, inBlackburn et al., 2006.Kamp, J. A. W., 1968. Tense Logic and the Theory of LinearOrder, Ph.D. thesis, University of California, Los Angeles.Kowalski, R. A. and Sergot, M. J., 1986, “A Logic-Based Calculus ofEvents”, 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, TheLanguage 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 Problemsfrom the Standpoint of Artificial Intelligence”, in D. Michie and B.Meltzer (eds.), Machine Intelligence 4, Edinburgh UniversityPress, pages 463-502.Mellor, D. H., 1981, Real Time, Cambridge: CambridgeUniversity Press. (Chapter 6 reprinted with revisions as “The Unrealityof Tense” in R. Le Poidevin and M. MacBeath (eds.), The Philosophyof Time, Oxford University Press, 1993.)Øhrstrøm, P. and Hasle, P., 1995, Temporal Logic:From Ancient Ideas to Artificial Intelligence, Dordrecht, Bostonand London: Kluwer Academic Publishers.Pnueli, A., 1977, “The temporal logic of programs”, Proceedingsof the 18th IEEE Symposium on Foundations of Computer Science,pages 46-67.Prior, A. N., 1957, Time and Modality, Oxford: ClarendonPress.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, NewYork: MacmillanRescher, 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: AcademicPress.Shanahan, M., 1997, Solving the Frame Problem, CambridgeMA and London: The MIT Press.Taylor, B., 1985, Modes of Occurrence, AristotelianSociety Series, Volume 2, Oxford: Basil Blackwell.Xu, M., 1995, “On the basic logic of STIT with a singleagent”, Journal of Symbolic Logic, volume 60, pages459-483.Other Internet ResourcesRelated Entries artificial intelligence: logic and | frame problem | logic: hybrid | logic: modal | Prior, Arthur | time Copyright © 2008 byAntony Galton<A.P.Galton@exeter.ac.uk> |
|
