\documentclass[twoside, fleqn, 11pt]{article}

\usepackage{a4meu}
%\usepackage{amsmath}
\usepackage{amssymb}
%\usepackage{amsfonts}
%\usepackage[catalan]{babel}
%\usepackage[latin1]{inputenc}
\usepackage[boxed,longend]{algorithm2e}

\input{psfig}
\input{newcommand.tex}
%\input{newcommand-logica.tex}

\newcommand{\timeset}{{\cal T}}

\newcommand{\timet}{\cal T}
\newcommand{\ti}{\cal TI}

\newcommand{\tent}{{\cal E}}

\renewcommand{\li}{\cal L}

\newcommand{\instants}{T_{\mbox{\footnotesize point}}}
\newcommand{\tspans}{T_{\mbox{\footnotesize span}}}
%\newcommand{\tspans}{T_{\mbox{\footnotesize span}}}
\newcommand{\intervals}{T_{\mbox{\footnotesize int}}}

\newcommand{\finf}{{\cal F}_{\infty}}
\newcommand{\ft}{{\cal F}_t}
\newcommand{\ftime}{{\cal F}_{time}}

\newcommand{\rinf}{{\cal R}_{\infty}}
\newcommand{\rt}{{\cal R}_t}
\newcommand{\rtime}{{\cal R}_{time}}

\newcommand{\funat}{\mbox{\bf F}_{\infty}}
\newcommand{\funtime}{\mbox{\bf F}_{time}}
\newcommand{\funt}{\mbox{\bf F}_t}
\newcommand{\funevents}{\mbox{\bf F}_{event}}
\newcommand{\funfluents}{\mbox{\bf F}_{fluent}}

\newcommand{\predat}{\mbox{\bf P}_{\infty}}
\newcommand{\predtime}{\mbox{\bf P}_{time}}
\newcommand{\predt}{\mbox{\bf P}_t}
\newcommand{\predevents}{\mbox{\bf P}_{event}}
\newcommand{\predfluents}{\mbox{\bf P}_{fluent}}

\newcommand{\tokens}{E_{\mbox{\footnotesize token}}}
\newcommand{\fluents}{E_{\mbox{\footnotesize fluent}}}
\newcommand{\events}{E_{\mbox{\footnotesize event}}}
\newcommand{\acions}{E_{\mbox{\footnotesize action}}}
\newcommand{\states}{E_{\mbox{\footnotesize state}}}

\newcommand{\MTL}{\mbox{\it MTL\ }}
\newcommand{\TA}{\mbox{\it TA\ }}
\newcommand{\TTA}{\mbox{\it TTA\ }}
\newcommand{\TR}{\mbox{\it TR\ }}
\newcommand{\TTR}{\mbox{\it TTR\ }}

\bibliographystyle{abbrv}
 
\title{Temporal Qualification in Artificial Intelligence}
\author{Han Reichgelt \\
\small Department of Information Technology \\
\small {\it Georgia Southern University}\\
\small Statesboro, GA 30460-8150, U.S.A.  
\and 
Llu\'{\i}s Vila\thanks{Research funded by the Spanish CICYT under
  grant TIC2002-04470-C03-01
and under ``Web-I(2)'' grant TIC2003-08763-C02-01.
} \\
\small Department of Software\\
\small {\em Technical University of Catalonia}\\
\small Barcelona, Catalonia, Spain
}
\begin{document}
\comentari{Terminology and style codes:
- sorts: CAPS, 
- symbol sets: \bf, CAPS, 
- symbols: \em, CAPS, 
- semantic sets: CAPS, CAL, 
} % end comentari
\date{}
\maketitle

%\centerline{\framebox{2/May/04 draft}}

\begin{abstract}
We use the term {\em temporal qualification} to refer to
the way a logic is used to express that temporal propositions
are true or false at different times.
%
Various methods of temporal qualification have been proposed in the AI community.
Beginning with the simplest approach of adding time as an extra argument
to all temporal predicates,
these methods move to different levels of representational sophistication.
In this paper we describe and analyze a number of approaches
by looking at the syntactical, semantical and ontological decisions they make.
%
From the ontological point of view, there are two issues:
(i) whether time gets full ontological status or not
and 
(ii) what do the temporally qualified expressions represent:
{\em temporal types} 
or
{\em temporal tokens}.
%
Syntactically time can be explicit or implicit in the language.
%
Semantically
a line is drawn between methods whose semantics is based on standard first-order logic
and those that move beyond it to
either higher-order semantics,
possible-world semantics 
or an {\em ad hoc} non-standard temporal semantics.
%
\end{abstract}


% --------------------------------------------------------------------------
\section{Introduction}\label{Introduction}

% --- context
Temporal reasoning in artificial intelligence deals with
{\em relationships} that hold at some times and do not hold at other
times (called {\em fluents}),
{\em events} that occur at certain times,
{\em actions} undertaken by an actor at the right time to achieve a goal
and 
{\em states} of the world that are true or hold for a while and
then {\em change} into a new state that is true at the following time.
% --- example
Consider the following illustrative example that will be used
throughout the paper:
\begin{quote}
``On 1/4/04, 
SmallCo sent an offer for
selling goods $g$ to BigCo for price $p$
with a 2 weeks expiration interval.
BigCo received the offer three days later\footnote{This trading
  example probably ought to be updated to an e-treading scenario where
  the messages are received 2 or 3 seconds after being sent,
however we believe that the essential representation issues and results
still would be the same.} 
and it has been effective since then.
A properly formalized offer becomes effective as of it is received
by the offered and continues to be so until it is accepted by the offered
or the offer expires (as indicated by its expiration interval).
Anybody who makes an offer is committed to the offer as long as the
offer is effective.
Anybody who receives an offer is obliged to send a confirmation
to the offerer within two days.''
\end{quote}

\noindent This narrative contains instances of the temporal phenomena mentioned above:
\begin{itemize}
\item
{\em fluents} 
such as ``$x$ being effective from time $t$ to time $t'$''.
In this case, the beginning and the end and the duration are not fully
determined but the beginning is.
Naturally, this fluent may also hold on a set of non-overlapping intervals of time.
\item
{\em Actions} such as ``an agent $x$ to send an object or
  message $y$ to agent $z$ at time $t$''.
Observe that this also may happen more than once 
for the same $x$, $y$ and $z$, with $t$ being the only distinctive feature.
\item
{\em Events} such as ``$x$ receives $y$ on time $t$''.
Both executed actions and events potentially are causes of some
change in the domain.
In this case, the event causes the offer to be effective as of the reception time.
\item
{\em States} such as the state before ``1/Apr/04''
and the state right after receiving the offer
where the offer is effective and various obligations hold.
\end{itemize}

\noindent Additionally, we observe other kinds of temporal aspects such as:
\begin{itemize}
\item
Temporal features of an object or the object itself.
For instance ``the manager of SmallCo'' can be a different person at
different times
or even ``SmallCo'' could denote different companies at different times
depending on our timeframe.
\item
Temporal relations between events and fluents
such as
``The offer is effective as of it is received by the offered 
and will be so until it is accepted by the offered or it expires''
or
``sending an object \ul{causes} the destiny to receive it between 1 and
4 days later.''
\item
Temporal relations between fluents
such as
``the offered is committed to the offer as long as the offer is effective''
or 
``an offer cannot be effective and expired at the same time''.
% *** anything else ?
\end{itemize}

\noindent Notice that references to time objects may appear in a variety of styles:
absolute (``1/Apr/04''),
relative (``two days later''),
instantaneous (\now),
durative (``the month of march''),
precise (``exactly 2 days''),
vague (``around 2 days''),
etc.

This example illustrates the issues that must be addressed 
to design a formal language for temporal reasoning\footnote{The presentation is biased 
towards the standard definition of first-order logic (FOL),
although nothing prevents the situation of the elements described here in
the context of a different logic,
including non-standard semantics for FOL, modal logics and
higher-order logics.},
namely
the {\em model of time}
i.e. the set or sets of time objects (points, intervals, etc.)
that time is made of with their structure,
the {\em temporal ontology}
i.e. the classification of different temporal phenomena (fluents,
events, actions, etc.),
the {\em temporal constraints language},
i.e. the language for expressing constraints between time objects,
the {\em temporal qualification} method
and the {\em reasoning system}.
Research done on these issues is reviewed in the various chapters of 
this volume. 
Here we shall focus on {\bf Temporal Qualification}:
\begin{quote}
By a temporal qualification method we mean
%
the way a logic 
(that we shall call the {\em underlying logic} of our temporal framework)
is used to express the above temporal phenomena at specific times.
\end{quote}
One may either
adopt a well-known logic equiped with a well-defined model and proof theory
or
define a language with a non-standard model theory
and develop a proof theory for it.

Indeed, 
the temporal qualification method is a central issue in defining a temporal
reasoning framework and it is closely related to the other issues
mentioned above.
The reader must be aware that most of these issues are discussed in
other parts of this volume.
We discuss them here up to level needed to make
to make our presentation self-contained
and discuss the advantages and shortcomings of each temporal
qualification approach.

\subsection{Temporal Reasoning Issues}\label{FormalFramework}

\subsubsection{The Model of Time}

Modeling time as a mathematical structure requires deciding
(i) the class or classes of basic objects time is made of
such as instants, intervals, etc.
(i.e. the {\em time ontology})
and 
(ii) deciding what are the properties these time sets: 
dense vs. discrete, bounded vs. unbounded,  partial/total/\ldots
order, etc.
(i.e. the {\em time topology}).

This issue is discussed in chapter {\em Theories of Time and Temporal Incidence} 
in this handbook
and we shall remain silent on what the best model of time is.
When introducing a temporal qualification method
we shall merely assume we are given a {\em time structure}
$$
\langle \timeset_1, \ldots ,\timeset_{n_t}, \ftime, \rtime \rangle
$$
where each $\timeset_i$ is a non-empty set of time objects,
$\ftime$ is a set of functions defined over them,
and $\predtime$ is a set of relations over them.
For instance,
when formalizing our example we shall take a time structure with three sets:
a set of time points $\timeset_1$ that is isomorphic to the natural numbers
(where the grain size is one day),
the set of ordered pairs of natural numbers $\timeset_2$
and $\timeset_3$ a set of durations or temporal spans that is
isomorphic to the integers.
$\ftime$ contains the functions 
$\bbegin,\eend: \timeset_2 \mapsto \timeset_1,
-: \timeset_1 \times \timeset_1 \mapsto \timeset_3$ and
$\rtime$ contains relations like 
$<_1$ and $=_1$ for $\timeset_1$
$<_3$ and $=_3$ for $\timeset_3$
and the known qualitative interval relations like 
$\meets,\overlaps,\ldots\subseteq \timeset_2 \times \timeset_2$.

The decision made on the model of time is ``fairly'' independent of
the temporal qualification method but it has an impact on the formula
we one can write and the formula we can proof.
On the one hand,

The reader must bear in mind that the temporal qualification method one selects
will determine how the model of time adopted will be
embedded in the temporal reasoning system.
The completeness of a proof theory depends on the availability of a
theory that captures the properties of the model of time
and allows the proof system to infer all statements valid in the time structure.
Such a theory, the {\em theory of time},
may have the form of a set of axioms written in the temporal language
that will include symbols denoting functions in $\ftime$ and relations in $\rtime$.
For example,
the transitivity of ordering relationship (denoted by $<_1$) over $\timeset_1$ 
can be captured by the axiom
$$
\forall\ t_1, t_2, t_3\
[ t_1 <_1 t_2 \land t_2 <_1 t_3) \limplies t_1 <_1 t_3 ]
$$
Depending on the time structure and the expressive power of {\em underlying logic} 
it can be the case that such complete set of axioms cannot be written in our language.

\comentari{***(we should say that the axioms may be replaced by
  additional inference rules in the proof theory)
An alternative way to capture the theory of time is
defining a logic with a specific temporal semantics that 
fixes the desired properties for time and temporal truth.
Once the model theory is properly defined
then a proof theory can be designed with the appropriate set of
inference rules that ought to be able to generate all valid 
consequences that can be written in language.
Of course, this choice requires much more effort than the previous one.
}% end comentari


\subsubsection{Temporal Constraints Language}

The language of expressions denoting constraints between temporal
objects.
Formulas are logical combinations of
atoms built on 
{\em time constants} (possibly of different nature) e.g. ``1/Apr/04'' or ``2 days'',
that denote time objects in  $\timeset_1, \ldots ,\timeset_{n_t}$,
function symbols that denote functions in $\ftime$
(we call them {\em time functions}),
and predicates, we call them {\em time predicates},
that denote relations in $\rtime$
whose arguments are all {\em time terms}.


\subsubsection{Temporal Ontology and the Theory of Temporal Incidence}

As discussed in two previous chapters in this book (``Eventualities'' by A. Galton
and also partly in Vila's ``Theories of Time and Temporal Incidence''),
temporal statements can be classified in various classes
(as illustrated by the different temporal phenomena in our example)  
each associated with a pattern of temporal incidence.
Different temporal ontologies have been proposed in different contexts
such as natural language understanding and common-sense reasoning.
% ***references natural language understanding vanVendler, reasoning about change
% Shoham \cite{Shoham87b, GAlton...
In most cases,
the result of such ontological studies
is a classification of temporal relations 
into a number of classes (e.g. fluents, events, etc.).
For our purpose here we shall refer to these classes as 
$$
\mbox{\em temporal entities} = \{ \tent_1, \ldots , \tent_{e_n} \}
$$
and assume that each class is accompanied by a pattern of temporal incidence that
sometimes is characterized by one or more axioms written in our logical language
through some sort of {\em temporal incidence meta-predicates}.
We call the set of these axioms the {\em theory of temporal incidence} $\timeset_i$.

For instance,
when formalizing our example we shall have the following temporal entities:
%{\em temporal objects} that come to existence and disappear,
(i) {\em events} or {\em accomplishments}
such as ``send a legal object on time t'',
that occur either at a time point i.e. one day,
or during a time span (several days)
and 
(ii) {\em fluents} 
such as ``the offer is effective as of t''
that hold homogeneously throughout a number of days.
Whereas the occurrence of an event over an interval is {\em solid}
(if it holds on a interval it does not hold on any interval that overlaps with it),
the holding of a fluent over an interval is {\em homogeneous}
(if it holds during an interval it also holds over any subinterval).
For example, if we would have the meta-predicate $\holds^3$,
then for each fluent $R^k \in {\cal E}_{\small fluents}$\\
$
\mbox{}\hspace{0.5cm}
  \forall\ t_1,t_2,x_1,\ldots,x_k\ [\ \holds(t1,t2, R^k(x_1,\ldots,x_k))
  \limplies
\\\mbox{}\hspace{1cm}\forall\ t_3,t_4\ 
[(t_3,t_4)\subseteq (t_3,t_4)\limplies \holds(t3,t4, R^k(x_1,\ldots,x_k))]\ ]
$\\

Although these issues are out of the scope of this study,
we must bear in mind that the temporal qualification method 
determines how are the temporal incidence axioms written and 
the formula derived from them.


\subsection{Temporal Qualification Issues}\label{Issues}

Having the previous issues out of the way,
let's point out the issues determined by a temporal qualification method\footnote{As a matter of fact, it can be argued that any method of
  temporal qualification method can be regarded as the set of
  decisions made with respect to these issues.}:
\begin{itemize}
\item 
{\em The distinction between temporal and atemporal individuals.}
As illustrated by the example,
a distinction ought to be made between atemporal individuals
(i.e. individuals that are independent of time such as color green, number 3, \ldots)
and individuals whose existence depends on time
such as ``contract c1-280-440'' or ``the SmallCo company".
\item
{\em The distinction is made between temporal and atemporal functions.}
The introduction of time also leads to the need
of making a semantic distinction between temporal functions
and classical functions possibly co-existing in the same logic.
We define a {\em temporal function} as a function whose value can be
different at different times, for example ``the manager of''(SmallCo).
We shall call $\ft$ the set temporal function symbols
and $\finf$ the set of atemporal predicate symbols.
\item
{\em The distinction between temporal and atemporal relations.}
Similarly,
a temporal logic ought to have a semantic distinction between
relations whose truth-value can be different at different times,
such as 
``agent $a_1$ sends an offer to $a_2$ of selling $g$''
and
those whose truth-value is independent of time as in classical logics
such as ``a contract is a legal document'' (from the domain ontology)
and ``an offer is properly formalized''.
Notice that the {\em time relations} mentioned above are in fact atemporal relations.
% For a given domain, we***
\item
{\em The distinction between temporal occurrences and temporal types
  of occurrences.}
By a temporal occurrence (namely {\bf temporal token}) 
we mean a particular temporal relation when is true at a specific time
(e.g. ``on time t agent $a_1$ sends an offer to $a_2$ of selling $g$'')
as opposed to the term {\em temporal type} that 
means the set of all occurrences of a temporal relation 
(e.g. the set of all specific sending events of type ``agent $a_1$ sends an offer to $a_2$ of selling $g$'').
\item
{\em The specification of time and temporal incidence theories.}
As we explained,
the time and temporal incidence theories are do not condition the
temporal qualification
an representational issue for our temporal qualification method
is the flexibility and expressiveness provided to specify the axioms
of these theories.
\item
{\em The specification of ``nested'' temporal relations.}
A temporal relation that relates objects or other relations that in
turn are temporal.
For example, ``an agent is committed for a period to send a
confirmation of a certain offer''. The commitment, the send action
and the offer are all temporal relations.
\item
{\em The specification of relations between temporal relations or
  their occurrences.}
The paradigmatic example of this is the causal relation between 
a temporal relation whose occurrence causes another relation to hold.
Other examples are 
incompatibility between temporal relations,
correlation of temporal relations,
or class-subclass links bounds between temporal relations.
\end{itemize}

% --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- 
%\subsection{Overview}

As a matter of fact, 
temporal qualification is an issue 
in any formal temporal representation, no matter its context.
In this section we quickly overview temporal qualification in
different areas,
ending with temporal qualification in AI where we briefly introduce 
the approaches that will be discussed in detail in the following sections.

\subsection{Temporal Qualification in Logic}\label{TemporalQualificationinLogic}

\paragraph{Classical Logics.}
Classical logics have proven useful for reasoning 
about domains that are atemporal (such as mathematics) 
or in domains where time is not a relevant feature and can be
abstracted away 
(e.g. a diagnostic system in a domain where the times of the relevant symptoms
do not affect the result of the diagnosis).
However, in many domains time cannot be disregarded if we want our
logical system to be correct and complete.
Logicians have studied different theories to model time
and designed various temporal logics.
In such logics, 
statements are no longer timelessly true or false 
but are true or false at a certain time.
Temporality may be inherent in any component of the formula,
functions, predicates or logical connectives,
in particular, as soon as we have a time domain it is natural to {\em quantify} over time individuals.

A simple approach to formulating a temporal logic
is as a particular FOL with a time theory.
Temporal functions and predicates are supplemented with an additional argument
representing the time at which they are evaluated
and time is characterized by a set of first-order axioms.
Standard FOL syntax and semantics are preserved
and, therefore, standard FOL proof theory is also valid
however we must be careful with the time axioms.
On the one hand, 
as discussed above,
the completeness of the theorem prover depends on the existence 
of a complete first-order axiomatization for the intended time structures.
On the other hand, 
the time axioms may easily lead to an explosion of the search space to be explored by the theorem prover.

It is convenient to move to a {\bf many-sorted logics} 
\cite{Cohn87,Walther87,Manzano93,Cimattietal98}
since it naturally allows to distinguish between time and non-time individuals.
Many-sorted logics do not extend FOL's expressive power
(it is well-known that a many-sorted first-order logic can be translated to standard FOL)
but it provides several advantages.
Notation is more efficient as formulas are more readable, more
``elegant'' and some $\limplies$ can be dropped yielding more compact formulas.
Semantics also can be regarded as a simple FOL extension,
therefore many-sorted logic preserves the most interesting logical properties of FOL
while it provides some potential for making reasoning more efficient.
A formula parser can perform ``sort checking''
and some of the reasoning involving the sortal axioms
can be moved into the unification algorithm.
Although this leads to a more expensive unification step,
this is typically more than off set by the reduction in the search space
that can be achieve through the elimination of the sortal axioms
from the theory.
% The many-sorted This approach has been widely adopted within AI and we discuss it below in deeper detail.


\paragraph{Modal Logics.}
An alternative way to incorporate time is by complicating the model theory,
along the lines of modal logic.
Using the common Kripke-style possible world semantics for {\bf modal
  logics}, each {\em possible world} represents a different time
while the {\em accessibility relationship} becomes a temporal ordering
relationship between possible worlds.
Different modal temporal logics are obtained by
(i) imposing different properties on the accessibility relationship,
and
(ii) choosing different domain languages (e.g. propositional, first-order, ...).
In order to provide an efficient notation,
modal varieties of temporal logic use a number of temporal modal operators, 
operators that are applied to propositions in the domain logic
and change the time with respect to which the proposition is to be interpreted. 
Traditionally, four primitive  {\em modal temporal operators} are defined:
$F$ (at some future time), 
$P$ (at some past time), 
$G$ (at any future time) and 
$H$ (at any past time).
Hence $F \varphi$ denote that the formula $\varphi$ is true at
some future time.
Other common temporal modalities are
$p \until\ q$ ($p$ is true until $q$ is true),
$p \since\ q$ ($p$ has been true since $q$ has been true)
or $\AT(t)\ p$ ($p$ is true at time $t$).


\subsection{Temporal Qualification in Databases}

From a purely logical point of view,
classical database applications \cite{Ahn86,Tanseletal93,Chomicki94}
have followed the first approach outlined in the previous section.
In addition to the original relations and a data domain for the values of the attributes,
the temporal database includes a temporal domain.
Typically, temporal databases use an instant-based approach to time.
Some kind of mathematical structure is imposed on instants:
usually one that is isomorphic to the natural numbers.
A temporal database
can be abstractly defined in a number of different ways\cite{Chomicki94}.

\paragraph{The Model-theoretic View.}
A database is abstractly viewed as a two-sorted first-order language.
Each relation $P$ of arity $n$ gives rise to a predicate $R$ with arity $n+1$,
where the additional argument is a time argument. 
Its intended meaning is as follows:
$$
(a_1, \ldots, a_n, t)\in R\ \mbox{ if and only if }\ P(a_1, \ldots, a_n) \mbox{ holds
at time }t
$$
All $a_i$ are constant symbols denoting elements in a data domain.
The set of constant symbols is possibly extended with some symbols
denoting elements in the temporal domain.
The theory may also add some time function and relation symbols,
such as a function symbol $t+1$ to denote the time immediately following $t$
or the relation $<$ to denote temporal ordering.

Some databases require multiple temporal dimensions.
The usual case is that a single temporal domain is assumed.
The relational predicates are then given two temporal arguments
to indicate that the relation holds between two points in time (interval timestamps),
or a number of time arguments used to model multiple kinds of time.
For example, in the so-called {\em bi-temporal databases},
one set of temporal arguments refers to the  
{\em valid time} (the time when the relation is true in the real world)
and another to the
{\em transaction time} (the time when the relation was recorded in the database)
\cite{SnodgrassAhn86}.
The different interpretations of multiple temporal attributes
databases are captured by {\em integrity constraints}.
For example, a constraint may state that the beginning of an interval always precedes
its end or that transaction time is not before valid time. 

\paragraph{The Timestamp View.}
Moving to concrete databases 
(database that are to be implemented and therefore must allow for a finite representation),
the most useful view is the timestamp view.
In this view, each tuple is supplemented with a timestamp formula
possibly representing an infinite set of times.
A timestamp formula is a first-order formula with one free variable in
the language of the temporal domain, e.g. $0<t<3 \vee 10<t$.
Different temporal databases result from different decisions
about what subsets can be defined by timestamp formulas.
An interesting temporal domain is the Presburger arithmetic 
as it allows one to describe periodic sets 
and therefore has obvious application in calendars and repeating events.

It is not clear whether timestamps could be defined
in a language richer than the first-order theory of
the time domain \cite{Chomicki94}. 
However, there are some approaches that extend the timestamp view by
associating timestamps not to tuples but to attribute values \cite{Tansel93}.
Such approaches increase data expressiveness and temporal flexibility
but pay for this through increased query complexity, and hence decreased efficiency.

\paragraph{Temporal Query Languages.}
While the temporal arguments approach has been predominant in temporal databases 
a wide variety of languages have been explored for querying them.
These range from logic programs with a single instantaneous temporal
argument to temporal logics with modal operators such as \since, \until,
etc. 
Readers interested in temporal query languages are referred to the 
the chapter on this subject in this volume.


\subsubsection{Temporal Qualification in Computer Systems}\label{TemporalQualificationinCS}

Computer systems can be regarded as a sequence of states.
Each state is characterized by a set of propositions stating what is
true at that time.
Interesting reasoning tasks such as system specification, verification
and synthesis can be states in terms of logical properties that must
hold at some times/states in the future when the system starts at a
certain initial state.

In this context,
it is appropriate to model time as an ordered, discrete sequence of time points 
and 
the dominant temporal qualification approach is modal logics.
The reasons are that temporal modal operators allow one to easily express
relative temporal references
(e.g.,``the value of variable $a$ is $x$ until this assignment
statement is executed'').
Modal operators also provide a very efficient notation for various
levels of nested temporal references
(e.g. ``p will have been true until then'').
Also the semantics fits the discrete time model very well.
Since modal temporal logic is discussed at length in other chapters in
this volume we will not expand on this discussion here
and merely refer the reader to these other chapters.


\subsection{Temporal Qualification in AI}\label{TemporalQualificationinAI}

It has been recognized that AI problems
such as natural language understanding,
common-sense reasoning, planning, autonomous agents, etc. 
make greater demands on the expressive power of temporal logics
than many other areas in computer science.
For example, the temporal reasoning that autonomous agents are required to undertake
typically require both relative and absolute temporal references.
Autonomous agents also often require reasoning about
different possible futures and,
if they are to engage in abductive reasoning, 
they may have to consider different possible pasts
in order to determine which past is the best explanation
for the current state of affairs.

All techniques that have been employed in temporal databases
and/or computer science have also been applied in AI:
\begin{itemize}
\item
The method of {\em temporal arguments} has been an appealing method to many AI
researchers because of its simplicity,
the availability of interesting results on FOL theorem proving,
and the fact that its expressiveness is not as limited as has commonly
been claimed\cite{Bacchusetal91} if we allow temporal arguments in
functions as well as in predicates.
\item
{\em Temporal Modal logics} 
have been appealing to those interested in formalizing
natural language
(the so-called {\em tense logics}) and formal knowledge representation.
\end{itemize}
However, it is a third family of techniques that attracted much of
the attention from AI researchers, specially during the 80s and 90s,
namely the {\em reified approach}.
In the reified approach, one
``reifies'' temporal propositions and introduces \ul{names} for them.  
One then uses predicates such $\holds$ or $\occurs$ to express that the
named proposition is true at a certain time, or over a certain interval.
Classical examples of this approach are 
the {\em situation calculus} \cite{McCarthyHayes69,Reiter01,Shanahan00},
McDermott's logic for plans\cite{McDermott82}, 
Allen's interval logic \cite{Allen84}, 
{\em event calculus} \cite{KowalskiSergot86,Shanahan00},
the {\em time map manager} \cite{DeanMcDermott87},
Shoham's logic for time and change \cite{Shoham87b}
Reichgelt's temporal reified logic \cite{Reichgelt89},  
Token reified logics \cite{VilaReichgelt96}, 
action languages \cite{Lifschitz95}, etc.

The attraction of the reified approach is to a large extent due to the fact
that the inclusion of names for such entities
as actions, events, properties and states in the formalism
allows one to predicate and quantify over such entities,
something that is not allowed in either the method of temporal arguments
or in temporal modal logic.
This expressive power is important in many AI applications.
Even our seemingly simple example includes examples of propositions
that require quantification.
The proposition 
``An offer remains valid until it either expires or is withdraw''
is most naturally regarded as involving a quantification
over expiration and withdrawal events.
Other examples of propositions that are best regarded 
as involving quantification over events and/or states
include propositions such as 
``whenever company X is in need of cleaning services,
it issues a tender document'', or 
``State-funded agencies can only issue contracts
after an open and transparent tendering process''.

Although reified logics have proven very popular, 
they have come under attack from different angles.
First,
temporal reified systems have been presented without a {\em precise formal semantics}.
While temporal reified logics in general remain first-order,
the introduction of names for events and states,
and some meta-predicates tot assert their temporal occurrence,
means that one cannot simplistically rely on the standard semantics for first-order logic
to provide a rich enough semantics for a temporal reified logic.
In some cases, 
like Shoham's reified logic,
the apparent increased expressive power is not superior to that of the
standard, easy-to-define method of temporal arguments \cite{Bacchusetal91}
Second, in the cases in which the expressiveness advantage is clear,
the price to pay is a logic that may end being far too complex. 
Third, reified temporal logics also received criticisms from the ontological point view, 
Galton \cite{Galton91}, for example, considers them 
{\em ``philosophically suspect and technically unnecessary''},
as they seem to advocate the introduction of {\em temporal types} in the ontology.
One way to escape from this criticism is to move to an ontology of temporal
propositions based on {\em temporal tokens}.
A temporal token is not to be interpreted as a type of temporal
propositions but as a particular temporal instance of a temporal proposition.
Such ontology has been used as the basis for some alternative temporal
qualification methods
such as {\em temporal token arguments} or {\em temporal token reification}.


\subsection{Paper Outline}\label{TheDesiderata}

In the following sections we describe in detail
the most relevant methods of temporal qualification in AI 
that we briefly introduced in the previous subsection.
We look at the  
syntactical, semantical and ontological decisions they make.
As we have seen,
syntactically we distinguish between those that represent times as
additional arguments
and those that introduce specific temporal operators.
Semantically,
the main distinction is  
between those methods that stay within standard first-order logics
and those that move to some sort of non-standard semantics,
either defined from scratch
or by adapting some known non-classical semantics such as modal logics. 
Finally,
from the ontological point of view,
we distinguish between the methods that only give full ontological status
to time
from the ones that, in addition, include in the ontology denotations
for temporal propositions: 
these can be either {\em temporal types} 
or {\em temporal tokens} if they represent particular temporal
occurrences of a temporal expression.

Each method is illustrated by formalizing our trading example.
The reader should recall that we assume we are given the following:
\begin{itemize}
\item
{\bf The model of time.}
The {\em time structure} composed of the three time subdomains:
a set of time points $\timeset_1$ that is isomorphic to the natural numbers
(where the grain size is one day),
the set of ordered pairs of natural numbers $\timeset_2$
and $\timeset_3$ a set of durations or temporal spans that is
isomorphic to the integers.
$\ftime$ contains the functions 
$\bbegin,\eend: \timeset_2 \mapsto \timeset_1,
-: \timeset_1 \times \timeset_1 \mapsto \timeset_3$ and
$\rtime$ contains relations like 
$<_1$ and $=_1$ for $\timeset_1$
$<_3$ and $=_3$ for $\timeset_3$
and the known qualitative interval relations like 
$\meets,\overlaps,\ldots\subseteq \timeset_2 \times \timeset_2$.
\item
{\bf Temporal Entities and Temporal Incidence Theory.}
We have two temporal entities:
\begin{enumerate}
\item {\em events} or {\em accomplishments}
that occur either at a time point i.e. one day,
or during a time span (several days)
and the occurrence is {\em solid}:
if it holds on a interval it does not hold on any interval that overlaps with it.
\item {\em fluents} 
that hold homogeneously throughout a number of days:
if it holds during an interval it also holds over any subinterval.
\end{enumerate}
\end{itemize}

We analyze the advantages and shortcomings of each method
according to a set of representational, computational and engineering criteria
Among the representation criteria,
we shall first look at the {\bf expressiveness} of the language.
In particular, 
it is important for our temporal qualification method to
be able to represent the various types of propositions
and axioms indicated in previous sections.
The comparison will be informal and illustrated by our example.
Second, we shall look at the {\bf notational efficiency}.
For a host of reasons, it is important that one is able to formalize knowledge 
into formulas that are compact, readable and elegant.
Third, it is desirable to have an {\bf ontology} that is clean and not
unnecessarily complex. One wants to make sure that one avoids undesirable entities in one's ontology.
For example, an ontology that requires one to postulate the existence of
both types and tokens is suspect.  On the other hand, one also wants to make
sure that the entities that one postulates in one's ontology are rich enough
to enable one to express whatever temporal knowledge one wants to express.
A second type of criteria are {\bf theorem proving} criteria
such as soundness and completeness of the proof theory,
efficiency of any theorem provers, as well as the possibility of 
using implementation technique to improve the efficiency of the theorem prover. 
Finally, we also bear in mind what one might call ``engineering criteria'',
such as {\bf modularity} of the method.
Often temporal reasoning is but one aspect of the reasoning 
that the system is expected to undertake.
For example, an autonomous agent needs to be able to reason not only
about time
but also about the intentions of other agents that it is likely to have to deal with.
It would therefore be advantageous 
if the method of temporal qualification allows one to extend the
reasoning system to include reasoning about other modalities as well.


% --------------------------------------------------------------------------
\section{Temporal Modal Logic}\label{ModalLogic}

One possible approach to temporal qualification in AI is the adoption of
modal temporal logic (\MTL).
We already briefly discussed modal temporal logic in
section \ref{TemporalQualificationinLogic}.
Moreover, there is a chapter in this handbook devoted to modal varieties
of
temporal logic by H. Barringer and D. Gabbay,
and our discussion of this approach is therefore extremely condensed.

\subsection{Definition}

Temporal modal logics are a special case of modal logic.
Starting with a normal first order logic, one adds a number of modal
operators, 
sentential operators which, in the case of temporal modal logic, 
change the time at which the proposition in its scope is claimed to be
true.
In other words, the problem of temporal qualification is dealt with
by putting a modal operator in front of a non-modal proposition.
For example, one may introduce a modal operator $P$ (``was true in the
Past'').
When applied to a formula $\phi$, the modal operator would change 
the claim that $\phi$ is true
at this moment in time to one which states that $\phi$ was true some
time 
in the past.  
Thus, the statement 
``SmallCo sent offer o1 to BigCo some time in the past''
would be represented as 
$
P\ \send( \smallco, o1, \bigco )
$.

Modal temporal logic, as traditionally defined by philosophical logicians,
is not particularly 
expressive.  In its simplest form, modal temporal logic only allows 
existential and universal quantification over the past and the future.  
In other words, in its simplest form, modal temporal 
logic contains only four modal operators, 
namely $P$ (``was true in the past''),
$H$ (``has always been true''), 
$F$ (``will be true sometimes in the future'')
and $G$ (``is always going to be true'').  
Clearly, this is insufficient for Artificial Intelligence, or indeed
Computer Science.
For example, none of the propositions in our example could be expressed
in such an expressive poor formalism.
It is for this reason that a number of authors (e.g., Fischer, 1991;
Reichgelt, 1989)
have introduced a number of additional modal operators,
such as \until, \since
and a model operator scheme \at,
which takes a name for a temporal unit as argument and returns a modal
operator.
Alternatively, one can, as Barringer and Gabbay do in an earlier chapter
in this handbook,
introduce a unary predicate $p()$ for each proposition $p$ in the
original -propositional- language
and stipulate that $p(t)$ holds if $p$ is true at time point $t$.
Thus, $p(t)$ is essentially a different notation for $\AT(t)p$.
One advantage of the $AT$ operator is that it is easier to see
how it can be used in a full first-order logic.

Modal temporal logic inherits its model theory from generic modal logic.
The standard model theory for such logics relies 
on the notion of a possible world, 
as introduced in this context by Kripke (1963).  
In Kripke semantics, primitive expressions, such as constants and
predicates,
are evaluated with respect to a possible world.
Non-modal propositions can then be assigned truth value with respect to
possible worlds
as in standard models for first-order logic.
The semantics for modal propositions is defined
with the help of an accessibility relation between possible worlds.
In modal temporal logic, an intuitive way of defining possible worlds
is as points in time, and the accessibility relation between possible
worlds
as an ordering relation between possible worlds.
We then say that for example the proposition $Pp$ is true
in a possible world $w$ if there is a possible world $w'$,
which is temporally before $w$ and in which $p$ is true.
With this in mind, the definition of the semantics for other modal
operators is relatively natural.

The only complication to this picture is caused 
by an introduction of a possible $AT$ operator scheme.
Since this operator requires a name for a temporal unit as an argument,
the language has to be complicated to include names for such temporal units,
and the semantics has to be modified to ensure 
that such temporal units receive their proper denotation.
Obviously, the most appropriate way to deal with this complication
is to assign possible worlds as the designation of names for temporal
units,
and to include an additional clause in the semantics that
states that the proposition $\AT(t)p$ is true
if $p$ is true in the possible world denoted by $t$.

\subsection{Analysis}\label{MTAnalysis}

We defined a number of representational desiderata on any temporal
logic.
One of the criteria is the {\bf notational efficiency}
(conciseness, naturalness, readability, elegance, \ldots).
Compared to other temporal formalisms discussed in this paper,
modal temporal logic scores well on this criterion
since the temporal operators produce concise and natural temporal expressions.
Another issue is the {\bf modularity} with respect to other knowledge modalities
such as knowledge and belief operators.
It is straightforward to combine the syntax and semantics of a modal
temporal logic with a modal logic to represent, say, knowledge.
Syntactically, such a change merely involves adding a knowledge modal
operator;
semantically, it involves adding an accessibility relation for this
new modality.
The model theory now contains two accessibility operators,
one used for temporal modalities, the other for epistemic modalities.

As far as cleanness of the {\bf ontology} is concerned,
the main concern is the notion of a possible world.
There is a significant amount of philosophical literature
on whether possible worlds are ontologically acceptable or suspect.
Without wanting to delve into this literature,
it seems to us that a possible world can simply be regarded as a model
for a non-modal first order language,
and that this makes the notion ontologically unproblematic.
There are of course additional arguments about the identity of
individuals across possible worlds,
but it again seems to us that this problem can be solved relatively
easily
by insisting that the same set of individuals be used for each possible
world.

Where modal temporal logic is less successful is in its ability to 
represent the various sentences and axioms in our example.
Let's consider few statements from our example.
To formalize the statement
``An offer becomes effective when is received by the offered
and continues to be so until it is accepted by the offered
or the offer expires''
we introduce several predicates.
Let
$E(x)$ denote ``the offer x is effective'',
$R(x)$ denote ``the offer x is received''
$A(x)$ denote ``the offer x is accepted''
and 
$X(x)$ denote ``the offer x expires''.
The classic since-until tense logic can be used to express the example
as
$$
\begin{array}{l}
\forall\ x_a,y_a,x_o\\
\hspace{0.5cm}[\ E(o(x_a,y_a,x_o))\since R(y_a, o(x_a,y_a,x_o)) \land \\
\hspace{0.5cm}E(o(x_a,y_a,x_o)) \until ( A(y_a,x_o(x_a,y_a,x_o)) \lor
  E(x_o(x_a,y_a,x_o)) )
]\end{array}
$$
The problem is that modal temporal logic does not allow one to quantify 
over occurrences of a particular event.
Thus, a proposition like 
"every time a company makes an offer, it is
committed to that offer
until it either expires or has been accepted" would be impossible to
express.

Although the semantics for modal temporal logics is well understood,
it has to be admitted that the implementation of {\bf automated theorem
provers} for modal temporal logic is not straightforward.  One could of
course try to adopt a theorem prover developed for general modal logic.  
However, such theorem provers in
general do not allow for particularly complex accessibility
relationships between possible worlds.
Most merely allow accessibility relations to be serial, transitive,
reflexive 
or some combination of these.
However, such properties are clearly not enough
if one were to introduce intervals as one's temporal units.
In other words, using a general theorem prover as a reasoning mechanism
for modal temporal logic
is only likely to be successful if one uses points as one's temporal
units.
A more promising approach would be to develop theorem provers specifically
for temporal modal logic
\comentari{
\cite{AbadiManna86} and \cite{Fisher91} are early attempt at doing so.
}
which is a topic of ongoing research as discussed on other chapters in this volume.


% --------------------------------------------------------------------------
\section{Temporal Arguments}\label{TemporalArguments}

The oldest and probably most widely used approach to temporal qualification
is the method of temporal arguments (\TA)
as introduced in section \ref{TemporalQualificationinLogic}.
The idea of the temporal arguments approach is to start with a
traditional logical theory but to add additional arguments to predicates and function symbols
to deal with time.
In order to reflect the fact 
that the domain now contains both ``normal individuals'' and times, 
the theory is often formulated as an instance of a  
{\em many-sorted first-order logic with equality}.

\subsection{Definition}

As stated in section \ref{FormalFramework}
we assume 
(i) a given time structure
$
\langle \timeset_1, \ldots ,\timeset_{n_t}, \ftime, \rtime \rangle
$
with a FOL time axiomatization
, and 
(ii) a classification of temporal entities $\{\tent_1,\ldots,\tent_{e_n}\}$
each class accompanied by a temporal incidence axiomatization.

Given these,
we define the temporal arguments method as a many-sorted logic with the time sorts 
$T_1, \ldots , T_{n_t}$, one for each time set,
and a number of non-time sorts $U_1, \ldots, U_n$.

\paragraph{Syntax.}
The vocabulary is composed of the following symbols:
\begin{itemize}

\item a set of function symbols 
$
{\bf F} = \{ f^{ \langle D_1,\ldots,D_n \mapsto R\rangle } \}
$.
If $n=0$, $f$ denotes a single individual from sort $R$,
otherwise $f$ denotes a function $D_1 \times \ldots \times D_n \mapsto
R$
and depending of the nature of the $D_i$,
we distinguish between:
\comentari{
$
{\bf F}=\mbox{\bf F}_{T} \cup \mbox{\bf F}_{Temp} \cup \mbox{\bf F}_{\infty}
$
}% end comentari
\begin{itemize}
\item {\em Time functions} $\funtime$
whose domain and range are time sorts.
\item {\em Temporal functions} $\funt$
whose range is a non-time sort and 
whose domain include both, time and non-time sorts.
\item {\em Atemporal functions} $\funat$
whose range is a domain sort and whose domain do not include any time sort.
\end{itemize}
Time, temporal and atemporal terms are defined in the usual way.

\item a set of predicates
${\bf P} = \{ P^{ \langle D_1,\ldots,D_n \rangle } \}$.
If $n=0$, $P$ denotes a propositional atom,
otherwise $P$ denotes a relation defined over $D_1, \ldots, D_n$
and depending on whether $D_i$ are time or a non-time sorts
we distinguish between:
\begin{itemize}
\item {\em Time predicates}  $\predtime$
whose arguments are all time sorts.
\item {\em Temporal predicates}  $\predt$
whose arguments include both time and domain sorts.
\item {\em Atemporal predicates} $\predat$
whose arguments do not include any time sort.
\end{itemize}
\item a set of variable symbols for each sort.
\end{itemize}
We have three classes of basic formula:
atomic temporal formula, atomic atemporal formula
and temporal constraints.

\paragraph{Semantics.}
The semantics is the standard semantics of many-sorted logics.
Notice that time gets full ontological status as we have one or more time sorts,
yet temporal entities and temporal formulas receive no special treatment.


\subsection{Formalizing the Example}\label{TAformalizing}

Having assumed the models of time and temporal incidence indicated in \ref{Introduction},
we define the following {\bf sorts}:
$\instants$ for time points,
$\intervals$ for time intervals, and 
$\tspans$ for time spans or durations,
$A$ for agents,
$O$ for legal objects,
$G$ for trading goods,
$S$ for legal status and 
$ \$ $ for money.
Our {\bf vocabulary} includes the following symbols:
\begin{itemize}
\item a set of constants for each sort:
day constants = $\{1/8/04, \now, \ldots \}$,
time interval constants = $\{ 3/04, 2004, \ldots \}$,
time span constants = $\{ 3d, 2w, 1y, \ldots \}$,
the constant \now,
agent constants = $\{\John, \Jane, \bigco, \smallco, \ldots\}$,
legal object constants = $\{o_1, o_2, \ldots\}$, 
etc.
\item 
the following sets of function symbols:
\begin{itemize}
\item $\funtime = 
\{ 
+_T^{\langle \instants, \tspans \mapsto \instants\rangle},
-_T^{\langle \instants, \instants \mapsto \tspans \rangle},
%\interval^{\langle \instants, \instants \mapsto \intervals \rangle},
\ldots
\}
$
\item $\funt = 
\{
\manager^{\langle \intervals, A \mapsto A\rangle} \}
$
\item $\funat =
\{
\sale^{\langle G, P \mapsto O \rangle},
\offer^{\langle A, A, O, \tspans \mapsto O \rangle}
\}
$
\end{itemize}

\item the following sets of predicates:
\begin{itemize}
\item $\predtime = 
\{ 
\leq^{\langle \instants, \instants \rangle},
=^{\langle \instants, \instants \rangle}, 
\ldots
\}
$
\item $\predt = 
\predevents \cup \predfluents$
\begin{itemize}
%\item {\em Objects}: $\offer^{\langle A, A, G, T, T, P, T, T\rangle}$
%(where the last two times denote the birth and death time of the offer), \ldots 
\item $\predevents = 
\{
\send^{ \langle \instants, A, A, O \rangle },
\receive^{ \langle \instants, A, O \rangle },
\accept^{ \langle \instants, A, O \rangle },
\\\hspace*{2cm}
\expire^{ \langle \instants, O \rangle }
\}$
\item $\predfluents =
\{
\effective^{\langle \instants, \instants, O \rangle},
\accepted^{\langle \instants, \instants, O \rangle},
\\\hspace*{2cm}
\expired^{\langle \instants, \instants, O \rangle}
\}$
\end{itemize}
\item $\predat = 
\{
\correctform^{\langle O \rangle},
\leq_{\$}^{\langle P, P\rangle}
\mbox{(that denotes the $\leq$ relation between prices)}
\}$
\end{itemize}
\item
and a set of variable symbols for each sort.
%${\bf V}_T = \{ x_t, y_t, \ldots \}$, 
%${\bf V}_A = \{ x_a, y_a, \ldots \}$, \ldots
\end{itemize}
\noindent The statements in the example can be formalized as follows:
\begin{enumerate}
\item
``On 1/4/04 SmallCo sent an offer to BigCo for selling goods $g$ 
for price $p$ with a 2 weeks expiration interval.''\\
$\hspace*{0.5cm}
  \send(1/4/04, \smallco, \bigCo, \offer(\smallco, \bigco, \sale(g, p), 2w))
$
\item
``BigCo received the offer three days later and it has been effective
since then.''\\
$\hspace*{0.5cm}
  \receive(1/4/04+3d, \bigCo, \offer(\smallco,\bigco,\sale(g,p),2w))\ \land
\\\hspace*{0.5cm}
  \effective(1/4/04+3d, \now, \offer(\smallco,\bigco,\sale(g,p),2w))
$
\item
``A properly formalized offer becomes effective when it is received by
the offered ...''\\
$
\forall\ t_1:\instants,
x_a,y_a:A, x_o: O, ts:\tspans, 
\\\hspace*{0.5cm}
  [\ \correctform(\offer(x_a,y_a,x_o,ts))\ \land \
  \receive(t_1, y_a, \offer(x_a,y_a,x_o,ts)\ \limplies 
\\\hspace*{0.5cm}
  \exists t_2:\instants\ 
  [\ \effective(t_1, t_2, \offer(x_a,y_a,x_o,ts)\ \land\ t_1\leq t_2\ ]
\\\hspace*{0.5cm}]
$
\item
``\ldots (an effective offer) continues to be so until
it is accepted by the offered
or the offer expires (as indicated by its expiration interval).''\\
$
\forall\ t_1,t_2:\instants, x_a,y_a:A, x_o:O, ts:\tspans
\\\hspace*{0,5cm}
  [\ \effective(t_1, t_2, \offer(x_a,y_a,x_o,ts)) \land t_1 \leq t_2 \limplies
\\\hspace*{0,5cm} \exists t_3:\instants\ 
[ \accept(t_3,y_a,\offer(x_a,y_a,x_o,ts)) \land t_1 < t_3 \leq t_1+ts]\ \lor
\\\hspace*{0,5cm}
  (t_2=t_1+ts \land \expire(t2,\offer(x_a,y_a,x_o,ts)))
\\\hspace*{0,5cm}]
$
\item 
``Anybody who makes an offer is committed to the offer as long as the
offer is effective.''\\
$
\forall\ t_1,t_2:\instants, x_a:A
\\\hspace*{0.5cm}
[\
  \effective(t_1,t_2, \offer(x_a,\_,\_,\_)) \limplies
  \committed(t_1,t_2, x_a, \offer(x_a,\_,\_,\_))
\ ]
$
\item
``Anybody who receives an offer is obliged to send a confirmation
to the offerer within two days.''\\
$
\forall\ t:\instants, x_a,y_a:A, x_o:O
\\\hspace*{0,5cm}
[\
  \receive(t,y_a,x_a,x_o) \limplies
  \obliged(t, t+2d, y_a, ??? )
\ ]
$
\end{enumerate}
\noindent The ``???'' in the last formula indicates that it is not
clear how to express that $y_a$ is obliged to 
``send a confirmation of $x_o$ to $x_a$'' 
since in standard FOL we cannot predicate or quantify over
propositions\footnote{The reader might come up with the idea of
 turning temporal predicates into terms in order to be able to take
 them as proper predicate arguments.
This is the idea of temp. reified logics that we discuss below.}.
Besides this example, 
there are few additional general statements whose formalization is
interesting to consider:
\begin{enumerate}
\item %1
Time axioms: ``The ordering between instants is transitive'':\\
$
\hspace*{0,5cm}
  \forall\ t_1,t_2,t_3:\instants\
[\ 
t_1 \leq t_2 \land t_2 \leq t_3 \limplies t_1 \leq t_3
\ ]
$
\item %2
Temporal Incidence axioms such as ``Fluents hold homogeneously'':\\
$
\hspace*{0,5cm}
  \forall\ t_1,t_2,t_3,t_4:\instants, x_1:S_1, \ldots , x_n:S_n,
\\\hspace*{1cm}
[\
  P( t_1, t_2,x_1, \ldots ,x_n) \land
  t_1 \leq t_3 \leq t_4 \leq t_2 \land
  t_1 \neq t_4 \limplies
  P( t_3, t_4, x_1, \ldots ,x_n)
\ ]
$

\noindent This an ``axiom schema'' that is a shorthand for a potentially large
set of axioms, one for each fluent predicate $P$ in the language.
\end{enumerate}

\noindent The previous examples are instances of relations holding between
temporal entities, which can be important in some applications.
In common-sense reasoning and planning, for instance,
it is important to specify the $\cause$ relationship:
\begin{quote}
``Whenever an offer is effective it {\em causes} the agent who made the
offer to be committed to it as long as the offer is effective.''
\end{quote}
Again, 
it is not clear how to express this piece of knowledge in the method
of temporal arguments since it requires the predicate
$\causes$
to take as argument the proposition
$\effective(t_1, t_2, \offer(x_a,y_a,x_o,ts))$
which is beyond standard many-sorted FOL.
A similar problem arises we attempt to formalize the following properties:
\begin{itemize}
\item %6
``Whenever a cause occurs its effects hold.''
\item %7
``Causes precede their effects.''
\comentari{
\item %8
``Being effective and expired are incompatible status for an offer.''
\item %9
``Incompatible fluents do not overlap in time.''
}% end comentari
\end{itemize}


\subsection{Theorem Proving} % --- --- --- ---

Defining a temporal logic as a standard many-sorted logic has the advantage 
that we can use the various deductive systems available 
for many-sorted logics \cite{Cohn87,Walther87,Manzano93,Cimattietal98}.
However, we must bear in mind that,
while many-sorted logics often allow one to delete sortal axioms,
such as ``All offers are legal documents'',
the inclusion of a number of time
sorts and predicate symbols with a specific meaning
(as determined by the properties of the model of time adopted)
requires one to add a potentially large number of axioms
that capture the nature of the temporal incidence theory.
Moreover, it may be impossible to define a set of axioms
that completely capture our time structure. 
For instance, we have taken the ``set of integers'' as our duration subdomain.
But it is well-known  that there is no complete axiomatization of
the integers in first-order logic if the language includes addition.
Therefore, it is important to choose a temporal structure that can be
characterized fully in first-order logic, such as 
{\em ``unbounded linear orders''},
{\em ``totally ordered fields''} or
some of the theories discussed in chapter ``Theories of Time and Temporal
Incidence''.

Having a complete axiomatics and therefore a complete proof
theory, though, is merely the beginning of the story.
Time axioms can be a heavy load for our theorem prover
as they often lead to a significant increase in the size of the search space.
This problem may lead to the unavoidable effort of developing an
specialized temporal theorem prover.

\subsection{Analysis}\label{TAAnalysis}

The method of temporal arguments has a number of advantages 
over other approaches to temporal qualification.
First, the {\bf ontology} that one is committed to is relatively straightforward.
In addition to ``normal'' objects, 
one merely has to add time objects to one's ontology.
Compared to the ontologies that underlie the other approaches to
temporal quantification, the ontology is both parsimonious and clean.
Moreover, again in contrast with some of the approaches discussed in this chapter,
the system does not make any ontological commitments itself,
and one is therefore completely free to make the ontology
as parsimonious as the application allows.

Second, despite it seeming simplicity,
the {\bf expressive power} of languages embodying 
the temporal arguments approach exceeds 
that of many other approaches to temporal quantification.
The inclusion of additional temporal arguments in predicate and function symbols
allows one both to express information about individuals 
and their properties at specific times and to quantify over times.
Moreover, it is straightforward to include purely temporal axioms explicitly in one's theories.
However, this is not to say that the method of temporal arguments gives one
all the desired expressive power.
For example, as we indicated in the previous section,
since it stays within the expressive limitations of first-order logic,
it is not possible to express temporal incidence properties for all
temporal entities in class (fluents, events and so on)
or any other property or relation about temporal entities
such as ``event e at time t causes fluent f to be true at time t''.

Third, the {\bf notation} is perhaps not as efficient 
as some of the alternatives, specifically modal logic.
Many of the modal temporal operators 
are a notational shortcut for existential or universal quantification.
For example, the modal operator $F$ provides an existential quantification over future times.
Since no such notational shortcuts exist in systems based on the method of temporal arguments,
the expression of sentences becomes more tedious in such systems.
This is true in particular of sentences that require embedded temporal quantification,
such as ``The contract will have been signed by then''.

Fourth,
as we already indicated in the previous section,
the fact that the method of temporal arguments is based on a standard
first-order logic 
means that one can use the tried and tested {\bf theorem proving} methods
for such systems,
which is not the case of methods based on a temporal logic with 
a non-standard temporal semantics.
Moreover, setting up the system as an instance of a multi-sorted logic
allows one to take advantage of the more efficient theorem provers developed for such logic.
However, it is important to mention that the fact that one is forced to include
explicit axioms describing temporal structures in one's theories
has detrimental effects on the performance of the actual theorem provers.
Many of the additional axioms lead to an combinatorial explosion of the search space
and therefore significantly increase the time required to find a proof.
For example, some axioms, such as for every point in time, there is a later point in time,
are recursive and, unless carefully controlled, lead to an infinite search space.
We discuss some approaches that can be used to address some of these issues below.

Finally, since the arguments  that are added to the predicate and function symbols 
denote time, the method of temporal arguments does not easily lend itself
to the {\bf modular} inclusion of other modalities, such as epistemic or deontic modalities.

The methods that we discuss below
have been developed to overcome some of the shortcomings associated with the method of
temporal arguments.
One way of increasing the expressive power of the formalism
without moving to a higher-order logic
is through the addition of some vocabulary and 
a complication in the ontology.
The {\em temporal token arguments} is one such approach.


% --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- 
\section{Temporal Token Arguments}\label{TemporalTokenArguments}

The temporal token argument method (\TTA)
was introduced in the early AI temporal databases such as the
{\em Event Calculus} \cite{KowalskiSergot86}
and Dean's {\em Time Map Manager} \cite{DeanMcDermott87}
and later presented in \cite{Galton91} in deeper detail.
It is based on the simple idea,
common in the database community,
of introducing a key to identify every tuple in a relation.
Here, a tuple of a temporal relation represents
an instance of that relation holding at a particular time or time span.
Therefore, we introduce a key that identifies
a temporal instance of the relation, namely a {\bf temporal token},
which shall receive full ontological status.

\subsection{Definition}

For a given time structure
$
\langle {\cal T}_1, \ldots ,{\cal T}_{n_t}, {\cal F}_T, {\cal R}_T\rangle
$
and a given set of {\em temporal entities}
$
\{ {\cal E}_1, \ldots , {\cal E}_{n_e} \}
$,
we define a standard many-sorted first order language with the
following {\em sorts}: 
one time sort $T_1,\ldots,T_{n_t}$ for each set of time objects,
a number of non-time sorts $U_1, \ldots, U_n$
and one token sort $E_1,\ldots, E_{n_e}$ for each temporal entity.


\paragraph{Syntax.}
It is very similar to the temporal arguments method
but instead of having extra time arguments in our temporal predicates,
the extra argument is a single {\em temporal token} term.
In turn token terms are taken as arguments by
(i) time functions,
and
(ii) temporal incidence predicates that we introduce below.
 
The vocabulary is extended accordingly:
\begin{itemize}
\item
{\em Function symbols}:
In addition to the function symbol sets in temporal arguments,
we have a set of {\bf time-token} functions
(not to be confused with time functions)
that map tokens to their relevant times,
for example the function 
$\interval: \tokens \mapsto \intervals$ 
that returns the time interval associated with a given token.
\item
{\em Predicate symbols}:
{\em Temporal predicates} no longer have any time argument,
but instead have a single token argument from the sort 
of the temporal entity denoted by the temporal predicate.
Thus,
$\effective(t_1, t_2, \offer(\_))$
becomes
$\effective(tt_1, \offer(\_))$ where $tt_1$
is a constant symbol of the new $\fluents$ sort.

{\em Time} and {\em Atemporal predicates} remain the same.
We incorporate one new {\bf Temporal Incidence Predicate (TIP)}\footnote{TIPs actually are atemporal if we look at the definition we have given to this term.}
for each temporal entity ${\cal E}_i$
which takes as sole argument a term of the temporal sort $E_i$.
Given our temporal ontology we shall have 2 TIPs:
$\holds(\mbox{\it fluent token})$ expresses that the fluent token holds
throughout the time interval associated to it that is denoted 
by the term $\interval(tt_1)$
and $\occurs(\mbox{\it event token})$ for event occurrence.
\end{itemize}


\paragraph{Semantics.}
The standard many-sorted first-order semantics is preserved
with both time domains, non-time domains and temporal token domains
with the usual interpretation of function and predicate symbols.
Time and temporal incidence theories are incorporated as a set of first order axioms.


\subsection{Formalizing the Example}\label{TTAformalizing}

We illustrate the approach by formalizing the example.
We make the same assumptions as before and 
we will frequently refer to the formalization of this example in the temporal arguments method.

In addition to the {\bf sorts} defined in the \TA\ example
we introduce sorts for tokens of each temporal entity: 
$\events$ for event tokens and $\fluents$ for fluent tokens.
In turn, our vocabulary will include event token constants
and fluent token constants.
Besides the usual functions,
we have the following {\bf time-token functions}:
$\ttime(\mbox{\em token})$ denotes the time of an instantaneous temporal token,
$\bbegin(\mbox{\em token})$ denotes the initial instant of a temporal token,
$\eend(\mbox{\em token})$ denotes the ending instant
and
$\interval(\mbox{\em token})$ the time interval of the token.

In addition to the time and atemporal predicates from the previous
formalization, the {\em temporal predicates} now are as follows:
\begin{itemize}
\item {\em Events}: 
$\send^{ \langle \events, A, A, O \rangle }$
(where the last argument denotes the event token of this particular send event),
$\receive^{ \langle \events, A, A, O \rangle }$,
and $\accept^{ \langle \events, A, O \rangle }$.
\item {\em Fluents}: 
$\effective^{ \langle \fluents, O \rangle }$
(where the first argument denotes the fluent token of a particular
period where the legal object $O$ is effective),
$\accepted^{ \langle \fluents, O \rangle }$
and\\ $\expired^{ \langle \fluents, O \rangle }$.
\end{itemize}

As in the \TA\ method, we have four classes of basic formula:
atomic atemporal formula,
atomic temporal formula,
temporal constraints
and temporal incidence formula.

\noindent The statements in the example can be formalized as follows:
\begin{enumerate}
\item
``On 1/4/04, SmallCo sent an offer to BigCo
for selling goods $g$ for price $p$ with a 2 weeks expiration interval.''\\
$
\hspace*{0.5cm}
  \send(s_1,\smallco,\bigco,\offer(\smallco,\bigco,\sale(g,p),2w))\ \land
  \ \occurs(s_1) \land \ttime(s_1,1/4/04)
$
\item
``BigCo received the offer three days later and it has been effective
since then.''\\
$\hspace*{0.5cm}
  \receive(r_1,\bigCo,\offer(\smallco,\bigco,\sale(g,p),2w))\
  \land
  \occurs(r_1)\ \land\ 
\\\hspace*{0.5cm}
  \ttime(r_1)=1/4/04+3d\ \land
\\\hspace*{0.5cm}
  \effective(e_1, \offer(\smallco, \bigco, \sale(g,p), 2w))\ \land\ \holds(e_1)\ \land
\\\hspace*{0.5cm}
  \ttime(r_1)=\bbegin(e_1)\ \land\ \eend(e_1)=now
$
\item
``A properly formalized offer becomes effective when is received by
the offered ...''\\
$
\forall\ tt_1:\events, ts:\tspans, x_a,y_a:A,\ x_o:O
\\\hspace*{0.5cm}
  [\ \correctform(\offer(x_a, y_a, x_o, ts))\ \land\ 
\\\hspace*{0.5cm}
  \receive(tt_1, y_a, x_a, \offer(x_a, y_a, x_o, ts))
  \ \land\ \occurs(tt_1)\ \limplies 
\\\hspace*{0.5cm}
  \exists\ tt_2:\fluents
\\\hspace*{1cm}[\
    \effective(tt_2, \offer(x_a, y_a, x_o, ts))\ \land\ \holds(tt_2)
    \ \land\ tt_1\ \meets\ tt_2\ ]
\\\hspace*{0,5cm}]
$
\item
``\ldots (an effective offer) continues to be so until
it is accepted by the offered
or the offer expires (as indicated by its expiration interval).''\\
$
\forall\ tt_1:\fluents, x_a,y_a:A,\ x_o:O,\ ts:\tspans
\\\hspace*{0.5cm}
  [\ \effective(tt_1,\offer(x_a,y_a,x_o,ts))\ \land\ \holds(tt_1)\ \limplies
\\\hspace*{0.5cm}
  \exists tt_2:\events\ 
\\\hspace*{1cm}
    [ \accept(tt_2,y_a,\offer(x_a,y_a,x_o,ts))\ \land\ \occurs(tt_2)\land
\\\hspace*{1cm}
    \bbegin(tt_1) < \ttime(tt_2) \leq \bbegin(tt_1)+ts ]
\\\hspace*{0,5cm}\lor
\\\hspace*{0,5cm}
  (\eend(tt_1)=\bbegin(tt_1)+ts\ \land\ 
\\\hspace*{0,5cm}
    \exists tt_2:\events\ 
\\\hspace*{1cm}[\expire(tt_2,\offer(x_a,y_a,x_o,ts))\
    \land\ \occurs(tt_2) \land
\\\hspace*{1cm}\eend(tt_1)=\ttime(tt_2)])
\\\hspace*{0,5cm}]
$
\item 
``Anybody who makes an offer is committed to the offer as long as the
offer is effective.''\\
$
\forall\ tt_1:\fluents, x_a,y_a:A, x_o:O, ts:\tspans
\\\hspace*{0,5cm}
[\ \effective(tt_1, \offer(x_a,y_a,x_o,ts)) \land \holds(tt_1)\ \limplies 
\\\hspace*{0,5cm}
  \exists\ tt_2:\fluents\ 
\\\hspace*{1cm}
    [\ \committed(tt_2, x_a, \offer(x_a, y_a, x_o, ts)) \land 
    \holds(tt_2)\ \land 
\\\hspace*{1cm}
    \interval(tt_1)=\interval(tt_2)\ ]\ ]
$
\item
``Anybody who receives an offer is obliged to send a confirmation
to the offerer within two days.''\\
$
\forall\ tt_1:\events, x_a,y_a:A, x_o:O, ts:\tspans  
\\\hspace*{0,5cm}[\
  \receive(tt_1,y_a,\offer(x_a,y_a,x_o,ts))\land\occurs(tt_1)\limplies
\\\hspace*{0,5cm}\exists tt_2:\events
\\\hspace*{1cm}
    [\obliged(x_a, tt_2) \land \send(tt_2, y_a, x_a, \conf(x_o))\ \land
\\\hspace*{1cm}
    \ttime(tt_1)\leq \ttime(tt_2) \leq \ttime(tt_1)+2d \ ]\ ]
$
\end{enumerate}
\noindent Observe that we express that $x_a$ is obliged to a temporal
proposition by using a temporal token of that proposition.
In general,
the additional flexibility of temporal tokens allows us 
(i) to talk about temporal occurrences that may or may not happen,
and 
(ii) to express that an agent is obliged to that event.
This is not possible in the \TA\ method.

\noindent Let's see how the more general statements are formalized:
\begin{itemize}
\item %1
Time axioms are expressed as usual:\\
$\hspace{0.5cm}
\forall\ t_1,t_2,t_3:\instants
[\
t_1 \leq t_2 \land t_2 \leq t_3 \limplies t_1 \leq t_3
\ ]
$
\item %2
Temporal Incidence axioms become more compact since
we can quantify over all the instances of a given entity 
(e.g. all fluents) independently of their particular meaning.
It is no longer necessary to have an ``axiom schema''.
For instance the ``homogeneity of fluent holding'' is stated by:\\
$\hspace{0.5cm}
\forall\ tt:\fluents, I:\intervals\ 
[\ 
holds(tt) \land I \subseteq \interval(tt) \limplies \holdson(tt,I)
\ ]
$
\item
``It is necessary for an offer to be properly written to be effective''.\\
$
\forall\ tt:\fluents, x_o:O\
[ \effective(tt,x_o)\land\holds(tt) \limplies \correctform(x_o) ]
$
\item
``Whenever an offer is effective it {\em causes} the agent who made the
offer to be committed to it for as long as the offer is effective.''\\
$\forall\ tt_1:\fluents, x_a,y_a:A, x_o:O,ts:\tspans
\\\hspace*{0,5cm}
  [\ \effective(tt_1,\offer(x_a,y_a,x_o,ts)) \land \holds(tt_1) \limplies
\\\hspace*{0,5cm}
  \exists tt_2:\fluents
\\\hspace*{1cm}[\ \cause(tt_1,tt_2) \land  
    \committed(tt_2,\offer(x_a,y_a,x_o,ts))\land
    \interval(tt_1,tt_2)\ ]\ ]
$
\item
``Whenever a cause occurs its effects hold.''\\
$\forall\ tt_1:\events, tt_2:\fluents
\\\hspace*{0,5cm}[ \occurs(tt_1)\land\cause(tt_1,tt_2)\limplies\holds(tt_2)]
$
\item
``Causes precede their effects.''\\
$\forall\ tt_1:\events, tt_2:\fluents
\\\hspace*{0,5cm}
  [\ \cause(tt_1,tt_2) \limplies 
    ( \occurs(tt_1) \limplies \holds(tt_2) \land \ttime(tt_1) \leq \bbegin(tt_2)\ ]
$
\end{itemize}


\subsubsection{Token Incidence Theory}

The specific semantics of temporal tokens
may yield some additional temporal incidence axioms.
An example is the so-called ``maximality of fluent tokens''. 
For practical reasons, one is interested in adopting the following convention:
\begin{quote}
``A fluent token denotes a {\em maximal} piece of time where that fluent is true.''
\end{quote}
A consequence of this is the following property
``Any two intervals associated with the same fluent are either identical
or disjoint.''
Thus,
in practice in can be interesting to define some additional incidence
predicates
such as 
$\holdsat^2$ and 
$\holdson^2$
which are shorthands for
$$
\begin{array}{l}
\holdsat(\mbox{\it fluent}, t)\equiv\exists f: \fluents\ 
  (fluent(f) \land \holds(f) \land i \in \interval(f))
\\
\holdson(\mbox{\it fluent}, I)\equiv\exists f: \fluents\
  (fluent(f) \land \holds(f) \land I \subseteq \interval(f))
\end{array}
$$
respectively, where $f$ is a variable of the {\em fluent token} sort
$\fluents$ and 
$fluent(f)$ denotes the atomic proposition fluent with the extra
temporal token argument $f$.


\subsection{Analysis}\label{TTAAnalysis}

The temporal token arguments method has several advantages.
The extra objects (the temporal tokens) introduced in the language
gives the {\bf notation} an increased flexibility
that helps overcome some of the expressiveness problems that we
identified in the temporal arguments method:
First,
as temporal tokens are used as argument of other predicates
it is useful to express nested temporal references as shown by the example.
Second, different levels of time are supported by diversifying the time-token functions. 
For instance, we may have 
$\bbegin_{\mbox{v}}(tt_1)$ to refer to {\em valid time} and
$\bbegin_{\mbox{t}}(tt_1)$ to refer to {\em transaction time}.
Third, 
at the implementation level, 
a different temporal constraint network instance is maintained for
each time level. Every temporal term will be mapped to a node in its corresponding constraint network.

However, the increased notation flexibility causes the notation to be
more baroque and sometimes awkward (compare the formalization of our
example here with the formalizations obtained by other methods).
To improve notational {\em conciseness} we can define some syntactic sugar 
that allows the omission of token symbols whenever they are not
strictly necessary. % ***expand

Another advantage of this approach is its {\bf modularity}.
A clear separation is made between the temporal and other information
as a atomic temporal formulas are linked to time through time-token functions
like \bbegin\ and \eend.
However, token symbols can also be used as the link to other
modalities
as the deontic modalities of commitment and obligation illustrated by the example.

% --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- ---
\comentari{***
\section{Non-standard Temporal Arguments}\label{NSTemporalArguments}
An alternative is moving to a non-standard semantics that incorporates 
a model of time 
and developing a new proof theory that is complete for that semantics.
}

% --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- --- ---
\section{Temporal Reification}\label{TemporalReification}

Temporal reification (\TR) was motivated by the desire to
extend the expressive power of the temporal arguments approach
while remaining within the limits of first order logic.
It is achieved by: 
(i) complicating the underlying ontology
and 
(ii) representing temporal propositions
as terms in order to be able to predicate and quantify over them. 

In essence, in reified temporal logic, 
both time objects and temporal entities receive full ontological status
and one introduces in the language terms referring to them.
The {\em Temporal Incidence Predicates}
are used to associate a temporal entity with its time of occurrence
and allow a direct and natural axiomatization of the 
given temporal incidence properties, 
as illustrated in the example below.


\paragraph{Syntax.}
Reified temporal logics are in fact relatively straightforward to
construct from a standard first order language.
First, it is useful to
move to a sorted logic in which we make a distinction between temporal
entities, normal individuals and temporal units.
Second, for each
$n$-place function symbol in the first order language, one introduces a
corresponding $n$-place function symbol in the reified language.  Its
sortal signature is that it maps $n$ normal individuals into a normal
individual.  For each $n$-place predicate in the original language, one
also introduces a $n$-place function symbol in the language.  However, its
sortal signature is different.  It takes as input $n$ normal individuals
and maps them into a temporal entity.  

\paragraph{Semantics.}
Interestingly, not many authors worried about providing a
clear model-theoretic semantics for their formalism, either because they
were not interested in doing so, or because they believed that reified
temporal logic would simply inherit its semantics from first order
predicate calculus.  It was not until \cite{Shoham87b} that the
semantics of reified temporal logics became an issue.  Shoham observed
that reified temporal logic are very similar to formalizations of the
model theory for modal temporal logic in a first order logic and proposed
to formulate the semantics for reified temporal logic in these terms.
It is not clear that the actual framework proposed by Shoham actually
achieved this.
For example, \cite{VilaReichgelt96} argue that Shoham's
formalism is more appropriately regarded as being a hybrid between
a modal temporal logic and a system in the tradition of the
temporal arguments method.
As a matter of fact, Shoham's is subsumed by the \TA\ method\cite{Bacchusetal91}.
Nevertheless, Shoham's insight was the inspiration for Reichgelt
\cite{Reichgelt89} who indeed formulated a reified temporal logic.


\subsection{Formalizing the Example}\label{TRformalizing}

Let's see how this method is used to formalize our example.
We make the same assumptions and 
we shall be continuously referring
to the formalization of this example made with the temporal arguments method.

Besides the {\bf sorts} 
$T_i$ for time instants,
$T_I$ for time intervals,
$A$ for agents, etc.
we now have additional sorts,
one for each temporal entity: 
$\events$ for events and $\fluents$ for fluents.
Our {\bf vocabulary} is composed of:
\begin{itemize}
\item For each sort, a set of constant symbols,
including event constants
and fluent constants.

\item We have time, temporal and atemporal function symbols as in the
  temporal arguments approach
except that the set of temporal functions 
(where we have functions like $\offer^{\langle A, A, O, T \mapsto O\rangle}$)
is extended with new temporal functions produced by temporal
reification, one for each temporal relation 
(which in the temporal arguments is represented by a temporal predicate):
\begin{itemize}
\item $\events = 
\{
\send^{\langle A, A, O \mapsto \events \rangle},
\receive^{\langle A, O \mapsto \events \rangle},
\accept^{\langle A, O \mapsto \events\rangle}, \\
\hspace*{2cm}\expire^{\langle O \mapsto \events\rangle}
\}$
\item $\fluents =
\{
\effective^{\langle O \mapsto \fluents \rangle}, \ldots
\}$
\end{itemize}

\item the following sets of predicates:
\begin{itemize}
\item $\predtime =
\leq^{\langle T, T\rangle}, =^{\langle T, T\rangle}, \ldots$

\item $\predat = 
\leq_{\$}^{\langle P, P\rangle}$
(that denotes the $\leq$ relation between prices).
\end{itemize}

\item and a set of variable symbols for each sort.
\end{itemize}

\noindent The statements in the example may be formalized as follows:
\begin{enumerate}
\item
``On 1/4/04, SmallCo sent an offer to BigCo for selling goods $g$ for
price $p$ with a 2 weeks expiration interval.''\\
$\hspace*{0.5cm}
\occurs(1/4/04,\send(\smallco,\bigco,\offer(\smallco,\bigco,\sale(g,p),2w)))
$
\item
``BigCo received the offer three days later and it has been effective
since then.''\\
$\hspace*{0.5cm}
\occurs(1/4/04+3d,
  \receive(\bigCo,\offer(\smallco,\bigco,\sale(g,p),2w)))\land
\\\hspace*{0.5cm}
  \holds(1/4/04+3d,now,
  \effective(\offer(\smallco, \bigco,\sale(g,p), 2w))) 
$
\item
``A properly formalized offer becomes effective when is received by
the offered ...''\\
$
\forall\ t_1:\instants, x_a,y_a:A,
\\\hspace*{0.5cm}
  [\ \correctform(\offer(x_a,y_a,\_,\_))\ \land 
  \occurs(t_1, \receive(y_a,\offer(x_a,y_a,\_,\_)))\ \limplies 
\\\hspace*{0.5cm}
  \exists t_2:\instants\ [\ \holds(t_1,t_2,\effective(\offer(x_a,y_a,\_,\_)))]
\\\ ]
$
\item 
``\ldots (an effective offer) continues to be so until
it is accepted by the offered
or the offer expires (as indicated by its expiration interval).''\\
$
\forall\ t_1, t_2:\instants, x_a,y_a:A, x_o:O, ts:\tspans
\\\hspace*{0,5cm}
  [\ \holds(t_1, t_2, \effective(\offer(x_a,y_a,x_o,ts)))\ \limplies
\\\hspace*{0,5cm}
  \exists t_3:\instants\ [t_1 < t_3 \leq t_1+ts \land \occurs(t_3, \accept(y_a,x_o)) ]\ \lor
\\\hspace*{0,5cm}
  ( t_2=t_1+ts \land \occurs(t_2,\expire(offer(x_a,y_a,x_o,ts))))
\\\hspace*{0,5cm}]
$
\item 
``Anybody who makes an offer is committed to the offer as long as the
offer is effective.''\\
$
\forall\ t_1,t_2:\instants, x_a:A, x_o:O
\\\hspace*{0,5cm}[\
  \holds(t_1, t_2, \effective(\offer(x_a,\_,\_,\_))) \limplies 
\\\hspace*{0,5cm}
  \holds(t_1, t_2, \committed(x_a, \offer(x_a,\_,\_,\_)))
\ ]
$
\item
``Anybody who receives an offer is obliged to send a confirmation
to the offerer within two days.''\\
$
\forall\ t:\instants, x_a,y_a:A, x_o:O,
\\\hspace*{0,5cm}
[
  \occurs(t, \receive(y_a, \offer(x_a,y_a,x_o,\_))) \limplies
\\\hspace*{0,5cm}
  \holds(t, t+2d, \obliged(y_a, send(y_a,x_a,\conf(\offer(x_a,y_a,x_o,\_)))))
]
$
\end{enumerate}

\noindent Now last formula is legal but still the formalization we have is not that clear.
It expresses that the obligation holds between $t$ and $t+2d$
but indeed it is ``sending the confirmation'' that 
must be between $t$ and $t+2d$.
Next, let's see how the more general statements are formalized:
\begin{itemize}
\item %1
Time axioms are expressed as usual:\\
$
\forall\ t_1,t_2,t_3:\instants\
[\
t_1 \leq t_2 \land t_2 \leq t_3 \limplies t_1 \leq t_3 
\ ]
$
\item %2
Temporal incidence axioms become more compact since
we can quantify over all the instances of a given entity 
(e.g. all fluents) independently of their particular meaning
(and it is no longer necessary to have an ``axiom schema'').
For instance the ``homogeneity of fluent holding'' is stated as:\\
$
\forall\ t_1,t_2,t_3,t_4:\instants, f:\fluents
\\\hspace*{0.5cm}
[\ \holds(t_1,t_2,f) \land 
  t_1 \leq t_3 \leq t_4 \leq t_2 \land
  t_1 \neq t_4 \limplies
  \holds(t_3,t_4,f)
\ ]
$
\item
``It is necessary for an offer to be properly written to be effective''.\\
$
\forall\ t,t':\instants, x_o:O\
\ [ \holds(\effective(t,t',x_o)) \limplies \correctform(x_o) ]
$
\item
``Whenever an offer is effective it {\em causes} the agent who made the
offer to be committed to it for as long as the offer is effective.''\\
$
\forall\ t_1,t_2:\instants, x_a,y_a:A, x_o:O,ts:\tspans
\\\hspace*{0,5cm}
[\ 
\cause( 
  \effective(t_1,t_2,\offer(x_a,y_a,x_o,ts)), 
  \committed(t_1,t_2,x_a,\offer(x_a,y_a,x_o,ts)))
\ ]
$
\item
``Whenever a cause occurs its effects hold.''\\
$
\forall\ e:\events, f:\fluents\
[\ \occurs(e) \land \cause(e,f) \limplies \holds(f)\ ]
$
\item
``Causes precede their effects.''\\
$\forall\ e:\events, f:\fluents
\\\hspace*{0,5cm}
  [\ \cause(e,f) \limplies (\occurs(e) \limplies \holds(f) \land
  \ttime(e) < \bbegin(f))\ ]
$
\end{itemize}


\subsection{Full Temporal Reified Logic}

Implicitly in the previous section we have restricted ourselves to
reification of atomic propositions,
but we can push it further and reify also non-atomic propositions
(as first discussed in \cite{McDermott82,Allen84}).
This can be motivated by statements like the following: 
\begin{enumerate}
\item
``The offer \ldots has been sent but not effective from $t_1$ to $t_2$''.
$
\holds( t_1,t_2,\sent(o_1)\land\lnot\effective(o_1)
$
\item
``From $t_1$ to $t_2$ all offers offered by agent $a_1$ have been frozen.''
$
\holds(t_1,t_2, \forall x_a:A, x_o:O, ts:\tspans\
  [ frozen(\offer(a_1,y_a,x_o,ts)) ]
$
\item
``As of 1/may/04, when an offer is sent the offerer will have to pay a
tax within the next 3 days.''
$
\holds(1/may/04,+\infty,
  \forall x_a,y_a:A, x_o:O, ts:\tspans\
  [ send(x_a,y_a,\offer(x_a,y_a,x_o,ts))
  \limplies 
  Obligation(pay(x_a,tax),t?,t?)
  ]
$
\end{enumerate}

{\em Reichgelt's reified temporal logic}
takes as its starting point modal temporal logic,
and the observation that the semantics for such logics can itself
relatively straightforward be formalized in a first-order language.
This language, however, becomes rather baroque
as it needs to include terms to refer both to semantic entities
and terms to refer to the expressions in the modal temporal logic.
Thus, a full reified logic would need to codify such statements
as ``Fp(a) is true at time t if and only if there is a time t' later than t 
at which the individual denoted by a is an element of the set denoted by P''
and this requires the full reified logic to have expressions
to refer to times (``t, t' ''), expressions to refer to individuals (``the individual denoted by a'')
and denotations of predicates (``the set denoted by P''),
as well as expressions to refer to expressions in the modal temporal logic
that is used as its starting point (``the expression a'').
The semantics for a full reified logic becomes correspondingly complex,
as it needs to include normal individuals and points in time,
as well as entities corresponding to the linguistic entities 
that make up the underlying modal temporal logic.
Reichgelt's logic is therefore more of academic interest, rather than of any practical use.
However, the system shows that one can indeed use Shoham's proposal
to regard reified temporal logics as a formalization of the semantics of modal temporal logic
in a complicated, sorted but classical first-order logic.


\subsection{Advantages and Shortcomings of Temporal Reified method}

As illustrated by the example, 
the temporal reification method provides a fairly natural and
efficient notation and an expressive power clearly superior than
temporal arguments as it can talk and quantify over temporal relations
satisfactorily.
% ** notation ?

However temporal reified approaches have been criticized on two
different direction.
On the one hand,
because the {\bf ontologies} they commit one to.
In the example
$\occurs(1/4/04+3d,
  \receive(\bigCo,\offer(\smallco,\bigco,\sale(g,p),2w)))\land
\\
  \holds(1/4/04+3d,now,
  \effective(\offer(\smallco, \bigco,\sale(g,p), 2w))) 
$
we observe that, in both cases, the non-time arguments to
the temporal incidence predicate stand for a type of event or fluent, respectively. 
There are two objections against the introduction of event and state types.
The first is ontological.  Thus, taking his lead from \cite{Davidson67}, 
and following a long tradition in ontology, 
A. Galton \cite{Galton91} argues that a logic which forces one to reify event {\em tokens}
instead of event {\em types}, would be preferable on ontological grounds.  
Using Occam's
razor, Galton argues that one should not multiply the entities in one's
ontology without need, and that, unless one is a die-hard Platonist, one
would prefer an ontology based on particulars rather than universals.
A second argument against the introduction of types is that the resulting
logic may have expressiveness shortcomings.
Haugh \cite{Haugh87b} talks about the 
``individuation and counting of the events of a particular type''.
One cannot, for instance, refer
to the set of multiple effects originated by a single event causing them.
% *** add example
Also, one cannot quantify over causes and the related set of the
effects each produces in order to assert general constraints between them.

On the other hand, temporal reification has been criticized as an
unnecessary technical complication,
specially in the case that it is not defined as a standard many-sorted
logic
and we have to develop a new model theory and a proof theory 
that is complete for it.
Some researchers look at the {\em temporal token arguments} method a
the ideal alternative since it avoid both criticisms 
and seem to retain the expressiveness adavantages,
in particular in quatifying over predicates as shown in the \TTA\ section.



\section{Temporal Token Reification}\label{TemporalTokenReification}

This method is motivated by the attempt
of achieving the expressiveness advantages of temporal reification
(while staying in standard FOL)
and the ontological and technical advantages of temporal tokens
shown by the temporal token arguments approach
which avoids having to reify temporal types.

The primary intuition behind {\em Temporal Token Reification} (\TTR)
 is that one reifies temporal tokens
rather than temporal types.
However rather than making names for event tokens
an additional argument to a predicate 
(like in the temporal token arguments approach),
it proposes to introduce ``meaningful'' names for temporal tokens.
This allows one to talk and quantify about ``parts of a token''
as well as over all tokens 
and thus express express general temporal properties.


\subsection{Definition}
The logical language of \TTR is a many-sorted FOL with same sorts that
\TTA:
$T_1, \ldots , T_{n_t}$, one for each time set,
a number of non-time sorts $U_1, \ldots, U_n$
and one token sort $E_1,\ldots, E_{n_e}$ for each temporal entity.

\paragraph{Syntax.}

The vocabulary is is defined accordingly to the ideas above.
\begin{itemize}
\item 
{\em Function symbols:}
In addition to the time and atemporal function symbols of \TTA,
we have 
On the one hand, we have
a $m+n$-place function symbol for each $n$-place temporal relation,
with its first $m$ arguments being of a time sort
and its last $n$ arguments being of some non-time or token sort
and its output being either of type $E_i$.

On the other hand, 
we have the usual {\em time-token function} symbols, 
whose input argument is of sort $E_i$
and whose output argument is of sort $T_j$.
For instance,
$\bbegin$ denotes the starting point of a temporal token 
and their definition is straightforward.  Thus
\[
\bbegin(f(\ldots, t, t')) = t' 
\]
where $f(\ldots, t, t')$ is a term referring to a temporal token.

Finally, the language contains the 1-place function symbol $\TYPE$.
It takes as argument the name of a temporal token 
and returns a function from pairs of points in time into the set of
event or state tokens respectively. Hence,

\[ \TYPE(f(\ldots, t, t')) \]

is basically syntactic sugar for

\[ \lambda x \lambda y f(\ldots,x,y) \]

\item 
{\em Predicate symbols:}
As \TTA,
\TTR makes {\em TIPs} 1-place.
It contains one of them for each $E_i$
with its only argument being the name for an temporal entity.
For instance,
the predicates $\holds$ or $\occurs$ simply state that a
fluent token indeed holds, or that an event token indeed occurs.
\end{itemize}

\paragraph{Semantics.}
The semantics of the \TTR\ is relatively straightforward as well
and \TTR\ function and predicate symbols are mapped onto the
appropriate functions and relations respecting the signature of the
symbol.
Additionally, there are a few conditions that we need to
impose on our models in order to reflect intuitions about the nature of
time and the nature of the temporal entities.

\comentari{SEMANTICA NO STANDARD

There are a few conditions that we need to
impose on our models in order to reflect intuitions about the nature of
time and the nature of the temporal entities.

First, one of the differences between states and events is that if a
state is true over an interval $i$, it is also true over all
sub-intervals of $i$.  In the case of events, if an event is true over
an interval $i$, then it is false over all sub-intervals of $i$.  We
need to ensure that our model theory does indeed enforce this.  Thus, we
have the following conditions:

\begin{description}
\item
if \( {\cal I}(f(x,\ldots,x',t_{1},t_{2})) \in {\cal I}(HOLDS) \) \\
and \( {\cal I}(t_1) < {\cal I}(t_3) < {\cal I}(t_4) < {\cal I}(t_2) \) \\
\hspace*{-.75cm}then \( {\cal I}(f(x,\ldots,x',t_3,t_4)) \in {\cal I}(HOLDS) \)
\item
if \( {\cal I}(f(x,\ldots,x',t_{1},t_{2})) \in {\cal I}(OCCURS) \) \\
and \( {\cal I}(t_1) < {\cal I}(t_3) < {\cal I}(t_4) < {\cal I}(t_2) \) \\
\hspace*{-.75cm}then \( {\cal I}(f(x,\ldots,x',t_3,t_4)) \not\in {\cal I}(OCCURS) \)
\end{description}

Second, we need to ensure that the denotations of the special function
symbols \( \BEGIN, \END \) and \( \TYPE \) are indeed correct.  We
therefore need the following additional constraints:

\begin{description}
\item
\( {\cal I}(\BEGIN(f(x,\ldots,x',t,t'))) = {\cal I}(t) \)
\item
\( {\cal I}(\END(f(x,\ldots,x',t,t'))) = {\cal I}(t') \)
\item
\( {\cal I}(\TYPE(f(x,\ldots,x',s,s')))(< {\cal I}(t),{\cal I}(t')>) =
   {\cal I}(f(x,\ldots,x',t,t')) \)
\end{description}

Finally, a number of additional constraints may have to be imposed on
the temporal ordering relation to reflect one's intuitions about the
nature of time.  For example, one may want to guarantee the temporal
extension of tokens by the inclusion of

\begin{description}
\item
\( {\cal I}(\BEGIN(f(x,\ldots,x',t,t'))) < {\cal
I}(\END(f(x,\ldots,x',t,t'))) \)
\end{description}


The denotations of more complex expressions can now be defined in
the normal ways.  For example,

\begin{description}
\item
if $f$ is an $n$ place function symbol, \\
and \( f(x,\ldots,x') \) is a
well-formed term, \\
\hspace*{-.75cm} then
${\cal I}(f(x,\ldots,x')) = {\cal I}(f)({\cal I}(x),\ldots,{\cal I}(x'))$
\end{description}


The notions of truth and validity are also defined in the normal way.
For example,
\begin{description}
\item
Let $<M, {\cal I}>$ be a $TRL$-model, \\
$P$ an $n$-place predicate symbol, \\
and 
$<x\ldots,x'> $ $n$ terms of the appropriate sorts,\\
\hspace*{-.75cm}then \( <M, {\cal I}> \models P(x,\ldots,x') \)
iff \( <{\cal I}(x),\ldots,{\cal I}(x')> \in {\cal I}(P) \)
\end{description}
} % end comentari


\subsection{Formalizing the Example}\label{TTRformalizing}

The {\bf sorts} 
and the vocabulary is as in the temporal reification 
with the following additions:

\begin{itemize}
\item
$\funtime =
\{ 
\eend^{\langle \fluents, \instants, \instants \mapsto \instants \rangle},
\bbegin^{\langle \fluents, \instants, \instants \mapsto \instants \rangle}
\}$
where\\ $f(\ldots, t, t')$ is a term referring to a fluent-token.
\item 
$\funt = \funevents \cup \funfluents$
\begin{itemize}
\item
$\funevents =
\{
\send^{ \langle \instants, A, A, O \mapsto \events\rangle },
\receive^{ \langle \instants, A, O \mapsto \events\rangle },
\\\hspace*{2cm}
\accept^{ \langle \instants, A, O \mapsto \events\rangle },
\expire^{ \langle \instants, O \mapsto \events\rangle }
\}$
\item
$\funfluents =
\{
\effective^{\langle O, \instants, \instants \mapsto \fluents\rangle}
\}$
\end{itemize}
\item
$\predt = \emptyset$
\item
$\predat =
\{
\leq_{\$}^{\langle P, P\rangle}
\}$
(that denotes the $\leq$ relation between prices).
\item
and a set of variable symbols for each sort.
%${\bf V}_T = \{ x_t, y_t, \ldots \}$, 
%${\bf V}_A = \{ x_a, y_a, \ldots \}$, \ldots
\end{itemize}
\noindent The statements in the example can be formalized as follows:
\begin{enumerate}
\item
``On 1/4/04, SmallCo sent an offer for selling goods $g$ to BigCo for
price $p$ with a 2 weeks expiration interval.''
$\hspace*{0,5cm}
\occurs(
\send(1/4/04, \smallco, \bigCo, \offer(\smallco,\bigco,\sale(g,p),2w))
)
$
\item
``BigCo received the offer three days later and it has been effective
since then.''\\
$\hspace*{0,5cm}
\occurs(\receive(1/4/04+3d,\bigCo,\offer(\smallco,\bigco,\sale(g,p),2w)))\ \land
\\\hspace*{0,5cm}
\holds(\effective(1/4/04+3d,\now, \offer(\smallco,\bigco,\sale(g,p),2w)))
$
\item
``A properly formalized offer becomes effective when is received by
the offered...''\\
$
\forall\ t_1:\instants,x_a,y_a:A,x_o:O,ts:\tspans
\\\hspace*{0.5cm}
  [\ \correctform(\offer(x_a,y_a,x_o,ts)) \land
\\\hspace*{0.5cm}
  \occurs(\receive(t_1,y_a,\offer(x_a,y_a,x_o,ts))) \limplies 
\\\hspace*{0,5cm}
  \exists t_2\
  [\holds(\effective(t_1,t_2,\offer(x_a,y_a,x_o,ts)))\land t_1\leq t_2]
\ ]
$
\item
``\ldots (an effective offer) continues to be so until
it is accepted by the offered
or the offer expires (as indicated by its expiration interval).''\\
$
\forall\ t_1,t_2:\instants,x_a,y_a:A,x_o:O,ts:\tspans
\\\hspace*{0,5cm}
  [\ \holds(\effective(t_1, t_2, \offer(x_a,y_a,x_o,ts)))
  \land t_1\leq t_2 \limplies
\\\hspace*{0,5cm}\exists t_3:\instants [
  \accept(t_3,y_a,\offer(x_a,y_a,x_o,ts)) \land
  t_1 < t_3 \leq t_1+ts ]\ \lor
\\\hspace*{0,5cm}
  (t_2=t_1+ts \land \occurs(\expire(t2,\offer(x_a,y_a,x_o,ts))))
\ ]
$
\item 
``Anybody who makes an offer is committed to the offer as long as the offer is effective.''\\
$
\forall\ t_1,t_2:\instants, x_a:A
\\\hspace*{0.5cm}
[
  \holds(\effective(t_1,t_2, \offer(x_a,\_,\_,\_))) \limplies
\\\hspace*{0.5cm}
  \occurs(\committed(t_1,t_2, x_a, \offer(x_a,\_,\_,\_)))
]
$
\item
``Anybody who receives an offer is obliged to send a confirmation
to the offerer within two days.''\\
$
\forall\ t_1:\instants,x_a:A,x_o:O,
\\\hspace*{0,5cm}
[
  \occurs(\receive(t_1,y_a,\offer(x_a,y_a,x_o,\_)))
  \limplies
\\\hspace*{0,5cm}
  \holds(\obliged(t,t+2d,y_a,send(y_a,\conf(\offer(x_a,y_a,x_o,\_)))))
\\\hspace*{0,5cm}]
$
\end{enumerate}
Let's look at the additional statements:
\begin{itemize}
\item %1
Time axioms: ``The ordering between instants is transitive'':\\
$
\forall\ t_1,t_2,t_3:\instants\
[\ 
t_1 \leq t_2 \land t_2 \leq t_3 \limplies t_1 \leq t_3
\ ]
$
\item %2
Temporal Incidence axioms such as ``Fluents hold homogeneously'':\\
$\forall f:\fluents, t_1,t_2,t_3,t_4:\instants
\\\hspace*{0,5cm}
  [\ \holds(\TYPE(f)(<t_1,t_2>)) \land t_1 \leq t_3 \leq t_4 \leq
  t_2 \land t_1 \neq t_4 \limplies
\\\hspace*{0,5cm}
  \holds(\TYPE(f)(<t_3,t_4>))
\ ]
$
\item
``It is necessary for an offer to be properly written to be effective''.\\
$
\forall\ t_1,t_2:\instants, x_o:O\
\\\hspace*{0,5cm}
[ \holds(\effective(t_1,t_2,x_o)) \limplies \correctform(x_o) ]
$
\item
``Whenever an offer is effective it {\em causes} the agent who made the
offer to be committed to it for as long as the offer is effective.''\\
$
\forall\ t_1,t_2:\instants, x_a,y_a:A, x_o:O, ts:\tspans\\
\hspace*{0,5cm}
  [\cause( 
  \effective(t_1,t_2,\offer(x_a,y_a,x_o,ts)), 
  \committed(t_1,t_2,x_a,\offer(x_a,y_a,x_o,ts))
)]
$
\item
``Whenever a cause occurs its effects hold.''\\
$
\forall\ e:\events, f:\fluents
\\\hspace*{0,5cm}[\ \occurs(e) \land \cause(e,f) \limplies \holds(f)\ ]
$
\item
``Causes precede their effects.''\\
$
\forall\ e:\events, f:\fluents\\
\hspace*{0,5cm}
  [\ \cause(e,f) \limplies (\occurs(e) \limplies \holds(f) \land
  \ttime(e) \leq \bbegin(f))\ ]
$
\end{itemize}


% \subsection{Analysis}

% --------------------------------------------------------------------------
\section{Conclusion}\label{Conclusion}

In this chapter we have identified the relevant issues around the
temporal qualification method which is  central in the definition
of a temporal reasoning system in AI.
%
We have described the most relevant temporal qualification methods,
illustrated them with a rich example
and analysed advantages and shortcomings with respect to a number of
representational and reasoning efficiency criteria.
The various methods are schematically presented in figure
\ref{fig:tqscheme}.

\begin{figure}[ht]
\centerline{\psfig{figure=tq.eps,width=5.5in}}
\caption{Temporal qualification methods in AI.}
\label{fig:tqscheme}
\end{figure}

Temporal arguments is the classical, easy to define method
that turns out to be more expressive that what has traditionally been
recognized. 
It is enough for many applications except for those where one needs
to represent nested temporal references
or we needs to quantify over temporal propositions.
In fact,
the subsequent methods are a response to this limitation
in a more or less sophisticated manner.
{\em Temporal Token Arguments} allows a ``sort of'' quantification
while the language is a mere temporal arguments approach
by moving to a token-based ontology and introducing names for temporal
token in the language which provides a good deal of represenation
flexibility.
The other two approaches are based on reification which is a natural
way to talk and quantify over temporal propositions.
The increased expressiveness allows one to express statements like
``receiving an offer causes to be obliged to send a confirmation''
or
`` causes never preced their effects'' which is not possible in the
temporal argumentn method.

Technically the temporal reification methods are not that complex.
It can be complex if one preferes to define a non-standard
semantics for that, but it is not strictly necessary: 
some temporal reified logics can be defined as a many-sorted logic
with the appropriate time and temporal incidence axiomatizations.
In such case, it is important to be aware that these axioms can be a
source of high inefficiency for the theorem prover.
Things can get very complicated, though, 
if we aim at supporting the reification of non-atomic formula
as shown in \cite{Reichgelt86}.
It is not clear what is the practical interest of this
and it is not known what is the relationship between such logic
and temporal modal logics defined over a first order language.


\bibliography{temporal,cs,ai,logic}

\end{document}

\comentari{
\subsection{Improving the efficiency of theorem provers for the method of temporal arguments}\label{eff}

As said, theorem provers for theories formulated in the method of temporal arguments
are only complete if one includes a set of axioms describing the model of time
one wishes to adopt.
The problem is that many such axioms 
will in general significantly expand the search space for the theorem prover.  
For example, axioms, such as
``for every moment in time, there is a later moment in time'',
or ``for any two points in time, there is an intervening point in time'',
because of their recursive nature, may lead to a 
significant expansion of the search space 
if one uses a backward chaining theorem  prover 
and its use would therefore have to be carefully controlled.  
Clearly, the problem becomes more pronounced the more axioms one includes.  
It becomes extremely serious if one uses intervals as temporal units, 
and includes the various axioms necessary to specify 
the behavior of the temporal predicates that are necessary.
This situation is not dissimilar to the problem that arises in Schubert's
steamroller, a problem in the automated theorem proving literature that
led directly to the development of theorem provers for sorted logic.  
Schubert's steamroller includes a large
number of statements formalizing subclass relationships between classes. 
For example, it contains statements such as ``Foxes are carnivores'', and
``Caterpillars are insects''.  The main problem with these axioms is that
they lead to an explosive expansion of the search space. 

The solution that theorem provers for sorted logic provide is the
incorporation of the information in some of the axioms into the
unification mechanism of the theorem prover.  In the case of sorted logic,
one incorporates information about the sortal structure of the underlying
theory in the unification algorithm, hence eliminating them from the set
of axioms.  The result is that although individual unification steps are
considerably more expensive than for non-sorted logics, the total number
of unificati on steps is significantly reduced.  Empirical studies show
that the overall result is a significant speed-up in the overall theorem
proving process. 

This observation has led a number of researchers to explore the
possibility of developing theorem provers that allow one to incorporate
some of the axioms in the theory of time
into the unification algorithm of the theorem prover.  
Work in this direction can be found in \cite{Aitkenetal94} 
who in a sense generalize \cite{Frisch91}.
\cite{Aitkenetal94} describe a mechanism which allows one to automatically 
incorporate temporal information into the temporal argument
that is added in the method of temporal arguments.  For example,
using the temporal reification approach
the sentence ``SmallCo made an offer to BigCo sometime in the past''
would be represented as

\( \offer(\smallco, \bigco, t:\now) \)

The notion of a world-path is due to Ohlbach who uses it in a theorem
prover for modal logics.  Roughly, the idea is that the world-path indicates
in which world the proposition is assumed to be true.  In the above example,
\( t:\now \) refers to a moment 
in time sometime before the current point in time \(\now \).
Ohlbach then complicates the unification algorithm to take world-paths into
account.  The way in which the unification algorithm is complicated depends
on the modal axioms that are true in the modal logic under consideration.
Thus, in a modal logic in which the accessibility relationship is transitive,
the world-path arguments \( 0:w:w' \) and \( 0:w'' \) would unify with the
unification \( w'/w'' \).  After all, if $w'$ is accessible from $w$ and $w$
is accessible from $0$ and the accessibility relationship is transitive,
then $w'$ is (directly) accessible from $0$ as well.
Obviously, this idea can be relatively straightforwardly applied to the current situation,
where one could use world-path unification algorithms to unify temporal arguments.

In addition to introducing world-path arguments in their expressions, 
\cite{Aitkenetal94} also show how one can automatically construct a more
complicated unification algorithm from the temporal axioms.  Empirical
tests show the resulting system to be considerably faster than a naive
theorem prover for reified temporal logic.  However, the scope of the work
is clearly limited by the scope of the world-paths unification method for
theorem proving in modal logic, and work
on providing a theorem prover for temporal modal logic with intervals is still
very much a research issue.  Nevertheless, what \cite{Aitkenetal94}  show is 
that any progress made in that area can probably be used to provide more
powerful and efficient theorem provers for logic that rely on the method of temporal arguments
as well.
} % end comentari
