\documentstyle[jair,twoside,11pt,theapa]{article}

\jairheading{9}{1998}{463-506}{4/98}{12/98}
\ShortHeadings{A Temporal Description Logic for Reasoning
about Actions and Plans}
{Artale \& Franconi}
\firstpageno{463}

%%%%%%%%%%%%%%%%%% 78 colonne %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Set <key> to true, to show keywords.

\newif\ifkey
%% \keytrue
\keyfalse

%%%%%%%%%% macros %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand {\vspazio}  {\vspace{0.4 em}}
\newcommand {\smalltab} {\hspace*{5mm}}
\newcommand {\tab}      {\hspace*{10mm}}
\newcommand {\bigtab}   {\hspace*{15mm}}
\newcommand {\hugetab}  {\hspace*{20mm}}

\newcommand {\I}   {{\cal I}}
\newcommand {\dom} {\Delta} 
\newcommand {\Dom} {\Delta^{\I}}              
\newcommand {\Ind} {\mbox{${\cal O}$}}
\newcommand {\OT} {\mbox{${\cal OT}$}}

\newcommand {\per}  {\mbox{\bf .}} 
\newcommand {\set}  [1] {\{#1\}}
\newcommand {\card} [1] {|{#1}|}
\newcommand {\Fdom} [1] {\mbox{\sl dom}\ \!#1}

\newcommand {\Int}    [1] {#1^{\I}}
\newcommand {\Ints}    [1] {#1^{\I_S}}
\newcommand {\INT}    [1] {(#1)^{\I}}
\newcommand {\Nint}   [1] {#1^{\I}_t}
\newcommand {\NINT}   [1] {(#1)^{\I}_t}
\newcommand {\Intt}   [1] {#1^{\I}_{\V,t}}
\newcommand {\Inttw}  [1] {#1^{\I}_{\W,t}}
\newcommand {\INTT}   [1] {(#1)^{\I}_{\V,t}}
\newcommand {\Intx}   [2] {#1^{\I}_{\V,#2}}
\newcommand {\INTX}   [2] {(#1)^{\I}_{\V,#2}}
\newcommand {\Intth}  [1] {#1^{\I}_{\V,t,{\cal H}}}
\newcommand {\Intthw} [1] {#1^{\I}_{\W,t,{\cal H}}}
\newcommand {\INTTH}  [1] {(#1)^{\I}_{\V,t,{\cal H}}}
\newcommand {\INTTHS} [1] {(#1)^{\I,\S}_{\V,t,{\cal H}}}
\newcommand {\Intths} [1] {#1^{\I,\S}_{\V,t,{\cal H}}}
\newcommand {\Inthx}  [3] {#1^{\I}_{\V,#2,#3}}
\newcommand {\INThX}  [3] {(#1)^{\I}_{\V,#2,#3}}
\newcommand {\Eps}    [1] {#1^{\cal E}}
\newcommand {\EPS}    [1] {(#1)^{\cal E}}
\newcommand {\Inv}    [1] {\tilde #1}
\newcommand {\INV}    [1] {\tilde (#1)}

\newcommand{\Inds}{\mbox{${\cal J}$}}
\def\VMap{\mbox{${\cal M}$}}
\def\Estar{{\cal E}^*}
                                        
\def\AND{\sqcap}
\def\OR{\sqcup}
\def\NOT{\neg}
\def\ALL#1#2{\forall #1 \per #2}
\def\SOME#1#2{\exists #1 \per #2}
\def\SOMET#1{\exists #1}
\def\ALLRC{\ALL R C}
\def\SOMERC{\SOME R C}
\def\SOMERT{\SOMET R}
\def\SOMETIME{\Diamond}
\def\ST#1#2{\SOMETIME #1 \per\ #2}
\def\SST#1#2#3{\SOMETIME #1\ #2\per\ #3}
\def\ALLTIME{\Box}
\def\ALLT#1#2{\ALLTIME #1 \per\ #2}
\def\AT#1#2{\ALLTIME #1 \per #2}
\def\AGREE{\downarrow}
\def\DISAGREE{\uparrow}
\def\CHAIN{\circ}
\def\HOM{\mbox{$\nabla$}}
\newcommand{\Undef}[1]{#1\!\uparrow}
\def\CTN{\mbox{$\langle \overline{X},\overline{\TC},\overline{Q@X}\rangle $}}

\newcommand{\ATMOST}[3]{(\leq #1 \, #2 \, #3)}
\newcommand{\ATLEAST}[3]{(\geq #1 \, #2 \, #3)}
\newcommand{\BIGATMOST}[3]{\mbox{\Large (}\leq #1 \, #2 \, #3\mbox{\Large )}}
\newcommand{\BIGATLEAST}[3]{\mbox{\Large (}\geq #1 \, #2 \, #3\mbox{\Large )}}

\def\PERS{\mbox{$\Im\,$}} 

\def\NOW{\mbox{$\sharp$}}
\def\Parm{\mbox{$\star$}}

\def\TS{{\cal T}}
\def\IS{\mbox{$\TS^{\star}_{\mbox{\tiny $<$}}$}}
\def\T{{\cal T}} 
\def\V{{\cal V}} 
\def\H{{\cal H}} 
\def\W{{\cal W}} 
\def\P{{\cal P}} 
\def\S{{\cal S}} 
\def\M{\mbox{${\cal M}$}} 
\def\E{\mbox{${\cal E}$}} 
\def\INTVAR{\mbox{\it INT}}
\def\VAR{\mbox{\it VAR}}
\def\TC{{T\!\!c}}
\def\INTREL{\mbox{\it int\mbox{-}rel}}
\def\NC{E}
\def\ND{F}
\def\C-INV{\mbox{${\tilde C}$}} 

\def\SUBSUMEDBY{\sqsubseteq}
\def\NOTSUBSUMEDBY{\not\sqsubseteq}
\def\SUBSUMES{\sqsupseteq}
\def\NOTSUBSUMES{\not\sqsupseteq}
\def\SUBSUMED{\sqsubset}

\newcommand{\HS}      {\mbox{${\cal HS}$}}
\newcommand{\AL}      {\mbox{${\cal AL}$}}
\newcommand{\ALC}     {\mbox{${\cal ALC}$}}
\newcommand{\ALCF}    {\mbox{${\cal ALCF}$}}
\newcommand{\FLMIN}   {\mbox{${\cal FL}^{-{}}$}}

\newcommand{\TL}      {\mbox{${\cal T\!L}$}}
\newcommand{\TLU}      {\mbox{${\cal T\!LU}$}}
\newcommand{\TLF}     {\mbox{${\cal T\!L\mbox{-}F}$}}
\newcommand{\TLUFU}   {\mbox{${\cal T\!LU\mbox{-}FU}$}}
\newcommand{\TLALCF}  {\mbox{${\cal T\!L\mbox{-}ALCF}$}}
\newcommand{\F}       {\mbox{${\cal F}$}}
\newcommand{\FU}       {\mbox{${\cal FU}$}}

\newcommand{\Klone}   {\mbox{{\sc KL-One}}} 
\newcommand{\Back}    {\mbox{{\sc Back}}} 
\newcommand{\Loom}    {\mbox{{\sc Loom}}}
\newcommand{\Sbone}   {\mbox{{\sc SB-One}}} 
\newcommand{\Classic} {\mbox{{\sc Classic}}}
\newcommand{\Kris}    {\mbox{{\sc Kris}}}
\newcommand{\Yak}     {\mbox{{\sc Yak}}}
\newcommand{\Trex}    {\mbox{{\sc T-Rex}}}
\newcommand{\Clasp}   {\mbox{{\sc Clasp}}}
\newcommand{\Rat}     {\mbox{{\sc Rat}}}
\newcommand{\Strips}  {\mbox{{\sc Strips}}}

\newcommand{\Parbox}[1]{\parbox[t]{3in}{$ #1 $}}
\newcommand{\Parboxa}[1]{\parbox[t]{13cm}{$ #1 $}}
\newcommand{\Parboxb}[1]{\parbox[t]{7cm}{$ #1 $}}

\def\qed{\hfill{\mbox{$\Box$}}
  \ifdim\lastskip<\medskipamount \removelastskip\penalty55\medskip\fi}

%\newcounter {definition}[section]
%\def\thedefinition  {\thesection.\arabic{definition}}
%\newcommand{\definition}[2]
%{\vspace{1.3 ex}\refstepcounter{definition}\noindent{\sc Definition \thedefinition~(#1)} #2}

%%\newcounter{definition}
%%\newcommand{\definition}[2]
%% {\vspace{1.3 ex}\stepcounter{definition}\noindent{\bf Definition \thedefinition ~ (#1)}\\#2}

%%\newcommand{\Definition}[2]
%%{\vspace{1.3 ex}\stepcounter{definition}\noindent{\bf Definition \thedefinition ~ (#1)}#2}

\newtheorem{theorem}{Theorem}[section]
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{lemma}[theorem]{Lemma}

\newenvironment{proof}
  {\noindent{\em Proof.}}{\hfill $\Box$\vspace{1ex}}

\newenvironment{leftarray}
  {\vspace{1.3 ex}\renewcommand{\arraystretch}{1.3}\noindent$\begin{array}{l}}{\end{array}$\renewcommand{\arraystretch}{1}\vspace{1.3 ex}}

\newenvironment{leftarrayboxed}
  {\vspace{1.3 ex}\renewcommand{\arraystretch}{1.3}\noindent$\begin{array}{|r|}\hline}{\\\hline\end{array}$\renewcommand{\arraystretch}{1}\vspace{1.3 ex}}

\newenvironment{leftwoarray}
  {\vspace{1.3 ex}\renewcommand{\arraystretch}{1.3}\noindent$\begin{array}{ll}}{\end{array}$\renewcommand{\arraystretch}{1}\vspace{1.3 ex}}

\newenvironment{lefttriarray}
  {\vspace{1.3 ex}\renewcommand{\arraystretch}{1.3}$\begin{array}{lcl}}{\end{array}$\renewcommand{\arraystretch}{1}\vspace{1.3 ex}}

\newenvironment{lefteqnarray}
  {\vspace{1.3 ex}\renewcommand{\arraystretch}{1.3}\noindent$\begin{array}{rcl}}{\end{array}$\renewcommand{\arraystretch}{1}\vspace{1.3 ex}}

\newenvironment{lefteqnarrayfig}
  {\renewcommand{\arraystretch}{1.3}$\begin{array}{rcl}}{\end{array}$\renewcommand{\arraystretch}{1}}

\newenvironment{fiveeqnarrayfig}
  {\renewcommand{\arraystretch}{1.3}$\begin{array}{rclcl}}{\end{array}$\renewcommand{\arraystretch}{1}}

\newenvironment{lefteqnarrayboxed}
  {\vspace{1.3 ex}\renewcommand{\arraystretch}{1.3}\noindent$\begin{array}{|rcl|}\hline}{\\\hline\end{array}$\renewcommand{\arraystretch}{1}\vspace{1.3 ex}}

\newenvironment{Fourarray}
  {\vspace{1.3 ex}\renewcommand{\arraystretch}{1.3}\noindent$\begin{array}{@{\hspace{2em}}rlcl}}{\end{array}$\renewcommand{\arraystretch}{1}\vspace{1.3 ex}}

\newenvironment{leftfourarray}
  {\vspace{1.3 ex}\renewcommand{\arraystretch}{1.3}\noindent$\begin{array}{@{\hspace{2em}}lrcl}}{\end{array}$\renewcommand{\arraystretch}{1}\vspace{1.3 ex}}

\newenvironment{Eqnarraycomm}
  {\vspace{1.3 ex}\renewcommand{\arraystretch}{1.3}\noindent$\begin{array}{@{\hspace{1em}}rcl@{\tab}l}}{\end{array}$\renewcommand{\arraystretch}{1}\vspace{1.3 ex}}

\newenvironment{Eqnarraycommfig}
  {\renewcommand{\arraystretch}{1.3}$\begin{array}{@{\hspace{1em}}rcl@{\tab}l}}{\end{array}$\renewcommand{\arraystretch}{1}}

\newenvironment{Eqntabularcommfig}
  {\renewcommand{\arraystretch}{1.3}$\begin{array}{|l||@{\hspace{1em}}rcl@{\tab}l||}}{\end{array}$\renewcommand{\arraystretch}{1}}

\newenvironment{leftdescription}
  {\renewcommand{\arraystretch}{1.3}\begin{description}}{\end{description}\renewcommand{\arraystretch}{1}\vspace{1.3 ex}}

%%%%%%%%%%%%% title %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{document}

\title{
A Temporal Description Logic \\ for Reasoning
about Actions and Plans}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\author{\name Alessandro Artale \email artale@irst.itc.it \\
  \addr ITC-IRST, Cognitive and Communication Technologies Division\\ 
        I-38050 Povo TN, Italy \\ \\
  \name Enrico Franconi    \email franconi@cs.man.ac.uk \\
  \addr Department of Computer Science, University of Manchester\\
        Manchester M13 9PL, UK }

\maketitle


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{abstract} 
  
  A class of interval-based temporal languages for uniformly
  representing and reasoning about actions and plans is presented.
  Actions are represented by describing what is true while the action
  itself is occurring, and plans are constructed by temporally
  relating actions and world states.  The temporal languages are
  members of the family of Description Logics, which are characterized
  by high expressivity combined with good computational properties.
  The subsumption problem for a class of temporal Description Logics
  is investigated and sound and complete decision procedures are
  given. The basic language \TLF\ is considered first: it is the
  composition of a temporal logic \TL\ -- able to express interval
  temporal networks -- together with the non-temporal logic \F\ -- a
  Feature Description Logic. It is proven that subsumption in this
  language is an NP-complete problem. Then it is shown how to reason
  with the more expressive languages \TLUFU\ and \TLALCF. The former
  adds disjunction both at the temporal and non-temporal sides of the
  language, the latter extends the non-temporal side with set-valued
  features (i.e., roles) and a propositionally complete language.

\end{abstract} 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Introduction}

The representation of temporal knowledge has received considerable
attention in the Artificial Intelligence community in an attempt to
extend existing knowledge representation systems to deal with actions
and change.  At the same time, many logic-based formalisms were
developed and analyzed by logicians and philosophers for the same
purposes. In this class of logical formalisms, properties such as
expressive power and computability have been studied as regards
typical problems involving events and actions.

This paper analyzes from a theoretical point of view the logical and
computational properties of a knowledge representation system that
allows us to deal with time, actions and plans in a uniform way.  The
most common approaches to model actions are based on the notion of
{\em state change} -- e.g., the formal models based on the original
{\em situation
  calculus}~\cite{McCarthy:Hayes:69,sandewall:shoham:ai-94} or the
\Strips-like planning
systems~\cite{fikes:nilsson:71,lifschitz:strips:87} -- in which
actions are generally considered instantaneous and defined as
functions from one state to another by means of pre- and
post-conditions.  Here, an explicit notion of time is introduced in
the modeling language and actions are defined as {\em occurring over
  time intervals}, following the Allen proposal~\cite{allen:91}. In
this formalism an action is represented by describing the time course
of the world while the action occurs. Concurrent or overlapping
actions are allowed: effects of overlapping actions can be different
from the sum of their individual effects; effects may not directly
follow the action but more complex temporal relations may hold. For
instance, consider the motion of a pointer on a screen driven by a
mouse: the pointer moves because of the movement of the device on the
pad -- there is a cause-effect relation -- but the two events are
contemporary, in the common-sense notion of the word.

A class of interval temporal logics is studied based on Description
Logics and inspired by the works of Schmiedel~\citeyear{schmiedel:90} and
of Weida and Litman~\citeyear{weida:litman:kr-92}. In this class of
formalisms a {\em state} describes a collection of properties of the
world holding at a certain time.  {\em Actions} are represented
through temporal constraints on world states, which pertain to the
action itself.  {\em Plans} are built by temporally relating actions
and states.  To represent the temporal dimension classical Description
Logics are extended with temporal constructors; thus a uniform
representation for states, actions and plans is provided.
Furthermore, the distinction made by Description Logics between the
terminological and assertional aspects of the knowledge allows us to
describe actions and plans both at an abstract level (action/plan
types) and at an instance level (individual actions and plans). In
this environment, the {\em subsumption\/} calculus is the main
inference tool for managing collections of action and plan types.
Action and plan types can be organized in a subsumption-based
taxonomy, which plays the role of an action/plan library to be used
for the tasks known in the literature as plan retrieval and individual
plan recognition~\cite{kautz:91}.  A refinement of the {\em plan
  recognition\/} notion is proposed, by splitting it into the
different tasks of {\em plan description classification\/} --
involving a plan type -- and {\em specific plan recognition with
  respect to a plan description} -- involving an individual plan.
According to the latter reasoning task, the system is able to
recognize which type of action/plan has taken place at a certain time
interval, given a set of observations of the world.

Advantages of using Description Logics are their high expressivity
combined with desirable computational properties -- such as
decidability, soundness and completeness of deduction
procedures~\cite{buchheit:et:al:jair-93,aschaerf:dke-94,%
  donini:et:al:jlc-94,donini:et:al:tr-95}. The main purpose of this
work is to investigate a class of {\em decidable} temporal Description
Logics, and to provide complete algorithms for computing subsumption.
To this aim, we start with \TLF, a language being the composition of a
temporal logic \TL\ -- able to express interval temporal networks --
together with the non-temporal Description Logic \F\ -- a Feature
Description Logic~\cite{smolka:jlp-92}. It turns out that subsumption
for \TLF\ is an NP-complete problem.  Then, we show how to reason with
more expressive languages: \TLUFU, which adds disjunction both at the
temporal and non-temporal sides of the language, and \TLALCF, which
extends the non-temporal side with set-valued features (i.e., roles)
and a propositionally complete Description
Logic~\cite{hollunder:nutt:dfki-90}. In both cases we show that
reasoning is decidable and we supply sound and complete procedures for
computing subsumption.

%%%%%%%%%%%%%%%%%%%%%%%%%%% Structure %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\vspazio

The paper is organized as follows.  After introducing the main
features of Description Logics in Section~\ref{basic-dl},
Section~\ref{rel} organizes the intuitions underlying our proposal.
The technical bases are introduced by briefly overviewing the temporal
extensions of Description Logics relevant for this approach --
together with the inter-relationships with the interval temporal modal
logic -- specifically intended for time and action representation and
reasoning.  The basic feature temporal language (\TLF) is introduced
in Section~\ref{formal:language}. The language syntax is first
described in Section~\ref{sec-syntax}, together with a worked out
example illustrating the informal meaning of temporal expressions.
Section~\ref{sec-semantics} reveals the model theoretic semantics of
\TLF, together with a formal definition of the subsumption and
instance recognition problems.  Section~\ref{two-examples} shows that
the temporal language is suitable for action and plan representation
and reasoning: the well known {\em cooking} domain and {\em blocks
  world} domain are taken into consideration.  The sound and complete
calculus for the feature temporal language \TLF\ is presented in
details in Section~\ref{calculus}. A proof that subsumption for \TLF\ 
is an NP-complete problem is included.  The calculus for \TLF\ forms
the basic reasoning procedure that can be adapted to deal with logics
having an extended propositional part.  An algorithm for checking
subsumption in presence of disjunction (\TLUFU) is devised in
Section~\ref{disjunction-section}; while in
Section~\ref{Temporal:alcf} the non-temporal part of the language is
extended with roles and full propositional calculus (\TLALCF). In both
cases, the subsumption problem is still decidable.  Operators for
homogeneity and persistence are presented in
Section~\ref{full:language} for an adequate representation of world
states.  In particular, a possible solution to the {\em frame
  problem}, i.e., the problem to compute what remains unchanged by an
action, is suggested.  Section~\ref{related} surveys the whole
spectrum of extensions of Description Logics for representing and
reasoning with time and action.  This Section is concluded by a
comparison with {\em State Change} based approaches by briefly
illustrating the effort made in the situation calculus area to
temporally extend this class of formalisms.  Section~\ref{conclusion}
concludes the paper.


%%%%%%%%%%%%%%%%%%%%%%%%% DESCRIPTION LOGICS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Description Logics}
\label{basic-dl}

Description Logics\footnote{Description Logics have been also called
  {\em Frame-Based Description Languages}, {\em Term Subsumption
    Languages}, {\em Terminological Logics}, {\em Taxonomic Logics},
  {\em Concept Languages} or {\em \Klone-like languages}.} are
formalisms designed for a logical reconstruction of representation
tools such as {\em frames}, {\em semantic networks}, {\em
  object-oriented} and {\em semantic} data models --
see~\cite{calvanese:et:al:kr-94} for a survey.  Nowadays, Description
Logics are also considered the most important unifying formalism for
the many object-centered representation languages used in areas other
than Knowledge Representation. Important characteristics of
Description Logics are high expressivity together with decidability,
which guarantee the existence of reasoning algorithms that always
terminate with the correct answers.

This Section gives a brief introduction to a basic Description Logic,
which will serve as the basic representation language for our
proposal. As for the formal apparatus, the formalism introduced
by~\cite{schmidt-schauss:smolka:ai-91} and further elaborated
by~\cite{donini:et:al:ai-92,donini:et:al:jlc-94,%
donini:et:al:tr-95,buchheit:et:al:jair-93,degiacomo:lenzerini:ijcai-95,%
degiacomo:lenzerini:kr-96} is followed: in this way, Description
Logics are considered as a {\em structured} fragment of predicate
logic.  \ALC~\cite{schmidt-schauss:smolka:ai-91} is the minimal
Description Logic including full negation and disjunction -- i.e.,
propositional calculus, and it is a notational variant of the
propositional modal logic {\boldmath
  $K_{(m)}$}~\cite{halpern:moses:ijcai-85,schild:ijcai-91}.

\begin{figure}
{\small
  \begin{center}
    \leavevmode
    $\begin{array}{rcll}
      C,D & \rightarrow\ 
        & A \mid & \mbox{(atomic concept)} \\
      & & \top \mid  & \mbox{(top)} \\
      & & \bot \mid  & \mbox{(bottom)} \\
      & & \NOT C  \mid  & \mbox{(complement)} \\
      & & C\AND D \mid  & \mbox{(conjunction)} \\
      & & C\OR D \mid  & \mbox{(disjunction)} \\
      & & \ALL {P}{C} \mid  & \mbox{(universal quantifier)} \\
      & & \SOME {P}{C} \mid  & \mbox{(existential quantifier)} \\
      & & p:C \mid & \mbox{(selection)} \\
      & & p\AGREE q \mid    & \mbox{(agreement)}\\
      & & p\DISAGREE q \mid    & \mbox{(disagreement)}\\
      & & \Undef p  & \mbox{(undefinedness)} \\
      p,q & \rightarrow\ 
        & f \mid & \mbox{(atomic feature)} \\
      & & p \CHAIN q  & \mbox{(path)}
    \end{array}
    $
 \end{center}}
\caption[dl-syntax]{\label{dl-syntax} Syntax rules for the \ALCF\ 
Description Logic.}
\end{figure}

The basic types of a Description Logic are {\em concepts}, {\em
  roles}, {\em features}, and {\em individuals}.  A concept is a
description gathering the common properties among a collection of
individuals; from a logical point of view it is a unary predicate
ranging over the domain of individuals.  Properties are represented
either by means of roles -- which are interpreted as binary relations
associating to individuals of a given class values for that property
-- or by means of features -- which are interpreted as functions
associating to individuals of a given class a {\em single} value for
that property.  The language \ALCF, extending \ALC\ with features
(i.e., functional roles) is considered.  By the syntax rules of
Figure~\ref{dl-syntax}, \ALCF\ {\em concepts\/} (denoted by the
letters $C$ and $D$) are built out of {\em atomic concepts\/} (denoted
by the letter $A$), {\em atomic roles\/} (denoted by the letter $P$),
and {\em atomic features\/} (denoted by the letter $f$). The syntax
rules are expressed following the tradition of Description
Logics~\cite{baader:et:al:proposal-90}.
%%The simpler {\em feature} description logic \F\ is also introduced, as
%%the sub-language of \ALCF\ without negation, disjunction, and roles:
%%
%%$C, D \rightarrow A \mid \top \mid C\AND D \mid p\AGREE q \mid p:C$
%%
%%$p, q \rightarrow f \mid  p \CHAIN q$

The {\em meaning} of concept expressions is defined as sets of
individuals, as for unary predicates, and the meaning of roles as sets
of pairs of individuals, as for binary predicates.  Formally, an {\em
  interpretation\/} is a pair $\I = (\Int\Delta, \Int\cdot)$
consisting of a set $\Int\Delta$ of individuals (the {\em domain\/} of
$\I$) and a function $\Int{\cdot}$ (the {\em interpretation
  function\/} of $\I$) mapping every concept to a subset of
$\Int\Delta$, every role to a subset of $\Int\Delta\times\Int\Delta$,
every feature to a partial function from $\Int\Delta$ to $\Int\Delta$,
and every individual into a different element of $\Int\Delta$ -- i.e.,
$\Int{a}\neq\Int b$ if $a \neq b$ (Unique Name Assumption) -- such
that the equations of the left column in Figure~\ref{dl-semantics} are
satisfied.

The \ALCF\ semantics identifies concept expressions as fragments of
first-order predicate logic. Since the interpretation $\I$ assigns to
every atomic concept, role or feature a unary or binary (functional)
relation over $\Int\Delta$, respectively, one can think of atomic
concepts, roles and features as unary and binary (functional)
predicates.  This can be seen as follows: an atomic concept $A$, an
atomic role $P$, and an atomic feature $f$, are mapped respectively to
the open formulas $F_A(\gamma)$, $P(\alpha,\beta)$, and
$F_f(\alpha,\beta)$ with $F_f$ satisfying the functionality axiom
$\forall y,z\per F_f(x,y)\wedge F_f(x,z) \rightarrow y = z$ -- i.e.,
$F_f$ is a functional relation.

The rightmost column of Figure~\ref{dl-semantics} gives the
transformational semantics of \ALCF\ expressions in terms of FOL
well-formed formul\ae, while the left column gives the standard
extensional semantics.  As far as the transformational semantics is
concerned, a concept $C$, a role $P$ and a path $p$ correspond to the
FOL open formulae $F_C(\gamma)$, $F_P(\alpha,\beta)$, and
$F_p(\alpha,\beta)$, respectively.  It is worth noting that the
extensional semantics of the left column gives also an interpretation
for the formulas of the right column so that the following proposition
holds.
\begin{proposition}[Concepts vs. fol formul\ae]\label{fol}
  Let $C$ be an \ALCF\ concept expression. Then the transformational
  semantics of Figure~\ref{dl-semantics} maps $C$ into a logically
  equivalent first order formula.
\end{proposition}
A {\em terminology\/} or {\em TBox\/} is a finite set of {\em
  terminological axioms}.  For an atomic concept $A$, called {\em
  defined concept}, and a (possibly complex) concept $C$, a
terminological axiom is of the form $A\doteq C$.  An atomic concept
not appearing on the left-hand side of any terminological axiom is
called a {\em primitive concept}. {\it Acyclic simple} TBoxes only are
considered: a defined concept may appear at most once as the left-hand
side of an axiom, and no terminological cycles are allowed, i.e., no
defined concept may occur -- neither directly nor indirectly -- within
its own definition~\cite{nebel:cycles-91}.  An interpretation $\I$
{\em satisfies} $A\doteq C$ if and only if $\Int A = \Int C$.

%%%%%%%%%%%%%%%%%%%%%
\begin{figure}[t]
{\small
\begin{center}
\leavevmode
\renewcommand{\arraystretch}{1.2}
$\begin{array}{rl@{\hspace{1.5em}}l}

  \Int\top = & \Int\Delta & {\sf true} \\ 

  \Int\bot = & \emptyset & {\sf false}\\ 

  \Int{(\NOT C)} = & \Int\Delta \setminus \Int C & \neg F_C(\gamma)\\

  \Int{(C\AND D)} = & \Int C \cap \Int D & F_C(\gamma) \wedge F_D(\gamma)\\ 

  \Int{(C\OR D)} = & \Int C \cup \Int D & F_C(\gamma) \vee F_D(\gamma)\\ 

  \Int{(\SOME{P}{C})} = & \set{a\in\Int\Delta \mid \exists b\per (a,b)\in\Int
    P\wedge b\in\Int C} & \exists x\per F_P(\gamma,x)\wedge F_C(x)\\ 

  \Int{(\ALL{P}{C})} = & \set{a\in\Int\Delta \mid \forall b\per (a,b)\in\Int P
    \Rightarrow b\in\Int C} & \forall x\per F_P(\gamma,x) \Rightarrow
  F_C(x)\\ 

  \Int{(p:C)} = & \set{ a\in\Fdom{\Int p} \mid \Int p(a)\in\Int C} &
  \exists x\per F_p(\gamma,x) \wedge F_C(x)\\ 

  \Int{p\AGREE q} = & \set{ a\in \Fdom{\Int p}\cap\Fdom{\Int q}\mid
    \Int p (a) = \Int q (a) } & \mbox{{\large (}}\exists x\per F_p(\gamma,x) 
                                 \wedge F_q(\gamma,x)\mbox{{\large )}} \\

  \Int{p\DISAGREE q} = & \set{ a\in \Fdom{\Int p}\cap\Fdom{\Int q}\mid
    \Int p (a) \neq \Int q (a) } & \mbox{{\large (}}\exists x,y\per 
                 F_p(\gamma,x) \wedge F_q(\gamma,y)\mbox{{\large )}} \wedge \\
                            &  & \mbox{{\large (}}\forall x,y\per 
                                 F_p(\gamma,x) \wedge F_q(\gamma,y) \rightarrow
                                 x \neq y\mbox{{\large )}} \\


  \Int{(\Undef p)} = & \Int\Delta\setminus\Fdom{\Int p} & \neg \exists x\per
  F_p(\gamma,x)\\

  \Int{(p\CHAIN q)} = & \Int p{\scriptstyle\circ}\ \Int q & \exists x\per
  F_p(\alpha,x) \wedge F_q(x,\beta)

\end{array}$
\renewcommand{\arraystretch}{1}
\end{center}}
\ \hrulefill
\caption[dl-semantics]{\label{dl-semantics} 
  The extensional and transformational semantics in \ALCF.}
\end{figure}
%%%%%%%%%%%%%%%%%%%%%

As an example, consider the unary relation (i.e., a concept)
denoting the class of happy fathers, defined using the atomic
predicates {\tt Man, Doctor, Rich, Famous} (concepts) and {\tt CHILD,
  FRIEND} (roles):

\vspazio\noindent${\tt Happy Father}\doteq {\tt Man \AND
  (\SOME{CHILD}{\top}) \AND \ALL{CHILD}{(Doctor \AND
    \SOME{FRIEND}{(Rich \OR Famous)})}}$ \vspazio

\noindent i.e., the men whose children are doctors having some rich or 
famous friend.

An {\em ABox} is a finite set of {\em assertional axioms}, i.e.\ 
predications on individual objects.  Let \Ind\ be the alphabet of
symbols denoting {\it individuals}; an assertion is an axiom of the
form $C(a)$, $R(a,b)$ or $p(a,b)$, where $a$ and $b$ denote
individuals in \Ind.  $C(a)$ is satisfied by an interpretation $\I$
iff $\Int a \in \Int{C}$, $P(a,b)$ is satisfied by $\I$ iff $(\Int
a,\Int b)\in \Int{P}$, and $p(a,b)$ is satisfied by $\I$ iff
$\Int{p}(\Int a)=\Int b$.

A {\em knowledge base} is a finite set $\Sigma$ of terminological and
assertional axioms.  An interpretation $\I$ is a {\em model} of a
knowledge base $\Sigma$ iff every axiom of $\Sigma$ is satisfied by
$\I$.  $\Sigma$ {\em logically implies} $A\SUBSUMEDBY C$ (written
$\Sigma\models A\SUBSUMEDBY C$) if $\Int A \subseteq \Int C$ for every
model of $\Sigma$: we say that $A$ is {\em subsumed\/} by $C$ in
$\Sigma$. The reasoning problem of checking whether $A$ is {\em
  subsumed\/} by $C$ in $\Sigma$ is called {\em subsumption checking}.
$\Sigma$ {\em logically implies} $C(a)$ (written $\Sigma\models C(a)$)
if $\Int a \in \Int{C}$ for every model of $\Sigma$: we say that $a$
is an {\em instance\/} of $C$ in $\Sigma$. The reasoning problem of
checking whether $a$ is an {\em instance\/} of $C$ in $\Sigma$ is
called {\em instance recognition}.

An acyclic simple TBox can be transformed into an {\em expanded} TBox
having the same models, where no defined concept makes use in its
definition of any other defined concept. In this way, the
interpretation of a defined concept in an expanded TBox does not
depend on any other defined concept. It is easy to see that $A$ is
subsumed by $C$ in an acyclic simple TBox $\Sigma$ if and only if the
expansion of $A$ with respect to $\Sigma$ is subsumed by the expansion
of $C$ with respect to $\Sigma$ in the empty TBox.  The expansion
procedure recursively substitutes every defined concept occurring in a
definition with its defining expression; such a procedure may generate
a TBox exponential in size, but it has been proved~\cite{nebel:ai-90}
that it works in polynomial time under reasonable restrictions. The
following interchangeably refers either to reasoning with respect to a
TBox or to reasoning involving expanded concepts with an empty TBox.
In particular, while devising the subsumption calculus for the logics
considered here, it is always assumed that all defined concepts have
been expanded.

%%%%%%%%%%%%%%%%%%%%%%%%% Basic Related Works %%%%%%%%%%%%%%%%%%%%%%%%

\section{Towards a Temporal Description Logics}
\label{rel}

%%%%%%%%%%%%%%%%%%%%%% Schmiedel %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Schmiedel~\citeyear{schmiedel:90} proposed to extend Description
Logics with an interval--based temporal logic. The temporal variant of
the Description Logic is equipped with a model-theoretic semantics.
The underlying Description Logic is ${\cal
  FLENR}^-$~\cite{donini:et:al:tr-95}: it differs from \ALCF\ in that
it does not contain the $\top$ and $\bot$ concepts, it does not have
neither negation nor disjunction, and it has cardinality restrictions
and conjunction over roles. The new temporal term-forming operators
are the temporal qualifier {\sf at}, the existential and universal
temporal quantifiers {\sf sometime} and {\sf alltime}.  The qualifier
operator specifies the time at which a concept holds. The temporal
quantifiers introduce the temporal variables constrained by means of
temporal relationships based on Allen's interval algebra extended with
metric constraints to deal with durations, absolute times, and
granularities of intervals. To give an example of this temporal
Description Logic, the concept of ${\tt Mortal}$ can be defined by:

\vspazio\noindent
${\tt Mortal ~ \doteq ~ LivingBeing} ~ \AND ~
     \mbox{\large(} {\sf sometime}({\tt x}) ~ ({\sf after} ~ {\tt x} ~ 
     {\sf NOW}) ~~
     ({\sf at} ~ {\tt x} ~ (\NOT {\tt LivingBeing}))
     \mbox{\large)}
$
\vspazio

\noindent 
with the meaning of a {\tt LivingBeing} at the reference interval {\sf
  NOW}, who will not be alive at an interval {\tt x} sometime after
the reference interval {\sf NOW}.  Schmiedel does not propose any
algorithm for computing subsumption, but gives some preliminary hints.
Actually, Schmiedel's logic is argued to be
undecidable~\cite{bettini:dke-97}, sacrificing the main benefit of
Description Logics: the possibility of having decidable inference
techniques.

Schmiedel's temporal Description Logic, when closed under
complementation, contains as a proper fragment the temporal logic \HS\ 
proposed by Halpern and Shoham~\citeyear{halpern:shoham:91}.  The
logic \HS\ is a propositional modal logic which extends propositional
logic with modal formul\ae\ of the kind $\langle R \rangle\per\phi$
and $[ R ]\per\phi$ -- where $R$ is a basic Allen's temporal relation
and $\langle \rangle$ and $[ ]$ are the possibility and necessity
modal operators.  For example, the modal formula ${\tt
  LivingBeing}\wedge \langle{\sf after}\rangle\per \neg{\tt
  LivingBeing}$ corresponds to the abovementioned {\tt Mortal}
concept. Unfortunately, the \HS\ logic is shown to be undecidable, at
least for most interesting classes of temporal structures: ``{\em One
  gets decidability only in very restricted cases, such as when the
  set of temporal models considered is a finite collection of
  structures, each consisting of a finite set of natural
  numbers.}''~\cite{halpern:shoham:91}

%%%%%%%%%%%%%%%%%%%%%%% Weida and Litman %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Weida and Litman~\citeyear{weida:litman:kr-92,weida:litman:caia-94}
propose \Trex, a loose hybrid integration between Description Logics
and constraint networks. Plans are defined as collections of steps
together with temporal constraints between their duration.  Each step
is associated with an action type, represented by a generic concept in
{\sc K-Rep} -- a non-temporal Description Logic. Thus a plan is seen
as a {\em plan network}, a temporal constraint network whose nodes,
corresponding to time intervals, are labeled with action types and are
associated with the steps of the plan itself.  As an example of plan
in \Trex\ they show the plan of preparing spaghetti marinara:

\vspazio
\noindent$
\mbox{\large(} \mbox{\sf defplan\ }
     {\tt Assemble\mbox{-}Spaghetti\mbox{-}Marinara}\\  
      \tab(\parbox[t]{20em}{$
       (step1~~ {\tt Boil\mbox{-}Spaghetti})\\
       (step2~~ {\tt Make\mbox{-}Marinara})\\
       (step3~~ {\tt Put\mbox{-}Together\mbox{-}SM}))$}\\
      \tab(\parbox[t]{20em}{$
       (step1~~ ({\sf before~~ meets})~~ step3)\\
       (step2~~ ({\sf before~~ meets})~~ step3)) \mbox{\large)}
       $}
$
\vspazio

\noindent 
This is a plan composed by three actions, i.e., boiling spaghetti,
preparing marinara sauce, and assembling all things at the end.
Temporal constraints between the steps establish the temporal order in
doing the corresponding actions.  A structural plan subsumption
algorithm is defined, characterized in terms of graph matching, and
based on two separate notions of subsumption: pure terminological
subsumption between action types labeling the nodes, and pure temporal
subsumption between interval relationships labeling the arcs.  The
plan library is used to guide plan recognition~\cite{weida:phd-96} in
a way similar to that proposed by Kautz~\citeyear{kautz:91}.  Even if
this work has strong motivations, no formal semantics is provided for
the language and the reasoning problems.

%%%%%%%%%%%%%%%%%%%%%%%%% Our Proposal %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%\vspazio

Starting from the assumption that an action has a duration in time,
our proposal considers an interval-based modal temporal logic -- in
the spirit of Halpern and Shoham~\citeyear{halpern:shoham:91} -- and
reduces the expressivity of~\cite{schmiedel:90} in the direction
of~\cite{weida:litman:kr-92}.  While Schmiedel's work lacks
computational machinery, and Halpern and Shoham's logic is
undecidable, here an expressive decidable logic is obtained, providing
sound and complete reasoning algorithms.  Differently from \Trex\ 
which uses two different languages to represent actions and plans -- a
non temporal Description Logic for describing actions and a second
language to compose plans by adding temporal information -- here an
extension of a Description Logic is chosen in which time operators are
available directly as term constructors.  This view implies an
integration of a temporal domain in the semantic structure where terms
themselves are interpreted, giving the formal way both for a
well-founded notion of subsumption and for proving soundness and
completeness of the corresponding procedure.  As an example of the
formalism, the plan for preparing spaghetti marinara introduced above
is represented as follows:

\vspazio
\noindent
$
{\tt Assemble\mbox{-}Spaghetti\mbox{-}Marinara} \doteq \SOMETIME 
      (y\ z\ w)\ 
      \parbox[t]{18em}{$
        (y\ ({\sf before, meets})\ w)(z\ ({\sf before, meets})\ w) \per\ \\
        (\parbox[t]{16em}{$
         {\tt Boil\mbox{-}Spaghetti}@y\ \AND \\
         {\tt Make\mbox{-}Marinara}@z\ \AND\ \\
         {\tt Put\mbox{-}Together\mbox{-}SM}@w
       )
       $}$}
$
\vspazio

\noindent
Moreover, it is possible to build {\em temporal structured} actions --
as opposed to the atomic actions proposed in \Trex\ -- describing how
the world state changes because of the occurrence of an action: in
fact, our language allows for feature representation in order to
relate actions to states of the world (see Section~\ref{block}).  This
kind of expressivity is not captured by \Trex, since it uses a
non-temporal Description Logic to represent actions.  The main
application of \Trex\ is plan recognition; according to the ideas of
Kautz~\citeyear{kautz:91} a Closed World Assumption
(CWA)~\cite{weida:phd-96} is made, assuming that the plan library is
complete and an observed plan will be fully accounted for by a single
plan. CWA is not relied on here, following the Open World Semantics
characterizing Description Logics.  Weaker, but monotonic, deductions
are allowed in the plan recognition process.  However, their
procedures for recognizing a {\em necessary}, {\em optional} or {\em
  impossible} individual plan with respect to a plan description is
still applicable, if the plan library is given a closed world
semantics.

%%%%%%%%%%%%%%%%%%%%%%%%%% THE LANGUAGE %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{The Feature Temporal Language \TLF}
\label{formal:language}

The feature temporal language \TLF\ is the basic logic considered
here. This language is composed of the temporal Logic \TL\ -- able to
express interval temporal networks -- and the non-temporal Feature
Description Logic \F.  Note that, each logic of the family of Temporal
Description Logics introduced in this paper is identified by a
composed string in which the first part refers to the temporal part of
the language while the other one refers to the non-temporal part.

%%%%%%%%%%%%%%%%%%%%%%%%%% THE SYNTAX %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{Syntax}
\label{sec-syntax}

Basic types of the language are {\em concepts\/}, {\em individuals},
{\em temporal variables} and {\em intervals}. Concepts can describe
entities of the world, states and events. Temporal variables denote
intervals bound by temporal constraints, by means of which abstract
temporal patterns in the form of constraint networks are expressed.
Concepts (resp.  individuals) can be specified to hold at a certain
temporal variable (resp.  interval).  In this way, {\em action types}
(resp.  {\em individual actions}) can be represented in a uniform way
by temporally related concepts (resp.  individuals).

\begin{figure}[t]
  \begin{center}
    \setlength{\unitlength}{0.175in}
    \begin{picture}(23,12)
      \linethickness{2pt}
      \put(13, 0){\line( 1, 0){5}}
      \put(14, 2){\line( 1, 0){5}}
      \put(15, 4){\line( 1, 0){5}}
      \put(17, 6){\line( 1, 0){4}}
      \put(18, 8){\line( 1, 0){4}}
      \put(19,10){\line( 1, 0){4}}
      \put(15,11){\line( 1, 0){3}}
      \thinlines
      \put(15, 0){\line( 0, 1){11}}
      \put(18, 0){\line( 0, 1){11}}
      \put(0,12){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt] Relation}}
      \put(6,12){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt] Abbr.}}
      \put(10,12){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt] Inverse}}
      \put(16,12){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt] {\it i}}}
      \put(20,12){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt] {\it j}}}
      {\small
      \put(0,10){\makebox(0,0)[lb]{\sf\raisebox{0pt}[0pt][0pt] before$(i,j)$}}
      \put(6,10){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt] {\sf b}}}
      \put(10,10){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt] {\sf a}}}
      \put(0,8){\makebox(0,0)[lb]{\sf\raisebox{0pt}[0pt][0pt] meets$(i,j)$}}
      \put(6,8){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt] {\sf m}}}
      \put(10,8){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt] {\sf mi}}}
      \put(0,6){\makebox(0,0)[lb]{\sf\raisebox{0pt}[0pt][0pt] overlaps$(i,j)$}}
      \put(6,6){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt] {\sf o}}}
      \put(10,6){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt] {\sf oi}}}
      \put(0,4){\makebox(0,0)[lb]{\sf\raisebox{0pt}[0pt][0pt] starts$(i,j)$}}
      \put(6,4){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt] {\sf s}}}
      \put(10,4){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt] {\sf si}}}
      \put(0,2){\makebox(0,0)[lb]{\sf\raisebox{0pt}[0pt][0pt] during$(i,j)$}}
      \put(6,2){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt] {\sf d}}}
      \put(10,2){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt] {\sf di}}}
      \put(0,0){\makebox(0,0)[lb]{\sf\raisebox{0pt}[0pt][0pt] finishes$(i,j)$}}
      \put(6,0){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt] {\sf f}}}
      \put(10,0){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt] {\sf fi}}}
        }
    \end{picture}
  \end{center}
  \caption[allen-intervals]{\label{allen-intervals}
  The Allen's interval relationships.}
\end{figure}

For the basic temporal interval relations the Allen
notation~\cite{allen:91}\ (Figure~\ref{allen-intervals}) is used:
before ({\sf b}), meets ({\sf m}), during ({\sf d}), overlaps ({\sf
  o}), starts ({\sf s}), finishes ({\sf f}), equal ({\sf =}), after
({\sf a}), met-by ({\sf mi}), contains ({\sf di}), overlapped-by ({\sf
  oi}), started-by ({\sf si}), finished-by ({\sf fi}). {\em Concept
  expressions\/} (denoted by $C,D$) are syntactically built out of
{\em atomic concepts\/} (denoted by $A$), {\em atomic features\/}
(denoted by $f$), {\em atomic parametric features} (denoted by $\Parm
g$) and {\em temporal variables} (denoted by $X,Y$). Temporal concepts
($C,D$) are distinguished from non-temporal concepts ($E,F$),
following the syntax rules of Figure~\ref{syntax}. Names for atomic
features and atomic parametric features are from the same alphabet of
symbols; the \Parm\ symbol is not intended as operator, but only as
differentiating the two syntactic types.

\begin{figure}[t]
{\normalsize
\begin{center}
\begin{Eqntabularcommfig} \hline
\TL  & C,D & \rightarrow\ & \NC \mid            & \mbox{(non-temporal concept)} \\ 
     &     &              & C\AND D \mid        & \mbox{(conjunction)} \\
     &     &              & C @ X \mid          & \mbox{(qualifier)}\\
     &     &              & C [ Y ] @ X \mid    & \mbox{(substitutive qualifier)}\\
     &     &              & \SOMETIME {(\overline{X})}\ {\overline{\TC}}
                               \mbox{\large{\bf .}}{C}
                                         & \mbox{(existential quantifier)}\\
     &{\TC}& \rightarrow\ & ( X\ (R)\ Y ) \mid & \mbox{(temporal constraint)}\\
     &     &              & ( X\ (R)\ \NOW ) \mid & \\
     &     &              & ( \NOW\ (R)\ Y )    & \\
     & \overline{\TC}     & \rightarrow\ &  \TC \mid \TC\ \overline{\TC} &\\
     & R,S & \rightarrow\ & R\mbox{\large \bf \ ,\ }S \mid    
                                         & \mbox{(disjunction)}\\
     &     &              & {\sf s} \mid {\sf mi} \mid {\sf f} \mid \ldots 
                                         & \mbox{(Allen's relations)}\\
     & X,Y & \rightarrow\ & {\rm x} \mid  
                     {\rm y} \mid 
                     {\rm z} \mid \ldots        & \mbox{(temporal variables)}\\ 
     & \overline{X}       & \rightarrow\ &  X \mid X\ \overline{X} & \\
\hline \hline
\F  &\NC,\ND & \rightarrow\ & A \mid            & \mbox{(atomic concept)} \\
    &        &              & \top \mid         & \mbox{(top)} \\    
    &        &              & \NC\AND \ND \mid  & \mbox{(conjunction)} \\
    &        &              & p\AGREE q \mid    & \mbox{(agreement)}\\
    &        &              & p:\NC             & \mbox{(selection)}\\
    &   p,q  & \rightarrow\ & f \mid            & \mbox{(atomic feature)}\\
    &        &              & \star g \mid      & \mbox{(atomic parametric feature)}\\
    &        &              & p\CHAIN q         & \mbox{(path)}\\ \hline
\end{Eqntabularcommfig} 
\end{center}
}
\caption[syntax]{\label{syntax}
Syntax rules for the interval Description Logic \TLF}
\end{figure}

Temporal variables are introduced by the temporal existential
quantifier ``$\SOMETIME$'' -- excluding the special temporal variable
\NOW, usually called {\sf NOW}, and intended as the reference interval.
Variables appearing in temporal constraints ($\overline\TC$) must be
declared within the same temporal quantifier, with the exception of
the special variable \NOW.  Temporal variables appearing in the right
hand side of an ``$@$'' operator are called {\em bindable}. Concepts
must not include {\em unbound} (a.k.a.  {\em free}) bindable
variables. Informally, a bindable variable is said to
be {\em bound} in a concept if it is declared at the nearest temporal
quantifier in the body of which it occurs; this avoid the usual
formal inductive definition of a bound variable.  Moreover, in chained
constructs of the form $((C[Y_1]@X_1)[Y_2]@X_2\ldots)$ non bindable
variables -- i.e., the ones on the left hand side of an ``$@$''
operator -- cannot appear more than once. Note that, since Description
Logics are a fragment of FOL with one free variable, the above mentioned
restrictions force the temporal side of the language to have only one
free temporal variable, i.e., the reference time \NOW. 

As usual, terminological axioms for building simple acyclic \TLF\ 
TBoxes are allowed.  While using in a concept expression a name
referring to a defined concept, it is possible to use the substitutive
qualifier construct, to impose a coreference with a variable appearing
in the definition associated to the defined concept. The statement
$C[Y]@X$ constrains the variable $Y$, which should appear in the
definition of the defined concept $C$, to corefer with $X$ (see
Section~\ref{block} for an example).  A drawback in the use of this
operator is the requirement to know the internal syntactical form of
the defined concept, namely, the names of its temporal variables.

%%%%%%%%%%%%%%%%%%%%%%%% Assertions %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Let \Ind\ and \OT\ be two alphabets of symbols denoting {\it
  individuals} and {\it temporal intervals}, respectively. An
assertion -- i.e., a predication on temporally qualified individual
entities -- is a statement of one of the forms $C(i,a),\ p(i,a,b),\ 
\Parm g(a,b),\ R(i,j)$, where $C$ is a concept, $p$ is a feature,\ 
\Parm g is a parametric feature, $R$ is a temporal relation, $a$ and
$b$ denote individuals in \Ind, $i$ and $j$ denote temporal intervals
in \OT.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Informal SEMANTICS %%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsubsection{A clarifying Example}
\label{expressivity}

Let us now informally see the intended {\em meaning\/} of the terms of the
language \TLF\ (for the formal details see Section~\ref{sec-semantics}).
Concept expressions are interpreted over pairs of {\em temporal intervals}
and {\em individuals} $\langle i,a \rangle$, meaning that the individual $a$
is in the extension of the concept at the interval $i$. If a concept is
intended to describe an action, then its interpretation can be seen as the
set of individual actions of that type occurring at some interval.

Within a concept expression, the special ``\NOW'' variable denotes the
current interval of evaluation; in the case of actions, it is thought
that it refers to the temporal interval at which the action itself
{\em occurs}. The temporal existential quantifier introduces interval
variables, related to each other and possibly to the \NOW\ variable in
a way defined by the set of {\em temporal constraints}. To
evaluate a concept at an interval $X$, different from the current one,
it is necessary to temporally qualify it at $X$ -- written $C@X$; in this way,
every occurrence of \NOW\ embedded within the concept expression $C$
is interpreted as the $X$ variable\footnote{Since any concept is
  implicitly temporally qualified at the special \NOW\ variable, it is
  not necessary to explicitly qualify concepts at \NOW.}.  The
informal meaning of a concept with a temporal existential
quantification can be understood with the following examples in the
action domain.

\vspazio\noindent
${\tt Basic\mbox{-}Stack} ~ \doteq ~ 
   \SST {(x\ y)} {(x\ {\sf m}\ \NOW)(\NOW\ {\sf m}\ y)}
        \mbox{\Large(}
         ({\tt \Parm BLOCK}: {\tt OnTable})@x\ \AND\ 
         ({\tt \Parm BLOCK}: {\tt OnBlock})@y 
         \mbox{\Large)}
$
\vspazio

\noindent Figure~\ref{examples} shows the temporal dependencies of the 
intervals in which the concept {\tt Basic\mbox{-}Stack} holds.  {\tt
  Basic\mbox{-}Stack} denotes, according to the definition (a
terminological axiom), any action occurring at some interval involving
a ${\tt \Parm BLOCK}$ that was once {\tt OnTable} and then {\tt
  OnBlock}. The \NOW\ interval could be understood as the occurring
time of the action type being defined: referring to it within the
definition is an explicit way to temporally relate states and actions
occurring in the world with respect to the occurrence of the action
itself. The temporal constraints $(x\ {\sf m}\ \NOW)$ and $(\NOW\ {\sf
  m}\ y)$ state that the interval denoted by $x$ should meet the
interval denoted by \NOW\ -- the occurrence interval of the action
type {\tt Basic\mbox{-}Stack} -- and that \NOW\ should meet $y$.  The
parametric feature ${\tt \Parm BLOCK}$ plays the role of {\em formal}
parameter of the action, mapping any individual action of type {\tt
  Basic\mbox{-}Stack} to the block to be stacked, independently from
time.  Please note that, whereas the existence and identity of the
${\tt \Parm BLOCK}$ of the action is time invariant, it can be
qualified differently in different intervals of time, e.g., the ${\tt
  \Parm BLOCK}$ is necessarily {\tt OnTable} only during the interval
denoted by $x$.

\begin{figure}[t]
\begin{center}
\setlength{\unitlength}{0.16in}
\begin{picture}(18,3.5)(0,0)
{\footnotesize
\thicklines
\put(-1, 1){\vector( 1, 0){5}}
\put(4, 3){\vector( 1, 0){5}}
\put(18,1){\vector(-1, 0){9}}
\put(4, 1){\vector(-1, 0){5}}
\put(9, 3){\vector(-1, 0){5}}
\put(9, 1){\vector( 1, 0){9}}
\put(-1,1.4){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\tt OnTable(BLOCK)}}}
\put(4,3.5){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\tt Basic\mbox{-}Stack(BLOCK)}}}
\put(9,1.4){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\tt OnBlock(BLOCK)}}}
\put(0,0.3){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\it x}}}
\put(5,2.3){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]\NOW}}
\put(10,0.3){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\it y}}} }
\end{picture}
\end{center}\vspace{-1em}
\caption[examples]{\label{examples}
Temporal dependencies in the definition of the {\tt Basic\mbox{-}Stack} 
action.}
\end{figure}

Let us comment now on the introduction of explicit temporal variables.
The absence of explicit temporal variables would weaken the temporal
structure of a concept since arbitrary relationships between more than
two intervals could not be represented anymore. For example, having
only implicit intervals it is not possible to describe the situation
in which two concept expressions, say $C$ and $D$, hold at two meeting
intervals (say $x$, $y$) with the first interval starting and the
second finishing the reference interval (i.e., the temporal pattern
$(x\ {\sf meets}\ y)(x\ {\sf starts}\ \NOW) (y\ {\sf finishes}\ \NOW)$
cannot be represented). More precisely, it is not possible to
represent temporal relations between more than two intervals if they
are not derivable by the temporal propagation of the constraints
imposed on pairs of variables. While explicit variables go against the
general thrust of Description Logics, the gained expressive power
together with the observation that the variables are limited only to
the temporal part of the language are the main motivations for using
them. However, it is easy to drop them by limiting the temporal
expressiveness as proposed by Bettini~\citeyear{bettini:dke-97} (see also
Section~\ref{related}).

An assertion of the type {\tt Basic-Stack}$(i,a)$ states that the
individual $a$ is an action of the type {\tt Basic-Stack} occurred at
the interval $i$.  Moreover, the same assertion implies that $a$ is
related to a ${\tt \Parm BLOCK}$ , say $b$, which is of type {\tt
  OnTable} at some interval $j$, meeting $i$, and of type {\tt
  OnBlock} at another interval $l$, met by $i$.

\vspazio\noindent
${\tt Basic\mbox{-}Stack}(i,a)\Longrightarrow
\exists b\per\ {\tt \Parm BLOCK}(a,b)\wedge\exists j,l\per\ 
     (
     \parbox[t]{15em}{$
     {\tt OnTable}(j,b) \wedge {\tt OnBlock}(l,b) \wedge\\
     {\sf m}(j,i) \wedge {\sf m}(i,l))
     $}
$
\vspazio

\noindent An individual action is an object in the conceptual domain associated
with the relevant properties -- or states -- of the world affected by
the individual action itself via a bunch of {\em features}; moreover,
temporal relations constrain time intervals imposing an ordering in
the change of the states of the world.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% SEMANTICS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{Semantics}
\label{sec-semantics}

\begin{figure}[t]
{\normalsize
\begin{center}
\begin{lefteqnarrayfig}
\EPS{{\sf s}}     & = & \set{\langle [u,v],[u_1,v_1]\rangle 
                             \in \IS\times \IS\mid u=u_1 \wedge v<v_1}\\
\EPS{{\sf f}}     & = & \set{\langle [u,v],[u_1,v_1]\rangle 
                             \in \IS\times \IS\mid v=v_1 \wedge u_1<u}\\
\EPS{{\sf mi}}    & = & \set{\langle [u,v],[u_1,v_1]\rangle 
                             \in \IS\times \IS\mid u=v_1}\\
                  & \ldots & \mbox{\em (meaning of the other 
                                       Allen temporal relations)}\\
\EPS{R\mbox{\large \bf \ ,\ }S} 
                  & = & \Eps{R}\cup\Eps{S}\\
\Eps{\langle \overline{X},\overline{\TC}\rangle }
                  & = & \{ %\parbox[t]{7.5cm}{$
                           \V: \overline{X} \mapsto \IS \mid \ %\
                           \forall(X\ (R)\ Y)\in\overline{\TC}\per\
                               %\parbox[t]{4cm}{$
                               \langle \V(X),\V(Y)\rangle \in\Eps{R} \}. %$}
                              %$}
\end{lefteqnarrayfig}
\end{center}}
\ \hrulefill
\caption[t-semantics]{\label{t-semantics}
The temporal interpretation function.}
\end{figure}

In this Section, a Tarski-style extensional semantics for the \TLF\ 
language is given, and a formal definition of the subsumption and
recognition reasoning tasks is devised.  

Assume a linear, unbounded, and dense temporal structure $\TS
=(\P,<)$, where $\P$ is a set of time points and $<$ is a strict
partial order on $\P$.  In such a structure, given an interval $X$ and
a temporal relation $R$, it is always possible to find an interval $Y$
such that $(X~(R)~Y)$. The assumption of linear time -- which means
that for any two points $t_1$ and $t_2$ such that $t_1 \leq t_2$ the
set of points $\{t \mid t_1 \leq t \leq t_2\}$ is totally ordered --
fits the intuition about the nature of time, so that the pair
$[t_1,t_2]$ can be thought as the closed interval of points between
$t_1$ and $t_2$. The {\em interval set} of a structure $\TS$ is
defined as the set \IS\ of all closed intervals $[u,v] \doteq \set{ x
  \in \P \mid u \leq x \leq v, u\neq v}$ in $\TS$.

A {\em primitive interpretation\/} $\I \doteq \langle \IS, \Dom,
\Int\cdot \rangle $ consists of a set \IS\ (the {\em interval set} of
the selected temporal structure $\TS$), a set $\Dom$ (the {\em domain}
of $\I$), and a function $\Int{\cdot}$ (the {\em primitive
  interpretation function} of $\I$) which gives a meaning to atomic
concepts, features and parametric features:

\begin{leftarray}
   \Int A \subseteq \IS\times\Dom\ ; \tab
   \Int f : (\IS\times\Dom)\stackrel{partial}{\longmapsto} \Dom\ ; \tab
   \Int {\Parm g}: \Dom\stackrel{partial}{\longmapsto}\Dom
\end{leftarray}

\noindent Atomic parametric features are interpreted as partial functions; 
they differ from atomic features for being independent from time.

In order to give a meaning to temporal expressions present in generic
concept expressions, Figure~\ref{t-semantics} defines the {\em
  temporal interpretation function}.  The {\em temporal interpretation
  function} $\Eps\cdot$ depends only on the temporal structure $\TS$.
The labeled directed graph $\langle \overline{X},
\overline{\TC}\rangle$ -- where $\overline{X}$ is the set of variables
representing the nodes, and $\overline{\TC}$ is the set of temporal
constraints representing the arcs -- is called {\em temporal
  constraint network}. The interpretation of a temporal constraint
network is a set of variable assignments that satisfy the temporal
constraints. A {\em variable assignment} is a function $\V :
\overline{X}\mapsto\IS$ associating an interval value to a temporal
variable. A temporal constraint network is {\em consistent} if it
admits a non empty interpretation. The notation, $\Eps{\langle
  \overline{X}, \overline{\TC}\rangle _{\set{x_1\mapsto t_1,
      x_2\mapsto t_2,\ldots}}}$, used to interpret concept
expressions, denotes the subset of $\Eps{\langle \overline{X},
  \overline{\TC}\rangle}$ where the variable $x_i$ is mapped to the
interval value $t_i$.

It is now possible to interpret generic concept expressions. Consider
the equations introduced in Figure~\ref{c-semantics}. An {\em
  interpretation function}\ $\Intth\cdot$, based on a variable
assignment $\V$, an interval $t$ and a set of constraints
$\H=\set{x_1\mapsto t_1, \ldots}$ over the assignments of inner
variables, extends the primitive interpretation function in such a way
that the equations of Figure~\ref{c-semantics} are satisfied.
Intuitively, the interpretation of a concept $\Intth{C}$ is the set of
entities of the domain that are of type $C$ at the time interval $t$,
with the assignment for the free temporal variables in $C$ given by
$\V$ -- see $\INTTH{C @ X}$ -- and with the constraints for the
assignment of variables in the scope of the outermost temporal
quantifiers given by $\H$.  Note that, $\H$ interprets the variable
renaming due to the temporal substitutive qualifier -- see $\INTTH{C [
  Y ] @ X}$ -- and it takes effect during the choice of a variable
assignment, as the equation for
$\INTTH{\SST{(\overline{X})}{\overline{\TC}}{C}}$ shows.

\begin{figure}[t]
{\normalsize
\begin{center}
\begin{lefteqnarrayfig}
\Intth{A}            & = & \set{ a\in\Dom\mid \langle t,a\rangle  \in \Int A} 
                     ~~=~~  \Nint{A} \\
\Intth\top           & = & \Dom 
                     ~~=~~  \Int\top \\
\INTTH{C\AND D}      & = & \Intth C \cap \Intth D  \\
\INTTH{p\AGREE q}    & = & \set{ a\in \Fdom{\Nint p}\cap\Fdom{\Nint q}\mid
                                                   \Nint p (a) = \Nint q (a) }
                     ~~=~~  \NINT{p\AGREE q}  \\
\INTTH{p:C}          & = & \set{ a\in \Fdom{\Nint p} \mid 
                                                   \Nint p(a) \in\Intth C} \\
\INTTH{C @ X}        & = & \Inthx{C}{\V(X)}\H  \\
\INTTH{C[Y] @ X}     & = & \Inthx{C}{t}{\H\cup\set{Y\mapsto \V(X)}}  \\
\INTTH{\SST {(\overline{X})}{\overline{\TC}}{C}} 
                                            & = & \set{ a\in \Dom\mid
                                                   \exists \W \per\ \W\in
                                                    \Eps{\langle  \overline{X},\overline{\TC}
                                                     \rangle _{\H\cup\set{\NOW\mapsto t}}}
                                                      \wedge a \in\Int{C}_{\W,t,\emptyset}}\\
\Nint{f}             & = & %\parbox[t]{7.5cm}{$
                           \hat{f}_t:\Dom\stackrel{partial}{\longmapsto}\Dom \mid \ %\
                            \forall a\per\ 
                              \parbox[t]{15em}{$ 
                              (a\in\Fdom{\hat{f}_t}
                              \leftrightarrow %\\
                              \langle t,a\rangle  \in \Fdom{\Int f}) \wedge \\
                              \hat{f}_t(a)  = \Int f (t,a) 
                              %$} 
                              $} \\
\NINT{p\CHAIN q}     & = & \Nint {p} \CHAIN \Nint {q} \\
\Nint{\Parm g}       & = & \Int{\Parm g}
\end{lefteqnarrayfig}
\end{center}}
\ \hrulefill
\caption[c-semantics]{\label{c-semantics}
The interpretation function.}
\end{figure}

In absence of free variables in the concept expression -- with the
exception of \NOW -- for notational simplification the {\em natural}
interpretation function $\Nint{C},$ being equivalent to the
interpretation function $\Intth{C}$ with any $\V$ such that
$\V(\NOW)=t$ and $\H=\emptyset$ is introduced. The set of
interpretations $\set{\Intth{C}}$ obtained by varying $\I,\V,t$ with a
fixed $\H$ is maximal wrt set inclusion if $\H=\emptyset$, i.e., the
set of natural interpretations includes any set of interpretations
with a fixed $\H$.  In fact, since $\H$ represents a constraint in the
assignment of variables, the unconstrained set is the larger one. Note
that, for feature interpretation only the natural one is used since it
is not admitted to temporally qualify them.

An interpretation $\I$ satisfies the terminological axiom $A\doteq C$
iff $\Nint A = \Nint C$, for every $t$.  A concept $C$ is {\em
  subsumed\/} by a concept $D$ ($C\SUBSUMEDBY D$) if $\Nint C
\subseteq \Nint D$ for every interpretation $\I$ and every interval
$t$.  An interpretation $\I$ is a {\em model\/} for a concept $C$ if
$\Nint C \neq \emptyset$ for some $t$. If a concept has a model, then
it is {\em satisfiable}, otherwise it is {\em unsatisfiable}.

Each \TLF\ concept expression is always satisfiable, with
the proviso that the temporal constraints introduced by the
existential quantifiers are consistent.  This latter condition can be
easily checked during the reduction of the concept into a {\em normal
  form} when the {\it minimal} temporal network (see
Section~\ref{normal-form}, definition~\ref{temp-comp}) is computed.

It is interesting to note that only the relations {\sf s,\ f,\ mi\ }
are really necessary, because it is possible to express any temporal
relationship between two distinct intervals using only these three
relations and their transpositions {\sf si,\ fi,\ 
  m}~\cite{halpern:shoham:91}. The following equivalences hold:

\begin{lefteqnarray}
\SST{x}{(x\ {\sf a}\ \NOW)}{C@x} & \equiv & 
 \SST{xy}{(y\ {\sf mi}\ \NOW)(x\ {\sf mi}\ y)}{C@x}
\\
\SST{x}{(x\ {\sf d}\ \NOW)}{C@x} & \equiv & 
  \SST{xy}{(y\ {\sf s}\ \NOW)(x\ {\sf f}\ y)}{C@x}
\\
\SST{x}{(x\ {\sf o}\ \NOW)}{C@x} & \equiv & 
  \SST{xy}{(y\ {\sf s}\ \NOW)(x\ {\sf fi}\ y)}{C@x}
\end{lefteqnarray}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ABox %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

To assign a meaning to ABox axioms, the temporal interpretation
function $\Eps\cdot$ is extended to temporal intervals so that $\Eps
i$ is an element of \IS\ for each $i\in \OT$.  The semantics of
assertions is the following: $C(i,a)$ is satisfied by an
interpretation $\I$ iff $\Int a \in\Int{C}_{\Eps i}$; $p(i,a,b)$ is
satisfied by $\I$ iff $\Int{p}_{\Eps i}(\Int a) = \Int b$; $\Parm
g(a,b)$ is satisfied by $\I$ iff $\Int{\Parm g}(\Int a) = \Int b$; and
$R(i,j)$ is satisfied by $\I$ iff $\langle \Eps i,\Eps j\rangle
\in\Eps{R}$.  Given a knowledge base $\Sigma$, an individual $a$ in
$\Ind$ is said to be an {\em instance} of a concept $C$ {\em at the
  interval $i$} if $\Sigma \models C(i,a)$.

Now we are able to give a semantic definition for the reasoning task
we already called {\it specific plan recognition with respect to a
  plan description}. This is an inference service that computes if an
{\em individual action/plan} is an instance of an {\em action/plan
  type} at a certain interval, i.e., the task known as instance
recognition in the Description Logic community. Given a knowledge base
$\Sigma$, an interval $i$, an individual $a$ and a concept $C$, the
{\em instance recognition problem} is to test whether $\Sigma\models
C(i,a)$.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%\begin{array}[t]
\begin{figure}
\begin{center}
\setlength{\unitlength}{0.175in}
\begin{picture}(18,3.4)(0,0)
{\footnotesize 
\thicklines
\put(0, 1){\vector( 1, 0){8}}
\put(10, 3){\vector( 1, 0){8}}
\put(18,1){\vector(-1, 0){8}}
\put(8, 1){\vector(-1, 0){8}}
\put(18, 3){\vector(-1, 0){8}}
\put(10,1){\vector( 1, 0){8}}
\put(0,1.4){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\tt Make-Spaghetti}}}
\put(10,1.4){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\tt Boil}}}
\put(10,3.4){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\tt Boil-Spaghetti}}}
\put(1,0.3){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\it x}}}
\put(11,0.3){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]\NOW}}
\put(11,2.3){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]\NOW}} }
\end{picture}
\end{center}
\caption[marinara-1]{\label{marinara-1}
Temporal dependencies in the definition of the {\tt Boil\mbox{-}Spaghetti}
plan.}
\end{figure}

\section{Action and plan representation: two examples}
\label{two-examples}

An action description represents how the world state may evolve in
relation with the possible occurrence of the action itself. A plan is
a complex action: it is described by means of temporally related world
states and simpler actions. The following introduces examples of
action and plan representations from two well known domains, the
cooking domain~\cite{kautz:91,weida:litman:kr-92} and the block
world~\cite{allen:91}, with the aim of showing the applicability of
our framework.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Cooking %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{The Cooking Domain}
\label{cook}

Let us introduce the plan {\tt Boil-Spaghetti}: 

\vspazio
\noindent$
{\tt Boil\mbox{-}Spaghetti} ~~ \doteq ~~ 
   \SST {x} {(x\ {\sf b}\ \NOW)}
        {({\tt Make\mbox{-}Spaghetti}@x  \AND {\tt Boil})}
$
\vspazio

\begin{figure}[t]
\begin{center}
\setlength{\unitlength}{0.175in}
\begin{picture}(18,5.4)(0,0)
{\footnotesize 
\thicklines
\put(0, 1){\vector( 1, 0){5}}
\put(6, 3){\vector( 1, 0){5}}
\put(11,1){\vector(-1, 0){5}}
\put(5, 1){\vector(-1, 0){5}}
\put(11,3){\vector(-1, 0){5}}
\put(6, 1){\vector( 1, 0){5}}
\put(2, 5){\vector( 1, 0){7}}
\put(9, 5){\vector(-1, 0){7}}
\put(12,5){\vector( 1, 0){6}}
\put(18,5){\vector(-1, 0){6}}
\put(0,1.4){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\tt Make\mbox{-}Spaghetti}}}
\put(6,3.4){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\tt Boil\mbox{-}Spaghetti}}}
\put(6,1.4){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\tt Boil}}}
\put(2,5.4){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\tt Make\mbox{-}Marinara}}}
\put(12,5.4){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\tt Put\mbox{-}Together\mbox{-}SM}}}
\put(1,0.3){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\it x}}}
\put(7,2.3){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\it y}}}
\put(7,0.3){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\it y}}}
\put(3,4.3){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\it z}}}
\put(13,4.3){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\it w}}}
}
\end{picture}
\end{center}
\caption[ASM]{\label{ASM}
  Temporal dependencies in the definition of {\tt
    Assemble\mbox{-}Spa\-ghet\-ti\mbox{-}Ma\-ri\-na\-ra}.}
\end{figure}
%%%

\noindent Figure~\ref{marinara-1} shows the temporal dependencies of the 
intervals in which the concept {\tt Boil-Spa\-ghet\-ti} holds. The
definition employs the \NOW\ interval to denote the occurrence time of
the plan itself; in this way, it is possible to describe how different
actions or states of the world concurring to the definition of the
plan are related to it. This is why the variable \NOW\ is explicitly
present in the definition of {\tt Boil\mbox{-}Spaghetti}, instead of a
generic variable: the {\tt Boil} action should take place at the same
time of the plan itself, while {\tt Make\mbox{-}Spaghetti} occurs
before it. 

The definition of a plan can be reused within the definition of other
plans by exploiting the full compositionality of the language.  The
plan defined above {\tt Boil\mbox{-}Spaghetti} is used in the
definition of {\tt
  As\-sem\-ble\mbox{-}Spa\-ghet\-ti\mbox{-}Ma\-ri\-na\-ra}:

\vspazio
\noindent$
{\tt Assemble\mbox{-}Spaghetti\mbox{-}Marinara} ~~ \doteq ~~ \SOMETIME 
      (y\ z\ w)\ 
      \parbox[t]{18em}{$
       (y\ {\sf b}\ w)(z\ {\sf b}\ w) \per\ \\
       (\parbox[t]{16em}{$
         {\tt Boil\mbox{-}Spaghetti}@y \AND \\
         {\tt Make\mbox{-}Marinara}@z \AND \\
         {\tt Put\mbox{-}Together\mbox{-}SM}@w
       )
       $}$}
$
\vspazio

\noindent 
In this case, precise temporal relations between the nodes of two
corresponding temporal constraint networks are asserted: e.g., the
action {\tt Put\mbox{-}Together\mbox{-}SM} takes place strictly after
the {\tt Boil} action (Figure~\ref{ASM}).  Observe that the occurrence
interval of the plan {\tt
  Assemble\mbox{-}Spa\-ghet\-ti\mbox{-}Ma\-ri\-na\-ra} does not appear
in the Figure because it is not temporally related with any other
interval.

A plan subsuming {\tt Assemble\mbox{-}Spaghetti\mbox{-}Marinara} is
the more general plan defined below, {\tt
  Pre\-p\-are\mbox{-}Spa\-ghet\-ti}, supposing that the action {\tt
  Make\mbox{-}Sauce} subsumes {\tt Make\mbox{-}Marina\-ra}. This means
that among all the individual actions of the type {\tt
  Prepare\mbox{-}Spa\-ghet\-ti} there are all the individual actions
of type {\tt Assemble\mbox{-}Spa\-ghet\-ti\mbox{-}Ma\-ri\-na\-ra}:

\vspazio
\noindent$
{\tt Prepare\mbox{-}Spaghetti} ~~ \doteq ~~ \SOMETIME\ (y\ z)\ ()\per\ 
( %\parbox[t]{4cm}{$ 
     {\tt Boil\mbox{-}Spaghetti}@y \AND %\\
     {\tt Make\mbox{-}Sauce}@z) %$}
      $
\vspazio

\noindent  
However, note that {\tt Boil\mbox{-}Spaghetti} does not subsume {\tt
  Pre\-pa\-re\mbox{-}Spa\-ghet\-ti}, even if it is a conjunct in the
definition of the latter. This could be better explained observing
how the definition of {\tt Prepare\mbox{-}Spaghetti} plan is expanded:

\vspazio
\noindent$
{\tt Prepare\mbox{-}Spaghetti} ~~ \doteq ~~ \SOMETIME\ (x\ y\ z)\ 
  (x\ {\sf b}\ y)\per\ 
  ( \parbox[t]{15em}
    {$ {\tt Make\mbox{-}Spaghetti}@x \AND {\tt Boil}@y \AND  \\
       {\tt Make\mbox{-}Sauce}@z) $}$
\vspazio

\noindent Then, the {\tt Boil} action occurs at the interval
$y$ -- which can be different from the occurring time of {\tt
  Pre\-pa\-re\mbox{-}Spa\-ghet\-ti} -- as the effect of binding {\tt
  Boil\mbox{-}Spaghetti} to the temporal variable $y$. On the
contrary, in the definition of {\tt Boil\mbox{-}Spaghetti} the {\tt
  Boil} action takes place {\em necessarily} at the same time.
Subsumption between {\tt Prepare\mbox{-}Spaghetti} and {\tt
  Boil\mbox{-}Spaghetti} fails since different temporal relations
between the actions describing the two plans and the plans themselves
are specified.  In particular, observe that the {\tt
  Boil\mbox{-}Spaghetti} plan denotes a narrower class than the plan
expression

\vspazio
\noindent$
\SST {(x\ y)} {(x\ {\sf b}\ y)}
    {({\tt Make\mbox{-}Spaghetti}@x \AND {\tt Boil}@y)}$
\vspazio

\noindent which subsumes both {\tt Prepare\mbox{-}Spaghetti} and {\tt
  Bo\-il\mbox{-}Spa\-ghetti} itself.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% STACK %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{The Blocks World Domain}
\label{block}

As a further example of the expressive power of the temporal language,
it is now shown how to represent the {\tt Stack} action in the blocks world,
in a more detailed way than the previous simple {\tt Basic-Stack}
action used as a clarifying example.  Thus a stacking action involves
two blocks, which should be both clear at the beginning; the central
part of the action consists of grasping one block; at the end, the
blocks are one on top of another, and the bottom one is no longer
clear (Figure~\ref{allen-stack}).

Our representation borrows from the \Rat\ Description
Logic~\cite{heinsohn:et:al:ijcai-93} the intuition of representing
action parameters by means of partial functions mapping from the
action itself to the involved action parameter (see
Section~\ref{related}). In the language, these functions are called
{\em parametric features}. For example, the action {\tt Stack} has the
parameters {\tt \Parm OBJECT1} and {\tt \Parm OBJECT2}, representing
in some sense the objects that are involved in the action
independently from time.  So, in the assertion ``${\tt \Parm OBJECT1}
(a,block\mbox{-}a)$'', $block\mbox{-}a$ denotes the first object
involved in the action $a$ at any interval. On the other hand, an
assertion involving a (non-parametric) feature, e.g., ``${\tt ON}
(i,block\mbox{-}a, block\mbox{-}b)$'', does not imply anything about
the truth value at intervals other than $i$.

\begin{figure}[t]
\begin{center}
\setlength{\unitlength}{0.009in}
\begin{picture}(400,95)(20,670)
{\footnotesize 
\thicklines
\put(120,760){\vector(-1, 0){  0}}
\put(120,760){\vector( 1, 0){180}}
\put(160,720){\vector(-1, 0){  0}}
\put(160,720){\vector( 1, 0){140}}
\put(420,720){\vector(-1, 0){120}}
\put( 20,720){\vector( 1, 0){140}}
\put( 20,680){\vector( 1, 0){280}}
\put(400,680){\vector(-1, 0){100}}
\put(160,725){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\tt Holding-Block(OBJ1)}}}
\put( 20,685){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\tt Clear-Block(OBJ2)}}}
\put(300,685){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\tt ON(OBJ1, OBJ2)}}}
\put( 20,725){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\tt Clear-Block(OBJ1)}}}
\put(300,725){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\tt Clear-Block(OBJ1)}}}
\put(120,765){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\tt Stack(OBJ1, OBJ2)}}}
\put(180,710){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\it w}}}
\put( 40,670){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\it x}}}
\put(320,670){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\it y}}}
\put( 40,710){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\it v}}}
\put(320,710){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\it z}}}
\put(140,750){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]\NOW}}
}
\end{picture}
\end{center}
\caption[allen-stack]{\label{allen-stack}
Temporal dependencies in the definition of the {\tt Stack} action.  }
\end{figure}

The concept expression, which defines the {\tt Stack} action, makes use of
temporal qualified concept expressions, including feature {\em selections}
and {\em agreements}: the expression $({\tt \Parm OBJECT2}:$ ${\tt
  Clear\mbox{-}Block})@x$ means that the second parameter of the action
should be a {\tt Clear\mbox{-}Block} at the interval denoted by $x$; while
$({\tt \Parm OBJECT1}\!\CHAIN\!{\tt ON}\AGREE{\tt \Parm OBJECT2})@y$
indicates that at the interval $y$ the object {\tt on} which {\tt \Parm
  OBJECT1} is placed is {\tt \Parm OBJECT2}.  The formal definition of the
action {\tt Stack} is:

\vspazio\noindent
$
{\tt Stack} ~ ~ \doteq ~ ~ \SOMETIME 
  \parbox[t]{75ex}{$
       (x\ y\ z\ v\ w)\ \ 
       (x\ {\sf fi}\ \NOW)
       (y\ {\sf mi}\ \NOW) 
       (z\ {\sf mi}\ \NOW)
       (v\ {\sf o}\ \NOW)
       (w\ {\sf f}\ \NOW)
       (w\ {\sf mi}\ v) \per\\
       \mbox{\large (}
       \parbox[t]{70ex}{$
        ({\tt \Parm OBJECT2}: {\tt Clear\mbox{-}Block})@x \AND 
        ({\tt \Parm OBJECT1}\!\CHAIN\!{\tt ON}\AGREE{\tt \Parm OBJECT2})@y \AND\\
        ({\tt \Parm OBJECT1}:{\tt Clear\mbox{-}Block})@v \AND
        ({\tt \Parm OBJECT1}:{\tt Holding\mbox{-}Block})@w \AND\\
        ({\tt \Parm OBJECT1}:{\tt Clear\mbox{-}Block})@z      
      \mbox{\large )}
      $}
  $}
$
\vspazio

\noindent 
The above defined concept does not state which properties are the
prerequisites for the stacking action or which properties must be true
whenever the action succeeds.  What this action intuitively states is
that {\tt \Parm OBJECT1} will be on {\tt \Parm OBJECT2} in a situation
where both objects are clear at the start of the action. Note that the
world states described at the intervals denoted by $v,w,z$ are the
result of an action of {\em grasping} a previously clear block:

\vspazio\noindent
$
{\tt Grasp} ~ ~ \doteq ~ ~ \SOMETIME 
  \parbox[t]{75ex}{$
       (x\ w\ z)\ \ 
       (x\ {\sf o}\ \NOW) (w\ {\sf f}\ \NOW)
       (w\ {\sf mi}\ x) (z\ {\sf mi}\ \NOW) \per\\
       \mbox{\large (}
       \parbox[t]{70ex}{$
         ({\tt \Parm OBJECT1}:{\tt Clear\mbox{-}Block})@x \AND\
         ({\tt \Parm OBJECT1}:{\tt Holding\mbox{-}Block})@w \AND\\
         ({\tt \Parm OBJECT1}:{\tt Clear\mbox{-}Block})@z
      \mbox{\large )}
      $}
  $}
$
\vspazio

\noindent 
The {\tt Stack} action can be redefined by making use of the {\tt
  Grasp} action:

\vspazio\noindent
$
{\tt Stack} ~\doteq~ \SOMETIME 
  \parbox[t]{75ex}{$
       (x\ y\ u\ v)\ \ 
       (x\ {\sf fi}\ \NOW)
       (y\ {\sf mi}\ \NOW)
       (u\ {\sf f}\ \NOW)
       (v\ {\sf o}\ \NOW) \per\\
       \mbox{\large (}
       \parbox[t]{70ex}{$         
         ({\tt \Parm OBJECT2}: {\tt Clear\mbox{-}Block})@x \AND
         ({\tt \Parm OBJECT1}\!\CHAIN\!{\tt ON}\AGREE{\tt \Parm OBJECT2})@y
         \AND \\
         ({\tt Grasp}[x]@v)@u
      \mbox{\large )}
      $}
  $}
$
\vspazio

\noindent 
The temporal substitutive qualifier $({\tt Grasp}[x]@v)$ {\em renames}
within the defined {\tt Grasp} action the variable $x$ to $v$ and it
is a way of making coreference between two temporal variables, while
the temporal constraints peculiar to the renamed variable $x$ are
inherited by the substituting interval $v$. Furthermore, the effect of
temporally qualifying the grasping action at $u$ is that the \NOW\ 
variable associated to the grasping action -- referring to the
occurrence time of the action itself -- is bound to the interval
denoted by $u$.  Because of this binding on the occurrence time of the
grasping action, the \NOW\ variable in the grasping action and the
\NOW\ variable in the stacking action denote different time intervals,
so that the grasping action occurs at an interval finishing the
occurrence time of the stacking action.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% INSTANCE %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
Now it is shown how from a series of outside observations action
recognition can be performed -- i.e., the task called {\em specific
  plan recognition with respect to a plan description}.  The following
ABox describes a situation in which blocks can be {\em clear}, {\em
  grasped} and/or {\em on} each other, and in which a generic
individual action $a$ is taking place at time interval $i_a$ having
the blocks {\em block-a} and {\em block-b} as its parameters:

\begin{leftarray}
{\tt \Parm OBJECT1}(a,block\mbox{-}a),\ 
{\tt \Parm OBJECT2}(a,block\mbox{-}b),\\
{\sf o}(i_1,i_a),\ {\tt Clear\mbox{-}Block}(i_1,block\mbox{-}a), \  %\
{\sf fi}(i_2,i_a),\ {\tt Clear\mbox{-}Block}(i_2,block\mbox{-}b), \\
{\sf mi}(i_3,i_1),\ {\sf f}(i_3,i_a),\ 
{\tt Holding\mbox{-}Block}(i_3,block\mbox{-}a),\\  
{\sf mi}(i_4,i_a),\ {\tt Clear\mbox{-}Block}(i_4,block\mbox{-}a),\  
{\sf mi}(i_5,i_a),\ {\tt ON}(i_5,block\mbox{-}a,block\mbox{-}b)
\end{leftarray}

\noindent 
The system deduces that, in the context of a knowledge base $\Sigma$
composed by the above ABox and the definition of the {\tt Stack}
concept in the TBox, the individual action $a$ is of type {\tt Stack}
at the time interval $i_a$, i.e., $\Sigma \models {\tt Stack}(i_a,a)$.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%% CALCULUS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{figure}[t]
{\footnotesize 
\begin{lefteqnarrayfig}
  C@X\AND D@X & \rightarrow & (C\AND D)@X \\
  (C@X_1)@X_2 & \rightarrow &  C@X_1  \\
  (C@X_1 \AND D)@X_2 & \rightarrow &  C@X_1 \AND D@X_2 \\
  C\AND \SST {(\overline{X})}{\overline{\TC}}{D} & \rightarrow & \SST
  {(\overline{X})}{\overline{\TC}}{(C\AND D)}
  \\
  & & \mbox{{\sl if} $C$ {\sl doesn't contain free variables}}
  \\
  \SOMETIME (\overline{X})\overline{\TC}_1 \per \mbox{\Large (}C \AND & & \\
    \left[\left( \SST {(\overline{Y})}{\overline{\TC}_2}{D}\right)
      [Y_1]@X_1\ldots[Y_p]@X_q\right]\!@X \mbox{\Large )} & \rightarrow &
  \SOMETIME (\overline{X}\uplus_{[Y_1/X_1]\ldots[Y_p/X_q]} \overline{Y})
  \overline{\TC}_1\cup \overline{\TC}_{2+_{[\NOW/X]}}\per (C\AND D_+@X)
  \\
  & & \mbox{{\sl if} $D$ {\sl doesn't contain existential 
            temporal quantifiers}}\\
  p:(q:C)            & \rightarrow & (p\CHAIN q):C  \\
  p:(C \AND D)       & \rightarrow & p:C \AND p:D   \\
  p:(q_1 \AGREE q_2) & \rightarrow & p \CHAIN q_1 \AGREE p \CHAIN q_2 
\end{lefteqnarrayfig}

\vspace{1em} 

{\em Prescriptions: } $\overline{X}\uplus_{[Y_1/X_1]\ldots[Y_p/X_q]}
\overline{Y}$ returns the union of the two sets of variables
$\overline{X}$ and $\overline{Y}$, where each occurrence of
$Y_1,\ldots,Y_p$ is substituted by $X_1,\ldots,X_q$,
respectively, while all the other elements of $\overline{Y}$ occurring
in $\overline{X}$ are renamed with fresh new identifiers.  $Z_+$ is
intended to be the expression $Z$ where the same substitution or
renaming has taken place. The condition on the last rule forces
application to start from the last nested existential temporal
qualified concept.

\ \hrulefill
}
\caption[normal-form]{\label{normal-form}
  Rewrite rules to transform an arbitrary concept into an existential
  concept.}
\end{figure}
%%%%%%%%%%%%%%%%%%%%

\section{The Calculus for \TLF}
\label{calculus}

This Section presents a calculus for deciding subsumption between
temporal concepts in the Description Logic \TLF. The calculus is based
on the idea of separating the inference on the temporal part from the
inference on the Description Logic part. This is achieved by first
looking for a {\em normal form} of concepts.  Concept subsumption in
the temporal language is then reduced to concept subsumption between
non-temporal concepts and to subsumption between temporal constraint
networks. 

%%In the following, we will write ``$\SUBSUMES_{\footnotesize\F}$'' for
%%subsumption between non-temporal \F\ concepts.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Normal form %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{Normal Form}
\label{normal-concept}

Every \TLF\ concept expression can be reduced to an equivalent {\em
  existential concept} of the form: $\SST
{(\overline{X})}{\overline{\TC}}{(Q_0 \AND Q_1@X_1 \AND \ldots \AND
  Q_n@X_n)}$, where each $Q$ is a non-temporal concept, i.e., it is
an element of the language \F.  A concept in existential form can be
seen as a {\em conceptual temporal constraint network}, i.e., a
labeled directed graph $\langle \overline{X}, \overline{\TC},
\overline{Q@X}\rangle $ where arcs are labeled with a set of arbitrary
temporal relationships -- representing their disjunction -- nodes are
labeled with non-temporal concepts and, for each node $X$, the
temporal relation $(X = X)$ is implicitly true. Moreover, since the
normalized concepts do not contain free variables or substitutive
qualifiers, in the following the natural interpretation function (see
Section~\ref{sec-semantics}) is used.
\begin{proposition}[Equivalence of EF] 
  Every concept $C$ can be reduced in linear time into an equivalent
  existential concept $({\sl ef}\ \!C)$, by exhaustively applying the
  set of rewrite rules of Figure~\ref{normal-form}.
\end{proposition}
Note that $({\sl ef}\ \!C)$ makes explicit all the possible chains of
features by reducing each non-temporal concept $Q$ to a conjunction of
atomic concepts, feature selections restricted to atomic concepts and
feature agreements -- i.e., each $Q$ is a feature term
expression~\cite{smolka:jlp-92}.

%%%%%%% COVERING
The normalization proceeds by discovering all the possibles
interactions between nodes with the intention of making explicit all
the implicit information. A crucial temporal interaction occurs when a
node is always coincident with a set of nodes in every possible
interpretation of the temporal network.
\begin{definition}[Covering]{
    Given a temporal constraint network $\langle
    \overline{X},\overline{\TC}\rangle$, let $y \in \overline{X}$ and
    $\overline{Z} = \set{z_1,z_2,\ldots,z_p} \subseteq \overline{X}$,
    with $p\geq 1$, and $y \not\in \overline{Z}$. $\overline{Z}$ is a
    {\it Covering} for $y$ if $\forall \V \in \Eps{\langle
      \overline{X},\overline{\TC}\rangle }$,
    $\V(y)\in\set{\V(z_1),\V(z_2),\ldots,\V(z_p)}$
%%    \vspazio    
%%    $ \V(y) = \left\{ \begin{array}{ll}
%%                        \V(z_1) & \mbox{or} \\
%%                        \V(z_2) & \mbox{or} \\
%%                        \ldots  &           \\
%%                        \V(z_p) &
%%                      \end{array}
%%               \right. $
%%    \vspazio
    and for each $\overline{W} \subset \overline{Z}$, $\overline{W}$
    is not a covering for $y$. If $\overline{Z} = \emptyset$, then $y$ is
    called {\it uncovered}, otherwise $y$ is said {\it covered} by
    $\overline{Z}$.  }
\end{definition}
\begin{proposition}[Covering procedure]\label{cover-prop}{
    Given a temporal constraint network $\langle
    \overline{X},\overline{\TC}\rangle$ in {\em minimal} form (see,
    e.g.,~\cite{van:Beek:jair-96}) and a node $y \in \overline{X}$
    then the procedure described in Figure~\ref{cover-proc} returns
    all the possible coverings for $y$ with size $\geq 2$.  }
\end{proposition}

%%%%%%%%%%% COMPUTING COVERING
\begin{figure}
{\small
{\tt {\bf Procedure} Covering%
  ($\langle \overline{X},\overline{\TC}\rangle,\ y$):}\\
\smalltab\parbox[t]{\textwidth}{
{\tt mid} $\longleftarrow\emptyset$;\\
{\tt result} $\longleftarrow\emptyset$;\\
$\overline{Z} = 
  \{z\in\overline{X}\mid (z\ (=,\dots)\ y)\in \overline{\TC}\}$;\\
$\forall s\in\wp(\overline{Z})$ {\tt\bf do} \\
  \smalltab\parbox[t]{\textwidth}{
  {\tt {\bf if}} $\mid\!s\!\mid\geq 2$ {\tt\bf and} the graph 
     $\langle \overline{X},\overline{\TC}^*\rangle$
     obtained by deleting the ``='' temporal relation between\\
     the node $y$ and each of the nodes in $s$ is inconsistent\\
  {\tt {\bf then} mid} $\longleftarrow$ {\tt mid} $\cup\ \{s\}$;}\\
$\forall s\in$ {\tt mid {\bf do}} \\
  \smalltab\parbox[t]{\textwidth}{
  {\tt {\bf if} $\neg\exists t \in$ {\tt mid}$\per\ t\subseteq s$ \\
  {\tt {\bf then} result} $\longleftarrow$ {\tt result} $\cup\ \{s\}$;}
}
{\tt{\bf return} result}.
}
}

\ \hrulefill
\caption[covering]{\label{cover-proc}
  Procedure which computes a covering.}
\end{figure}
%%%%%%%%%%%

%%%%%%%%%% LCS
The idea behind the covering is that whenever a set of nodes
$\set{z_1,z_2,\ldots,z_p}$ is a covering for $y$ the disjunctive
concept expression $(Q_{z_1} \OR \ldots \OR Q_{z_p})$ should be
conjunctively added to the concept expression $Q_y$. Actually, since
in \TLF\ concept disjunction is not allowed it will be sufficient to
add to the node $y$ the {\em Least Commom Subsumer} ({\sc lcs}) of
$(Q_{z_1} \OR \ldots \OR Q_{z_p})$ as defined below.
\begin{definition}[{\sc lcs}]{
    Let $Q_1,\ldots,Q_n,Q,C$ be \F\ concept expressions. Then, the
    concept $Q =$ ${\sc lcs}\set{Q_1, \ldots,Q_n}$ is such that: $Q_1
    \SUBSUMEDBY Q ~\wedge~ \ldots ~\wedge~ Q_n\SUBSUMEDBY Q$ and there is
    no $C$ such that $Q_1\SUBSUMEDBY C ~\wedge~ \ldots ~\wedge~
    Q_n\SUBSUMEDBY C ~\wedge~ C \SUBSUMED Q$.  }
\end{definition}
%%%%%%%%%%% CEF
Given a concept in existential form, the temporal completion of the
constraint network is computed as described below.
\begin{definition}[Completed existential form]{
    
    The temporal completion of a concept in existential form -- the
    Completed Existential Form, CEF -- is obtained by sequentially
    applying the following steps:

\begin{itemize}
\item~({\em closure}) The transitive closure of the Allen temporal
  relations in the conceptual temporal constraint network is computed,
  obtaining a {\em minimal} temporal network (see,
  e.g.,~\cite{van:Beek:jair-96}).
  
\item~({\em =\ collapsing}) For each equality temporal constraint,
  collapse the equal nodes by applying the following rewrite rule:
  \\
  $ \SST {(\overline{X})}{\overline{\TC}\ (x_i\ =\ x_j)}{Q}
  ~\rightarrow~ \left\{ \begin{array}{ll} \SST {(\overline{X}
        \setminus \{x_j\})}
      {\overline{\TC}_{[x_j/x_i]}}{Q_{[x_j/x_i]}} &
      \mbox{\footnotesize{\sl if} $x_i\neq x_j$ {\sl and} $x_j\neq\NOW$.}\\
      \SST {(\overline{X} \setminus \{x_i\})}
      {\overline{\TC}_{[x_i/\NOW]}}{Q_{[x_i/\NOW]}} &
      \mbox{\footnotesize{\sl if} $x_i\neq x_j$ {\sl and} $x_j =
        \NOW$.}
           \end{array}
               \right.
$
\\
\noindent 
Then apply exhaustively the first rule of Figure~\ref{normal-form}.

\item~({\em covering}) For each $y \in \overline{X}$ let compute the
  covering $= \set{\overline{Z}_1,\ldots,\overline{Z}_n}$ following
  the procedure showed by proposition~\ref{cover-prop}.  Whenever the
  covering is not empty, translate $Q_y$ applying the following
  rewrite rule: $Q_y \rightarrow Q_y {\displaystyle \AND_{i=1\ldots
      n}} {\sc lcs}\set{Q_{i_1},\ldots,Q_{i_m}}$ where $\overline{Z}_i
  = \set{z_{i_1},\ldots,z_{i_m}}$, and $Q_{i_j}@z_{i_j}\in \CTN$.

\item~({\em parameter introduction})
  New information is added to each node because of the presence of
  parameters, as the following rules show. The $\leadsto$ symbol is
  intended so that, each time the concept expression in the
  left hand side appears in some node of the temporal constraint
  network, possibly conjoined with other concepts, then the right hand
  side represents the concept expression that must be conjunctively
  added to all the other nodes; square brackets point out optional
  parts; the letters $f$ ($\star f$) and $g$ ($\star g$), possibly
  with subscripts, denote atomic (parametric) features while $p$ and
  $q$ stand for generic features.

{\footnotesize
\begin{lefteqnarray}
\star g_1 \CHAIN \ldots \CHAIN \star g_n 
  \left[\CHAIN\ f \left[\CHAIN\ p\right]\right]: C   & ~\leadsto~ &
    \star g_1 \CHAIN \ldots \CHAIN \star g_n: \top \per \\

\star g_1 \CHAIN \ldots \CHAIN \star g_n 
  \left[\CHAIN\ f \left[\CHAIN\ p\right]\right] \AGREE 
  g\left[\CHAIN\ q \right]                           & ~\leadsto~ &
    \star g_1 \CHAIN \ldots \CHAIN \star g_n: \top \per \\

\star g_1 \CHAIN \ldots \CHAIN \star g_n \AGREE
  \star f_1 \CHAIN \ldots \CHAIN \star f_m           & ~\leadsto~ &
      \star g_1 \CHAIN \ldots \CHAIN \star g_n \AGREE
      \star f_1 \CHAIN \ldots \CHAIN \star f_m \per \\

\star g_1 \CHAIN \ldots \CHAIN \star g_n
   \CHAIN\ g \left[\CHAIN\ p\right] \AGREE
   \star f_1 \CHAIN \ldots \CHAIN \star f_m 
   \left[\CHAIN\ f \left[\CHAIN\ q\right]\right]     & ~\leadsto~ & 
      \star g_1 \CHAIN \ldots \CHAIN \star g_n: \top \ \AND\ \\
      &  & \star f_1 \CHAIN \ldots \CHAIN \star f_m: \top \per 
\end{lefteqnarray}
}
\end{itemize}
}
\label{temp-comp}
\end{definition}
%%
\begin{proposition}[Equivalence of CEF]
  Every concept in existential form can be reduced into an equivalent
  completed existential concept. 
\end{proposition}
%%
Both the {\em covering} and the {\em parameter introduction} steps can
be computed independently after the {\em =-collapsing} step and then
conjoining the resulting concept expressions. Observe that, to obtain
a completed existential concept, the steps of the normalization
procedure require linear time with the exception of the computation of
the transitive closure of the temporal relations, and the covering
step. Both these steps involve NP-complete temporal constraint
problems~\cite{van:Beek:90}.  However, it is possible to devise
reasonable subsets of Allen's algebra for which the problem is
polynomial~\cite{nebel:renz:97}. The most relevant properties of a
concept in CEF is that all the admissible interval temporal relations
are explicit and the concept expression in each node is no more
refinable without changing the overall concept meaning; this is stated
by the following proposition.
%%
%%%%%%%%%%%%%%% NODE INDEPENDENCE OF CEF
%%
\begin{proposition}[Node independence of CEF]\label{node-independence}
  Let $\langle \overline{X}, \overline{\TC}, \overline{Q@X}\rangle $
  be a conceptual temporal con\-stra\-int network in its completed
  form (CEF); then, for all $Q\in\overline{Q}$ and for all \F\ concept
  expressions $C$ such that $C\not\SUBSUMES Q$, there exists an
  interpretation $\I$ such that $\Nint{\langle \overline{X},
    \overline{\TC}, \overline{(Q\AND C)@X}\rangle } \neq \langle
  \overline{X},$ $\overline{\TC},$ $\overline{Q@X}\Nint\rangle$, for
  some interval $t$.
\end{proposition}
%%
\begin{proof}
  The proposition states that the information in each node of the CEF
  is independent from the information in the other nodes. In fact,
  $\langle \overline{X},$ $\overline{\TC},$ $\overline{(Q\AND
    C)@X}\Nint{\rangle} = \Nint{\langle \overline{X}, \overline{\TC},
    \overline{Q@X}\rangle}$ if the concept expression in one node
  implies new information in some other node. Two cases can be
  distinguished.

  \noindent i) {\em Covered Nodes}. Both the {\em (=\ collapsing)}
  rule and the {\em (covering)} rule provide to restrict a covered
  node with the most specific \F\ concept expression. Indeed, the {\em
    (=\ collapsing)} rule provides collapsing two contemporary nodes
  conjoining the concept expressions of each of them. On the other
  hand, the {\em (covering)} rule adds to the covered node the most
  specific \F\ concept expression that subsumes the disjunctive
  concept expression that is implicitly true at the covered node.
  Note that, thanks to the {\em (Closure)} rule, all the possible
  equal temporal relations are made explicit. So these two
  normalization rules cover all the possible cases of temporal
  interactions between nodes.

  \noindent ii) {\em No coincident nodes}. Every time-invariant 
  information should spread over all the nodes. Both parametric
  features and the $\top$ concept have a time-invariant semantics: the
  only time-invariant concept expressions are $\top$, $\star g_1
  \CHAIN \ldots \CHAIN \star g_n:\top$, $\star g_1 \CHAIN \ldots
  \CHAIN \star g_n \AGREE \star f_1 \CHAIN \ldots \CHAIN \star f_m$,
  with $n,m\geq 1$, or an arbitrary conjunction of these terms.  The
  {\em (parameter introduction)} rule captures all the possible
  syntactical cases of completion concerning time-invariant concept
  expressions. By induction on the syntax, it can be proven that
  adding to a node any other concept expression changes the overall
  interpretation.
\end{proof}

%%%%%%%%%%%%%%% Essential Graph
The last normalization procedure eliminates nodes with redundant
information. This final normalization step ends up with the concept in the
{\em essential graph form}, that will be the {\em normal form} used for
checking concept subsumption.
%%
\begin{definition}[Essential graph]{
    The subgraph of the CEF of a conceptual temporal constraint
    network $T = \langle \overline{X}, \overline{\TC},
    \overline{Q@X}\rangle $ obtained by deleting the nodes labeled
    only with time-invariant concept expressions -- with the exception
    of the \NOW\ node -- is called {\em essential graph} of $T$:
    (${\sl ess}\ \!T$).}
\label{ess-graph}
\end{definition}
%%
\begin{proposition}[Equivalence of essential graph]
  Every concept in completed existential form can be reduced in linear
  time into an equivalent essential graph form.
\end{proposition}
%%
\begin{theorem}[Equivalence of normal form]
  Every concept expression can be reduced into an equivalent essential
  graph form. If a polynomial fragment of Allen's algebra is adopted,
  the reduction takes polynomial time.
\end{theorem}
%%
\noindent 
As an example, the normal form is shown -- i.e., the essential graph -- of
the previously introduced {\tt Stack} action (see Section~\ref{block}):

\vspazio\noindent$
{\tt Stack} ~\doteq~
  \SOMETIME 
  \parbox[t]{26em}{$
      (x\ y\ v\ w\ z)
                    \parbox[t]{24em}{$
                    (x\ {\sf fi}\ \NOW)(y\ {\sf mi}\ \NOW) 
                    (z\ {\sf mi}\ \NOW)(w\ {\sf f}\ \NOW)(v\ {\sf o}\ \NOW)
                    (y\ {\sf mi}\ x) 
                    (z\ {\sf mi}\ x) (w\ {\sf f}\ x)\\
                    (v\ {\sf (o,d,s)}\ x) (z\ {\sf (=,s,si)}\ y) 
                    (w\ {\sf m}\ y)
                    (v\ {\sf b}\ y) (w\ {\sf m}\ z) 
                    (v\ {\sf b}\ z) (w\ {\sf mi}\ v) \per 
                    $}\\
       \mbox{\large (}
       \parbox[t]{25em}{$
         ({\tt \Parm OBJECT2}: {\tt Clear\mbox{-}Block}\ \AND\ 
          {\tt \Parm OBJECT1}: \top)@x \AND \\
          ({\tt \Parm OBJECT1}\!\CHAIN\!{\tt ON}\AGREE{\tt \Parm OBJECT2})@y
          \AND  \\
         ({\tt \Parm OBJECT1}:{\tt Clear\mbox{-}Block}\ \AND\ 
          {\tt \Parm OBJECT2}: \top)@v \AND \\
         ({\tt \Parm OBJECT1}:{\tt Hold\mbox{-}Block}\ \AND\ 
          {\tt \Parm OBJECT2}: \top)@w \AND\\
         ({\tt \Parm OBJECT1}:{\tt Clear\mbox{-}Block}\ \AND\ 
          {\tt \Parm OBJECT2}: \top)@z
      \mbox{\large )}
      $}
  $}
$
\vspazio

\noindent 
In this example, the essential graph is also the CEF of {\tt Stack} since
there are no redundant nodes.

%%%%%%%%%%%%%%%%%%%%%%%%%%%% SUBSUMPTION %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{Computing Subsumption}\label{subs}

A concept subsumes another one just in case every possible instance of
the second is also an instance of the first, for every time interval.
Thanks to the normal form, concept subsumption in the temporal
language is reduced to concept subsumption between non-temporal
concepts and to subsumption between temporal constraint networks. A
similar general procedure was first presented
in~\cite{weida:litman:kr-92}, where the language for non-temporal
concepts is less expressive -- it does not include features or
parametric features.

%%%%%%%%%%%%%%

To compute subsumption between non-temporal concepts -- which may
possibly include {\sc lcs} concepts -- we refer
to~\cite{borgida:et:al:aaai-92}. In the following, we will write
``$\SUBSUMES_{\footnotesize\F}$'' for subsumption between non-temporal
\F\ concepts taking into account {\sc lcs} concepts.

%%%%%%%%%%%%%%
%%
\begin{definition}[Variable mapping]
  A {\em variable mapping} \VMap\ is a total function
  $\VMap:\overline{X}_1\mapsto\overline{X}_2$ such that
  $\VMap(\NOW)=\NOW$.  We write $\VMap(\overline{X})$ to intend
  $\set{\VMap(X)\mid X\in \overline{X}}$, and $\VMap(\overline{\TC})$
  to intend $\set{(\VMap(X)\ (R)\ \VMap(Y))\mid (X\ (R)\ Y) \in
    \overline{\TC}}$.
\end{definition}
%%
\begin{definition}[Temporal constraint subsumption]{
    A temporal constraint $(X_1 (R_1) Y_1)$ is said to {\em subsume} a
    temporal constraint $(X_2 (R_2) Y_2)$ under a generic variable
    mapping \VMap, written $(X_1 (R_1) Y_1)$ $\SUBSUMES_{\VMap}$
    $(X_2$ $(R_2)$ $Y_2)$, if $\VMap(X_1)=X_2$, $\VMap(Y_1)=Y_2$ and
    $\EPS{R_1}\supseteq\EPS{R_2}$ for every temporal interpretation
    \E.}\label{def-tc-subs}
\end{definition}
%%
\begin{proposition}[TC subsumption algorithm]\label{prop-tc-subs}
  $(X_1 (R_1) Y_1)\SUBSUMES_{\VMap}(X_2 (R_2) Y_2)$ if and only if
  $\VMap(X_1) = X_2$, $\VMap(Y_1)=Y_2$ and the disjuncts in $R_1$ are a
  superset of the disjuncts in $R_2$.
\end{proposition}
%%
\begin{proof}
  Follows from the observation that the 13 temporal relations are mutually
  disjoint and their union covers the whole interval pairs space.
\end{proof}
%%
\begin{definition}[Temporal constraint network subsumption]
  A temporal constraint network $\langle \overline{X}_1,$
  $\overline{\TC}_1\rangle$ subsumes a temporal constraint network $\langle
  \overline{X}_2,$ $\overline{\TC}_2\rangle $ under a variable mapping
  $\VMap:\overline{X}_1\mapsto\overline{X}_2$, written $\langle
  \overline{X}_1, \overline{\TC}_1\rangle \SUBSUMES_{\VMap} \langle
  \overline{X}_2,\overline{\TC}_2\rangle $, if $\Eps{\langle
    \VMap(\overline{X}_1), \VMap(\overline{\TC}_1)\rangle }$ $\supseteq
  \langle \overline{X}_2,$ $\overline{\TC}_2\Eps\rangle$ for every temporal
  interpretation \E\per
\end{definition}
%%
\begin{proposition}[TCN subsumption algorithm]\label{prop-tcn-subs}
  $\langle \overline{X}_1, \overline{\TC}_1\rangle \SUBSUMES_{\VMap}
  \langle \overline{X}_2, \overline{\TC}_2\rangle $ iff,
  after computing the temporal transitive closure, there exists a
  variable mapping $\VMap:\overline{X}_1\mapsto\overline{X}_2$ such
  that for all $X_{1_i},Y_{1_j}\in\overline{X}_1$ exist
  $X_{2_m},Y_{2_n}\in\overline{X}_2$ which satisfy $(X_{1_i}\ (R_{1_{i,j}})\ 
  Y_{1_j})\SUBSUMES_{\VMap} (X_{2_m}\ (R_{2_{m,n}})\ Y_{2_n})$.
\end{proposition}
%%
\begin{proof}
  ``$\Leftarrow"$ Since from definition~\ref{def-tc-subs} $(X_{1_i}\ 
  (R_{1_{i,j}})\ Y_{1_j})\SUBSUMES_{\VMap} (X_{2_m}\ (R_{2_{m,n}})\ Y_{2_n})$
  implies that $\EPS{R_{1_{i,j}}}\supseteq\EPS{R_{2_{m,n}}}$ for every
  $\E$, then, from the definition of interpretation of a temporal
  constraint network, it is easy to see that each assignment of
  variables $\V$ in the interpretation of $\langle
  \overline{X}_2,\overline{\TC}_2\rangle $ is also an assignment in
  the interpretation of $\langle
  \VMap(\overline{X}_1),\VMap(\overline{\TC}_1)\rangle $.
  \\
  ``$\Rightarrow"$ Suppose that one is not able to find such a
  mapping; then, by hypothesis, for each possible variable mapping
  there exists some $i,j$ such that $R_{1_{i,j}}$ is not a superset of
  $R_{2_{m,n}}$. Since, by assumption, the temporal constraint networks
  are minimal, the temporal relation $R_{2_{m,n}}$ cannot be further
  restricted. So, for each variable mapping and each temporal
  interpretation $\E$, we can build an assignment $\V^*$ such that
  $\langle\V^*(X_{2_m}),\V^*(X_{2_n})\rangle \in \EPS{R_{2_{m,n}}}$ while
  $\langle\V^*(X_{1_i}),\V^*(X_{1_j})\rangle \not\in \EPS{R_{1_{i,j}}}$.
  Now, we can extend the assignment $\V^*$ in such a way that
  $\V^*\in\EPS{\langle \overline{X}_2,\overline{\TC}_2\rangle }$ while
  $\V^*\not\in\EPS{\langle
    \VMap(\overline{X}_1),\VMap(\overline{\TC}_1)\rangle }$.  This
  contradicts the assumption that $\langle \overline{X}_1,
  \overline{\TC}_1\rangle$ $\SUBSUMES_{\VMap}$ $\langle
  \overline{X}_2, \overline{\TC}_2\rangle $.
\end{proof}
%%
\begin{definition}[S-mapping]
  An {\em s-mapping} from a conceptual temporal constraint network
  $\langle \overline{X}_1,\overline{\TC}_1,\overline{Q@X}_1\rangle$ to
  a conceptual temporal constraint network $\langle \overline{X}_2,
  \overline{\TC}_2, \overline{Q@X}_2\rangle $ is a variable mapping
  $\S:\overline{X}_1\mapsto\overline{X}_2$ such that the non-temporal
  concept labeling each node in $\overline{X}_1$ subsumes the
  non-temporal concept labeling the corresponding node in
  $\S(\overline{X}_1)$, and $\langle \overline{X}_1,
  \overline{\TC}_1\rangle \SUBSUMES_{\S} \langle \overline{X}_2,$
  $\overline{\TC}_2\rangle $.
\end{definition}
%%
The algorithm for checking subsumption between temporal concept
expressions reduces the subsumer and the subsumee in essential graph
form, then it looks for an s-mapping between the essential graphs by
exhaustive search.  To prove the completeness of the overall
subsumption procedure it will be showed that the introduction of {\sc
  lcs}'s preserves the subsumption. A model-theoretic characterization
of the {\sc lcs} will be given for showing this property. Let's start
to build an Herbrand model for an \F\ concept. Let $C'(x)$ denote the
first order formula corresponding to a concept $C$ (see
proposition~\ref{fol}), while the functionality of features can be
expressed with a set of formul\ae\ {\boldmath $F$}. By syntax
induction it easy to show that $C'(x)$ is an existentially quantified
formula with one free variable.  Moreover, the matrices of such
formula is a conjunction of positive predicates.  $\mbox{{\boldmath
    $F$}}\cup\{C'(x)\}$ is logically equivalent to $\mbox{{\boldmath
    $F$}} \cup\set{C''(x)}$ where the functionality axioms allow to
map every subformula $\bigwedge_y \exists y\per F_f(x,y)$ into
$\exists ! y\per F_f(x,y)$.  Then $C''(x)$ is such that all the
existential quantifiers in $C'(x)$ (which come from the first order
conversion of features) are replaced by $\exists !$ quantifiers.  Now,
$\mbox{{\boldmath $F$}}\cup\{C'''(a)\}$ -- where $a$ is a constant
substituting the free variable $x$ and $C'''(a)$ is obtained by
skolemizing the $\exists !$ quantified variables -- is a set of definite
Horn clauses.
%%
\begin{definition}[Herbrand model]\label{mhm}
  Let $C$ be an \F\ concept expression. Then we define its {\em
    Minimal Herbrand Model} ${\cal H_C}$ as the {\em Minimal Herbrand
    Model} of the above mentioned set of definite Horn clauses
  $\mbox{{\boldmath $F$}}\cup\{C'''(a)\}$.
\end{definition}
%%
\begin{lemma}[\F\ concept subsumption]\label{h-subs}
  Let $C,D$ be \F\ concept expressions, and ${\cal H_C},{\cal H_D}$
  their minimal Herbrand models obtained by skolemizing the first
  order set $\mbox{{\boldmath $F$}}\cup\set{C'''(a),D'''(a)}$. Then,
  $C\SUBSUMEDBY D$ iff ${\cal H_D}\subseteq{\cal H_C}$.
\end{lemma}
%%
\begin{proof}
  $C\SUBSUMEDBY D$ iff $\mbox{{\boldmath $F$}}\cup\{C'(x)\}\models
  D'(x)$, iff $\mbox{{\boldmath $F$}}\cup\{C''(x)\}\models D''(x)$,
  where $C''$ and $D''$ are obtained by applying the functionality
  axioms to the set $\set{C'(x),D'(x)}$ (i.e., unifying the
  variables in the functional predicates) and then replacing all the
  existential quantifiers by $\exists !$ quantifiers. Now, $C'''(x)$
  and $D'''(x)$ are obtained by skolemizing the $\exists !$ quantified
  variables in the following way: let $C''(x) = \exists !
  y_1,\ldots,y_n\phi(x,y_1,\ldots,y_n)$ and let $D''(x) = \exists !
  y_1,\ldots,y_k,z_1,\ldots,z_m\psi(x,y_1,\ldots,y_k,z_1,\ldots,z_m)$,
  with $0\leq k \leq n$, then skolemize the formula: $\sigma =
  \exists ! y_1,\ldots,y_n,z_1,\ldots,z_m \phi(x,y_1,\ldots,y_n)
  \wedge \psi(x,y_1,\ldots,y_k,z_1,\ldots,z_m)$, and let $\sigma^0(x)$
  indicate its skolemized form.  Then, $C'''(x) = \phi^0(x)$ and
  $D'''(x) = \psi^0(x)$. Now, since every existential quantification
  in $C''(x),D''(x)$ was of type $\forall\exists !$ then the thesis is
  true iff $\mbox{{\boldmath $F$}}\cup\{C'''(a)\}\models D'''(a)$,
  where $a$ is a constant substituting the free variable $x$
  (see~\cite{dalen:94}).  Now, as showed by lemma~\ref{mhm}, both
  $C'''(a)$ and $D'''(a)$ have minimal Herbrand models ${\cal
    H_C},{\cal H_D}$ that verify the lemma hypothesis. Then,
  $\mbox{{\boldmath $F$}}\cup\{C'''(a)\}\models D'''(a)$ iff ${\cal
    H_D}\subseteq{\cal H_C}$.
\end{proof}

We are now able to give a model-theoretic characterization of the {\sc
  lcs} that will be crucial to prove the subsumption-preserving property.
%% 
\begin{lemma}[{\sc lcs} model property]\label{lcs}{
    Let $Q_1,\ldots,Q_n$ be \F\ concept expressions, and ${\cal
      H}_{Q_1},$ $\ldots, {\cal H}_{Q_n}$ their minimal Herbrand models
    obtained by skolemizing the first order set $\mbox{{\boldmath
        $F$}}\cup\set{Q_1'''(a),\ldots,Q_n'''(a)}$.  Then, $Q = {\sc
      lcs}\set{Q_1,\ldots,Q_n}$ iff ${\cal H_{Q}}= {\cal H}_{Q_1} \cap
    \dots \cap {\cal H}_{Q_n}$.  }
\end{lemma}
%%
\begin{proof}
  First of all, let show that ${\cal H_{Q}}$ is the minimal Herbrand
    model of a concept $Q$ in the language \F. Every ${\cal H}_{Q_i}$
    can be seen as a rooted directed acyclic graph where nodes are
    labelled with (possible empty) set of atomic concepts and arcs
    with atomic features while equality constraints between nodes
    correspond to features agreement. Whithout loss of generality let
    us consider the case where ${\cal H_{Q}}= {\cal H}_{Q_1} \cap
    {\cal H}_{Q_2}$.  It is sufficient to show that ${\cal H_{Q}}$ is a
    rooted directed acyclic graph. Let $a$ be the root of ${\cal
      H}_{Q_1},{\cal H}_{Q_2}$, then will be proved by induction that
    if $F_i(a_{i-1},a_i) \in {\cal H_{Q}}$ (where $F_i$ is the first
    order translation of a feature, $a_{i-1},a_i$ are obtained as a
    result of the skolemization process, and $a_0 = a$) then
    $\set{F_1(a,a_1),\ldots,F_i(a_{i-1},a_i)} \subseteq {\cal H_{Q}}$.
    The case $i=1$ is trivial. Let $i>1$. Now, $F_i(a_{i-1},a_i) \in
    {\cal H_{Q}}$ iff $F_i(a_{i-1},a_i) \in {\cal H}_{Q_1}\cap{\cal
      H}_{Q_2}$. But $a_{i-1}$ is uniquely defined by the skolem
    function $f_{F_{i-1}}$ (where, the function symbols $f_{F_i}$ are
    newly generated for each feature $F_i$ by the skolemization
    process). Then, $F_i(a_{i-1},a_i) \in {\cal H}_{Q_1}\cap{\cal
      H}_{Q_2}$ iff $F_i(a_{i-1},f_{F_{i-1}}(a_i)) \in {\cal
      H}_{Q_1}\cap{\cal H}_{Q_2}$ iff
    $F_{i-1}(a_{i-2},f_{F_{i-1}}(a_i)) \in {\cal H}_{Q_1}\cap{\cal
      H}_{Q_2}$. Then the thesis is true by induction.
    
    Let us now prove the ``$\Leftarrow$'' direction.  Suppose by
    absurd that there is an \F\ concept $C$ such that:
    ${Q_1}\SUBSUMEDBY C ~\wedge~ {Q_2}\SUBSUMEDBY C ~\wedge~
    C\SUBSUMED Q$.  Then, ${Q_1} \SUBSUMEDBY C$ iff ${\cal
      H_C}\subseteq {\cal H}_{Q_1}$, and ${Q_2} \SUBSUMEDBY C$, iff
    ${\cal H_C}\subseteq {\cal H}_{Q_2}$.  But then ${\cal
      H_C}\subseteq {\cal H}_{Q_1}\cap {\cal H}_{Q_2}$, i.e., ${\cal
      H_C} \subseteq {\cal H_Q}$.  Then $Q \SUBSUMEDBY C$ which
    contradicts the hypothesis.
  
  The ``$\Rightarrow$'' direction can be proved with analogous
  considerations.
\end{proof}
%%
\begin{proposition}[{\sc lcs} subsumption-preserving property]\label{lcs-inv}
  Let $A,B,C,D$ be \F\ concepts, then $A \AND (B \OR C) \SUBSUMEDBY D$
  iff $A \AND {\sc lcs}\set{B,C} \SUBSUMEDBY D$.
\end{proposition}
%%
\begin{proof}
  $A \AND (B \OR C) \SUBSUMEDBY D$ iff $A \AND B \SUBSUMEDBY D$ and $A
  \AND C \SUBSUMEDBY D$. Now, $A \AND B \SUBSUMEDBY D$ iff
  $\mbox{{\boldmath $F$}}\cup\{A'''(a),B'''(a)\}\models D'''(a)$ iff
  ${\cal H_A}\cup{\cal H_B}\models D'''(a)$ iff ${\cal H_D}\subseteq
  {\cal H_A}\cup{\cal H_B}$. For the same reasons, $A\AND C
  \SUBSUMEDBY D$ iff ${\cal H_D}\subseteq {\cal H_A}\cup{\cal H_C}$.
  But then, ${\cal H_D}\subseteq{\cal H_A}\cup{\cal H_B}$ and ${\cal
    H_D}\subseteq {\cal H_A}\cup{\cal H_C}$, i.e., ${\cal
    H_D}\subseteq{\cal H_A}\cup({\cal H_B}\cap{\cal H_C})$, i.e.,
  ${\cal H_D}\subseteq{\cal H_A}\cup {\cal H}_{{\sc lcs}\{B,C\}}$.
  But, ${\cal H_D}\subseteq{\cal H_A}\cup {\cal H}_{{\sc lcs}\{B,C\}}$
  iff $A \AND {\sc lcs}\set{B,C}\SUBSUMEDBY D$.
\end{proof}

%%%%%%%%%%%%%%%%%%% Theorem 1
The following theorem provides a sound and complete procedure to
compute subsumption. The completeness proof takes into account
that the temporal structure is dense and unbounded. This allows us to
introduce any new node to a conceptual temporal constraint network
without changing its meaning. Remember that, for each of these
redundant nodes, time-invariant information holds.
%%
\begin{theorem}[\TLF\ concept subsumption]\label{subsumption-theorem}
  A concept $C_1$ subsumes a concept $C_2$ iff there exists an
  s-mapping from the essential graph of $C_1$ to the essential graph of
  $C_2$.
\end{theorem}
%%
\begin{proof}
  \noindent Let $T_1$ $= \langle \overline{X}_1,
  \overline{\TC}_1,\overline{Q@X}_1\rangle $ be the essential graph of
  $C_1$, and $T_2 = \langle \overline{X}_2, \overline{\TC}_2,$
  $\overline{Q@X}_2\rangle $ be the essential graph of $C_2$.

  \noindent ``$\Leftarrow"$ (Soundness). Follows from the fact that the 
  essential graph form is logically equivalent to the starting concept,
  and from the soundness of the procedures for computing both the TCN
  subsumption (proposition~\ref{prop-tcn-subs}) and the subsumption
  between non-temporal concepts~\cite{borgida:et:al:aaai-92}.

  \noindent ``$\Rightarrow"$ (Completeness). Suppose that such an 
  s-mapping does not exist.  Two main cases can be distinguished.
  
  i) There is not a mapping \VMap\ such that $\langle
  \overline{X}_1,\overline{\TC}_1\rangle \SUBSUMES_{\VMap} \langle
  \overline{X}_2,\overline{\TC}_2\rangle $.  By adding redundant nodes
  to $T_2$, an equivalent conceptual temporal constraint network
  $T_2^* = \langle \overline{X}_2^*, \overline{\TC}_2^*,
  \overline{Q@X}_2^*\rangle$ may be obtained. Let us consider such an
  extended network in a way that there exists a variable mapping
  $\VMap^*$ such that $\langle\overline{X}_1,\overline{\TC}_1\rangle
  \SUBSUMES_{\VMap^*} \langle
  \overline{X}_2^*,\overline{\TC}_2^*\rangle $.  Now, for all possible
  $\VMap^*$, there is a node $X_{1_i}\in \overline{X}_1$ such that
  $\VMap^*(X_{1_i}) = X_{2_j}$ with $X_{2_j}\not\in \overline{X}_2$.
  Now, $Q_{1_i}\not\SUBSUMES_{\footnotesize\F} Q_{2_j}$, since $X_{2_j}$
  cannot coincide with other nodes in $\overline{X}_2$ neither can
  have a covering otherwise the hypothesis that the mapping \VMap\ 
  does not exist would be contradicted. Then from
  proposition~\ref{node-independence} $Q_{2_j}$ is in a time-invariant
  node, whereas $Q_{1_i}$ is not since $T_1$ is an essential graph.
  Then, although the construction of $\VMap^*$ allows for the
  existence of a unique $\V$\footnote{Since subsumption is computed
    with respect to a fixed evaluation time, $\V$ maps the different
    occurrences of \NOW\ to the same interval; this justifies the
    choice that $\VMap(\NOW)=\NOW$.} for both networks (follows from
  proposition~\ref{prop-tcn-subs}), it is possible to build an
  instance of $T_2$ that is not an instance of $T_1$.
  
  ii) For each possible mapping \VMap\ such that $\langle
  \overline{X}_1,$ $\overline{\TC}_1\rangle \SUBSUMES_{\VMap} \langle
  \overline{X}_2,\overline{\TC}_2\rangle $ there will be always two
  nodes $X_{1_i}$ and $X_{2_j}$ such that $\VMap(X_{1_i})=X_{2_j}$ and
  $Q_{1_i}\not\SUBSUMES_{\footnotesize\F} Q_{2_j}$. Now, the concept
  expression $Q_{2_j}$ cannot be refined (looking for a subsumption
  relationship with $Q_{1_i}$) by adding to it an \F\ concept since
  from proposition~\ref{node-independence} this would change the
  overall interpretation. On the other hand, the {\sc lcs}
  introduction -- which would substitute the more specific concept
  disjunction implicitly presents because of a node covering -- is a
  subsumption-invariant concept substitution, as showed by
  lemma~\ref{lcs-inv}.

  Both cases contradict the assumption that $T_1$ subsumes $T_2$.
\end{proof}

%%%%%%%%%%%%%%%%%%% NP-COMPLETENESS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsubsection{Complexity of Subsumption}

Now it is shown that checking subsumption between \TLF\ concept
expressions in the essential graph form is an NP-complete problem.
Therefore, a polynomial reduction from the NP-complete problem of
deciding whether a graph contains an isomorphic subgraph is presented.
It is then shown that the subsumption computation, as proposed in
theorem~\ref{subsumption-theorem}, can be done by a non-deterministic
algorithm that takes polynomial time in the size of the concepts
involved. First of all let us consider the complexity of computing
subsumption between non-temporal concepts.
%%
\begin{lemma}[\F\ subsumpion complexity]
  Let $C,D$ be \F\ concept expressions that can contain {\sc lcs}'s.
  Then, checking whether $C\SUBSUMEDBY_{\footnotesize\F}D$ takes
  polynomial time.
\end{lemma}
%%
\begin{proof}
  See~\cite{borgida:et:al:aaai-92}.
\end{proof}

Here the problem of {\em subgraph isomorphism} is briefly recalled.
Given two graphs, $G_1 =(V_1,E_1)$ and $G_2 =(V_2,E_2)$, $G_1$
contains a subgraph isomorphic to $G_2$ if there exists a subset of
the vertices $V' \subseteq V_1$ and a subset of the edges $E'
\subseteq E_1$ such that $\mid\!V'\!\mid = \mid\!V_2\!\mid$,
$\mid\!E'\!\mid = \mid\!E_2\!\mid$, and there exists a one-to-one
function $f:V_2 \mapsto V'$ satisfying $\{u,v\} \in E_2$ iff
$\{f(u),f(v)\} \in E'$.

\noindent Given a graph $G = (V,E)$, with $V = \{v_1,\ldots,v_n\}$
associate a temporal concept expression: $C \doteq
\SST{(v_1,\ldots,v_n)}{\ldots (v_i~({\sf b,a})~v_j) \ldots} {(A@v_1
  \AND \ldots\AND A@v_n)}$, where $A$ is an atomic concept and
$\{v_i,v_j\}\in E$.  This transformation allows us to prove that the
problem of subgraph isomorphism can be reduced to the subsumption of
temporal concepts.
%%
\begin{proposition}\label{prop-np-hard}
  Given two graphs $G_1$ and $G_2$, $G_1$ contains a subgraph
  isomorphic to $G_2$ iff $C_2 \SUBSUMES C_1$, where $C_1$ and $C_2$
  are the corresponding temporal concepts expressions.
\end{proposition}
%%
\begin{proof}
  A temporal network with edges labeled only with the $({\sf before}
  \vee {\sf after})$ relation is always consistent, minimal and
  non-directed\footnote{If $(v_i~({\sf b,a})~v_j)$ then $(v_j~({\sf
      b,a})~v_i)$, too.}~\cite{gerevini:schubert:ai-94}.  Then, each
  temporal concept is in the essential graph form. Now the proof
  easily follows since, every time $G_2$ is an isomorphic subgraph of
  $G_1$ the one-to-one function $f$ is also an s-mapping from $C_2$ to
  $C_1$, and it is true that $C_2 \SUBSUMES C_1$. On the other hand,
  the s-mapping that gives rise to the subsumption is also the
  one-to-one isomorphism from $G_2$ to $G_1$.
\end{proof}
%%
\begin{theorem}[NP-hardness]\label{th-np-hard}
  Concept subsumption between \TLF\ concept expressions in normal form
  is an NP-hard problem.
\end{theorem}
%%
\begin{proof}
  Follows from proposition~\ref{prop-np-hard} and the reduction being
  clearly polynomial.
\end{proof}

Now the NP-completeness is proven.
%%
\begin{theorem}[NP-completeness]\label{th-np-completeness}
  Concept subsumption between \TLF\ concept expressions in normal form
  is an NP-complete problem.
\end{theorem}
%%
\begin{proof}
  To prove NP-completeness it is necessary to show that the proposed
  calculus can be solved by a nondeterministic algorithm that takes
  polynomial time.  Now, given two temporal concepts, $T_1$ and $T_2$,
  in their essential graph form, let $\mid\!  \overline{X}_1\!  \mid =
  N_1$ and $\mid\!  \overline{X}_2\!  \mid = N_2$.  Then, to check
  whether $T_1 \SUBSUMES T_2$, the algorithm guesses one of the
  $N_2^{N_1}$ variable mapping from $T_1$ to $T_2$ and verifies
  whether it is an s-mapping, too.  This last step can be done in
  deterministic polynomial time since, given a mapping $\VMap$, it is
  possible to determine whether $\langle \overline{X}_1,
  \overline{\TC}_1\rangle \SUBSUMES_{\VMap} \langle
  \overline{X}_2,\overline{\TC}_2\rangle$ by checking at most
  $N_1(N_1-1)/2$ edges looking for subsumption between the
  corresponding temporal relations (solved by a set inclusion
  procedure); while the $N_1$ non-temporal concept subsumptions can be
  computed in polynomial time.
\end{proof}

%%%%%%%%%%%%%%%%%%%%%%%%%%% Extending %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Extending the Propositional Part of the Language}

The propositional part of the temporal language can be extended to
have a more powerful, but still decidable, Description Logic.  It is
possible either to add full disjunction, both at the temporal and
non-temporal levels (\TLUFU), or to have a propositionally complete
language at the non-temporal level only (\TLALCF).

Please note that in these languages it is not possible to express full
negation, and in particular the negation of the existential temporal
quantifier.  This is crucial, and it makes the difference with other
logic-based
approaches~\cite{schmiedel:90,bettini:dke-97,halpern:shoham:91}.  The
dual of $\SOMETIME$ (i.e., the universal temporal quantifier
$\ALLTIME$) makes the satisfiability problem -- and the subsumption --
for propositionally complete languages undecidable in the most
interesting temporal
structures~\cite{halpern:shoham:91,venema:90,bettini:tesi-93}. For the
representation of actions and plans in the context of plan
recognition, the universal temporal quantifier is not strictly
necessary.  This limitation makes these languages decidable, with nice
computational properties, and capable of supporting other kinds of
useful extensions. The examples shown throughout the paper may serve
as a partial validation of the claim. Section~\ref{homo} proposes the
introduction of a limited universal temporal quantification that
maintains decidability of subsumption.

%%%%%%%%%%%%%%%%%%%%%%%%%%% Disjunction %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Disjunctive Concepts: \TLUFU}
\label{disjunction-section}

The language \TLUFU\ adds to the basic language \TLF\ the disjunction
operator -- with the usual semantics -- both at the temporal and
non-temporal levels:

\begin{Eqnarraycomm}
C, D & \rightarrow & \TL \mid C\OR D      & (\TLU) \\
E, F & \rightarrow & \F \mid \NC\OR \ND   & (\FU)
\end{Eqnarraycomm}

\noindent 
Before showing how to modify the calculus to check subsumption, let us
begin with a clarifying example.  The gain in expressivity allows us
to describe the alternative realizations that a given plan may have.
Let us consider a scenario with a robot moving in an empty room that
can move only either horizontally or vertically.  Let's call {\tt
  Rect-Move} that which involves a simple sequence of the two basic
moving actions. Then, to describe a {\tt Rect-Move} plan we can make
use of the disjunction operator:

\vspazio
\noindent
${\tt Rect\mbox{-}Move}~~ \doteq ~~ 
   \parbox[t]{28em}{$ 
      \SST {(x\ y)} {(\NOW\ {\sf m}\ x)(x\ {\sf m}\ y)}
        \mbox{\large(}
         {\tt Hor\mbox{-}Move}@x\ \AND\ {\tt Ver\mbox{-}Move}@y 
         \mbox{\large)}\ \OR \\
      \SST {(x\ y)} {(\NOW\ {\sf m}\ x)(x\ {\sf m}\ y)}
        \mbox{\large(}
         {\tt Ver\mbox{-}Move}@x\ \AND\ {\tt Hor\mbox{-}Move}@y 
         \mbox{\large)}
$}
$

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsubsection{The Calculus for \TLUFU}

%%%%%%%%
\begin{figure}
{\footnotesize 
\begin{center}
\begin{lefteqnarrayfig}
(C\OR D)@X & \rightarrow & C@X\OR D@X
\\ 
p:(C\OR D) & \rightarrow & p:C\OR p:D 
\\
(C_1\OR C_2)\AND D & \rightarrow & (C_1\AND D)\OR(C_2\AND D) 
\\ 
\SST {(\overline{X})}{\overline{\TC}}{(C\OR D)}  & \rightarrow & 
  \SST {(\overline{X})}{\overline{\TC}}{C}\OR
  \SST {(\overline{X})}{\overline{\TC}}{D}

\end{lefteqnarrayfig}
\end{center}
\ \hrulefill
}
\caption[normal-form]{\label{normal-form2}
Rewrite rules for computing the disjunctive form.}
\end{figure}
%%%%%%%%%
\subsubsection*{Normal Form}

In computing subsumption, a normal form for concepts is needed.  The
normalization procedure is similar to that reported in
Section~\ref{normal-concept}. Let us start by reducing each concept
expression into an equivalent {\em disjunctive concept} of the form:

\begin{leftarray}
\mbox{\large(}\SST {(\overline{X}_1)}{\overline{\TC}_1}{G_1}\mbox{\large)} \OR 
   \cdots \OR
\mbox{\large(}\SST {(\overline{X}_n)}{\overline{\TC}_n}{G_n}\mbox{\large)}\ 
   \OR  Q_{1} \OR \cdots \OR Q_{m}
\end{leftarray}

\noindent where $G_i$ are conjunctions of concepts of the form 
$Q_{i_k}@X_{i_k}$, and each $Q$ does not contain neither temporal
information, nor disjunctions, i.e., it is an element of the language
\F.
%%
\begin{proposition}[Equivalence of disjunctive form]
  { Every concept $C$ can be reduced into an equivalent
    disjunctive form $({\sl df}\ \!C)$, by exhaustively applying the
    set of rewrite rules of Figure~\ref{normal-form2} in addition to
    the rules introduced in Figure~\ref{normal-form}. }
\end{proposition}
%%
It is now possible to compute the {\em completed disjunctive normal
  form} (${\sl cdnf\ }C$). Each disjunct of such normal form has some
interesting properties, which are crucial for the proof of the
theorem~\ref{disj-subs} on concept subsumption: temporal constraints
are always explicit, i.e., any two intervals are related by a basic
temporal relation; there is no disjunction, either implicit or
explicit, neither in the conceptual part nor in the temporal part,
i.e., it is a \TLF\ concept; the information in each node is
independent of the information in the other nodes and it does not
contain time-invariant (i.e., redundant) nodes.
%%
\begin{definition}[Completed disjunctive normal form]
  Given a concept in {\em disjunctive form}, the {\em completed
    disjunctive normal form} is obtained by applying the following
  rewrite rules to each disjunct:
%%
\begin{itemize}
\item~({\em Temporal completion}) The rules of
  definition~\ref{temp-comp} are applied to each disjunct with the
  exclusion of the {\em covering} step, which is replaced by the {\em
    $\OR\mbox{-introduction}$} step. If a disjunct is unsatisfiable --
  i.e., the temporal constraint network associated with it is
  inconsistent -- then eliminate it.
  
\item~({\em Essential form}) The rules of definition~\ref{ess-graph}
  are applied to each disjunct.
  
\item~({\em $\OR$ introduction}) Reduce to concepts containing only
  basic temporal relationships:

$
\SOMETIME (\overline{X})\left(X_1\ (R\mbox{\large \bf ,}S)\ X_2\right)
  \overline{\TC} \per C  ~~ \rightarrow ~~
  \SOMETIME (\overline{X})(X_1\ R\ X_2)
     \overline{\TC} \per C\ \OR\ 
  \SOMETIME (\overline{X})(X_1\ S\ X_2)
     \overline{\TC} \per C
$
\end{itemize}
\end{definition}
%%%%%%%%%
\begin{proposition}[Equivalence of CDNF]
  Every concept expression can be reduced into an equivalent completed
  disjunctive normal concept.
\end{proposition}

%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsubsection*{Subsumption}

The theorem~\ref{disj-subs} reduces subsumption between CDNF concepts
into subsumption of disjun\-ction-free concepts, such that the results
of theorem~\ref{subsumption-theorem} can be applied.  The following
theorem gives a terminating, sound, and complete subsumption calculus
for \TLUFU.
%%
\begin{theorem}[\TLUFU\ concept subsumption] Let $C=C_1$ 
  $\OR$ $\cdots\OR C_m$ and $D=D_1\OR\cdots\OR D_n$ be \TLUFU\ 
  concepts in \mbox{CDNF}.  Then, $C\SUBSUMEDBY D$ if and only if~
  $\forall i \exists j\per\ C_i\SUBSUMEDBY D_j$.
\label{disj-subs}
\end{theorem}
%%
\begin{proof} Since it is easy to show that
  $ C_1 \OR \ldots \OR C_n \SUBSUMEDBY D ~\mbox{iff}~ \forall i \per
  C_i \SUBSUMEDBY D $ we need only to prove the restricted thesis: $
  C_i \SUBSUMEDBY D_1\OR\cdots\OR D_n ~ \mbox{iff}~ C_i \SUBSUMEDBY
  D_1\vee\ldots\vee C_i \SUBSUMEDBY D_n$. Every concept expression in
  CDNF corresponds to an existential quantified formula with two free
  variables. Moreover, the matrices of such formul\ae\ are
  conjunctions of positive predicates. Let us denote the formula
  corresponding to a concept $C$ as $C'(t,x)$. Now, the restricted
  thesis holds iff it is true that $F \cup\{C_i'''(a,b)\} \models
  D_1'''(a,b) \vee D_2'''(a,b)$. Now, let ${\cal H_B}$ the minimal
  Herbrand model of $F \cup \{C_i'''(a,b)\}$. Then, $F \cup
  \{C_i'''(a,b)\} \models D_1'''(a,b)\vee D_2'''(a,b) ~\mbox{iff}~
  {\cal H_B} \models D_1'''(a,b) \vee D_2'''(a,b)$.  Since we are
  talking of a single model, $D_1'''(a,b) \vee D_2'''(a,b)$ is valid
  in ${\cal H_B}$ if and only if either $D_1'''(a,b)$ or $D_2'''(a,b)$
  is valid in ${\cal H_B}$. This proves the theorem.\footnote{The
    proof of this theorem comes from an idea of Werner Nutt.}
\end{proof}

As a consequence of the
theorems~\ref{th-np-completeness},~\ref{disj-subs} the following
complexity result holds.
%%
\begin{theorem}[\TLUFU\ subsumption complexity]
  Concept subsumption between \TLUFU\ concept expressions in normal
  form is an NP-complete problem.
\end{theorem}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% ALCF  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{A Propositionally Complete Language:  \TLALCF}
\label{Temporal:alcf}

\TLALCF\ uses the propositionally complete Description Logic ${\cal
  ALCF}$~\cite{hollunder:nutt:dfki-90} for non-temporal concepts by
changing the syntax rules for \TLF\ in the following way:

\vspazio
$
E, F  \rightarrow  \FU \mid \bot \mid \NOT E 
                       \mid p \DISAGREE q  \mid \Undef p
                       \mid \ALL{P}{E} \mid \SOME{P}{E}  
                   ~~~\mbox{(\ALCF)}
$

\vspazio
\noindent The interpretation functions are extended to take into account 
roles: 

%%\vspazio
\begin{lefteqnarrayfig}
\Int P & \subseteq &\IS\times\Dom\times\Dom\\
\Nint{P}             & = & \hat{P}_t \subseteq\Dom\times\Dom \mid \ 
                            \forall a,b\per\ 
                              \langle a,b\rangle \in\hat{P}_t
                              \leftrightarrow 
                              \langle t,a,b\rangle \in \Int P
\end{lefteqnarrayfig}

%%\vspazio 
\noindent
As seen in Section~\ref{basic-dl}, \ALCF\ adds to \F\ full negation --
thus introducing disagreement ($p \DISAGREE q$) and undefinedness
($\Undef p$) for features, and role quantification ($\ALL{P}{E},
\SOME{P}{E}$).

As an example of the expressive power gained, let us refine the
description of the world states involved in the {\tt Stack} action
(see Section~\ref{block}). Suppose that a block is described by saying
that it has {\tt LATERAL-SIDE}s (role) and {\tt BOTTOM-} and {\tt
  TOP-SIDE}s (features). Then, the property of being clear could be
represented as follows:

\vspazio
\noindent
$
{\tt Clear\mbox{-}Block} ~\doteq~
     {\tt Block} \AND \ALL {\tt LATERAL\mbox{-}SIDE}{\tt Clear} \AND
     {\tt TOP\mbox{-}SIDE}:{\tt HAS\mbox{-}ABOVE} \DISAGREE
$
\vspazio

\noindent which says that, in order to be clear, each {\tt LATERAL-SIDE} 
has to be clear and nothing has to be over the {\tt TOP-SIDE}. Now,
the situation in which a block involved in a {\tt Stack} action is on
top of another one is reformulated with the following concept
expression:

\vspazio
\noindent
$
({\tt \Parm OBJECT1}\!\CHAIN\!{\tt TOP\mbox{-}SIDE}\!\CHAIN\!
{\tt HAS\mbox{-}ABOVE}\AGREE{\tt \Parm OBJECT2})
$
\vspazio

\noindent Furthermore, given the above definition of 
{\tt Clear\mbox{-}Block}s, it can be derived that:

\vspazio
\noindent
$
({\tt \Parm OBJECT1}\!\CHAIN\!{\tt TOP\mbox{-}SIDE}\!\CHAIN\!
{\tt HAS\mbox{-}ABOVE}\AGREE{\tt \Parm OBJECT2})
\SUBSUMEDBY
({\tt \Parm OBJECT1}: \NOT {\tt Clear\mbox{-}Block})
$
\vspazio

\noindent i.e., an object, having another object on top of it, 
is no more a clear object.

In \TLALCF\ it is possible to describe states with some form of
incomplete knowledge by exploiting the disjunction among non-temporal
concepts. For example, let us say that the agent of an action can be
either a human being or a machine: $\star {\tt AGENT}.({\tt Person}
\OR {\tt Robot})$.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsubsection{The Calculus for \TLALCF}

This Section presents a calculus for deciding subsumption between
temporal concepts in the Description Logic \TLALCF. Again, the
calculus is based on the idea of separating the inference on the
temporal part from the inference on the Description Logic part
(``$\SUBSUMEDBY_{\footnotesize\ALCF}$''), and adopting standard
procedures developed in the two areas.

\subsubsection*{Normal Form}

%%%%%%%%%%%%%%%%%%%%%%%%% Normal Form for TL-ALCF %%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{figure}
{\footnotesize 
\begin{center}
\begin{lefteqnarrayfig}
  \NOT \top         & \rightarrow & \bot \\
  \NOT \bot         & \rightarrow & \top \\
  \NOT (C \AND D)   & \rightarrow & \NOT C \OR \NOT D \\
  \NOT (C \OR D)    & \rightarrow & \NOT C \AND \NOT D \\
  \NOT\ \NOT C       & \rightarrow & C \\
  \NOT \ALL{P}{C}   & \rightarrow & \SOME{P}{\NOT C} \\
  \NOT \SOME{P}{C}  & \rightarrow & \ALL{P}{\NOT C} \\
  \NOT f:C          & \rightarrow & f\DISAGREE \OR\ f:\NOT C \\
  \NOT p:C          & \rightarrow & f\DISAGREE \OR\ f:(\NOT q:C)~~~~
                                   \mbox{if $p = f\CHAIN q$} \\
  \NOT p\AGREE q    & \rightarrow & p\DISAGREE \OR\ q\DISAGREE \OR\ 
                                   p\DISAGREE q \\
  \NOT p\DISAGREE q & \rightarrow & p\DISAGREE \OR\ q\DISAGREE \OR\ 
                                   p\AGREE q \\
  (f\CHAIN p)\DISAGREE     & \rightarrow & f\DISAGREE \OR\ f:(p\DISAGREE)
  
\end{lefteqnarrayfig}
\end{center}

{\em Note: }By $f$ we denote both an atomic feature and an atomic
parametric feature.

\hrulefill
}
\caption[normal-form]{\label{simple-form}
  Rewrite rules to transform an arbitrary concept into a simple concept.}
\end{figure}

Once more, the subsumption calculus is based on a normalization
procedure.  The first step reduces a concept expression into an
equivalent {\it existential form} -- $\SST
{(\overline{X})}{\overline{\TC}}{(Q_0 \AND Q_1@X_1 \AND \ldots \AND
  Q_n@X_n)}$ -- by applying the rewrite rules of
Figure~\ref{normal-form} augmented with the rule: $ p:(q_1 \DISAGREE
q_2) \rightarrow p \CHAIN q_1 \DISAGREE p \CHAIN q_2 $. Each $Q$ is a
non-temporal concept, i.e., it is an element of the language \ALCF.

In the following normalization step there will be a need to verify
concept satisfiability for non-temporal concept expressions. An \ALCF\ 
concept $E$ is unsatisfiable iff
$E\SUBSUMEDBY_{\footnotesize\ALCF}\bot$. Algorithms for checking
satisfiability and subsumption of concepts terms in \ALCF\ are
well known~\cite{hollunder:nutt:dfki-90}.
%%
\begin{definition}[Completed existential form]
  { The {\em temporal completion} of a concept in existential form --
    the {\em Completed Existential Form}, CEF -- is obtained by
    sequentially applying the following steps:
%%
\begin{itemize}
\item~({\em closure, collapsing, covering}) As reported in
  definition~\ref{temp-comp}. As for the {\em covering},
  translate the concept expression $Q_y$ applying the rewrite rule:
  $Q_y \rightarrow Q_y {\displaystyle \AND_{i=1\ldots n}}
  (Q_{i_1}\OR\ldots\OR Q_{i_m})$.

\item~({\em parameter introduction}) This requires two phases.
%%
\begin{enumerate}
  
\item Each $Q$ is translated in {\em disjunctive normal form}.  First
  the {\it simple form}\footnote{A {\em simple concept} contains only
    complements of the form $\NOT A$, where $A$ is a primitive
    concept, and no sub-concepts of the form $p\!\DISAGREE$, where $p$
    is not an atomic (parametric) feature -- this corresponds to a
    first order logical formula in negation normal form.} is obtained
  by transforming each $Q$ following the rewrite rules reported in
  Figure~\ref{simple-form}. The {\em disjunctive normal form} is then
  obtained by rewriting each $Q$ -- which is now in simple form --
  using the following rules, which correspond to the first order rules
  for computing the disjunctive normal form of logical formul\ae:

\begin{lefteqnarray}
  (C_1 \OR C_2) \AND D  & \rightarrow & (C_1 \AND D) \OR (C_2 \AND D) \\
  p:(C\OR D) & \rightarrow & p:C\OR p:D
\end{lefteqnarray} 
  
\item For each $Q_j = E_{j_1} \OR \ldots \OR E_{j_n}$, on compute its
  time-invariant part (let us indicate this particular concept
  expression as $\Inv{Q_j}$). This gives $\Inv{Q_j}$ by computing for
  each disjunct $E_{j_i}$ in $Q_j$ its time-invariant information
  $\Inv{E_{j_i}}$.  If $E_{j_i} \SUBSUMEDBY_{\footnotesize\ALCF}
  \bot$, then $\Inv{E_{j_i}} = \bot$.  Otherwise, rewrite every conjunct in
  $E_{j_i}$ as showed in Figure~\ref{par-intro}, while the conjuncts
  not considered there are rewrote to $\top$. Now, unless there is an
  $\Inv{E_{j_i}} = \top$, $\Inv{Q_j} = \Inv{E_{j_1}} \OR \ldots \OR
  \Inv{E_{j_n}}$ must be conjunctively added to all the other nodes.
\end{enumerate}
\end{itemize}
}
\label{temp-comp-2}
\end{definition}
%%
\begin{proposition}[Equivalence of CEF]
  Every concept in existential form can be reduced into an equivalent
  completed existential concept.
\end{proposition}
%%
As for the \TLF\ case, both {\em covering} and {\em parameter
  introduction} can be computed independently. As a consequence of the
above normalization phase, the proposition~\ref{node-independence}
(node independence) is now true for \TLALCF\ concepts in CEF. Observe
that, to obtain a CEF concept, the steps of the normalization
procedure require the computation of the transitive closure of the
temporal relations -- which is an NP-complete
problem~\cite{van:Beek:90} -- and the computation of \ALCF\ 
subsumption -- which is a PSPACE-complete
problem~\cite{hollunder:nutt:dfki-90}.

%%%%%%%%%%%%%%%%%%%% Figura Parameter Intro
\begin{figure}
{\footnotesize
\begin{center}
\begin{lefteqnarrayfig}
\star g_1 \CHAIN \ldots \CHAIN \star g_n 
  \left[\CHAIN\ f \left[\CHAIN\ p\right]\right]: C   & ~\rightarrow~ &
    \star g_1 \CHAIN \ldots \CHAIN \star g_n: \top \per \\

\star g_1 \CHAIN \ldots \CHAIN \star g_n 
  \left[\CHAIN\ f \left[\CHAIN\ p\right]\right] \AGREE 
  g\left[\CHAIN\ q \right]                           & ~\rightarrow~ &
    \star g_1 \CHAIN \ldots \CHAIN \star g_n: \top \per \\

\star g_1 \CHAIN \ldots \CHAIN \star g_n \AGREE
  \star f_1 \CHAIN \ldots \CHAIN \star f_m       & ~\rightarrow~ &
      \star g_1 \CHAIN \ldots \CHAIN \star g_n \AGREE
      \star f_1 \CHAIN \ldots \CHAIN \star f_m \per \\

\star g_1 \CHAIN \ldots \CHAIN \star g_n
   \CHAIN\ g \left[\CHAIN\ p\right] \AGREE
   \star f_1 \CHAIN \ldots \CHAIN \star f_m 
   \left[\CHAIN\ f \left[\CHAIN\ q\right]\right] & ~\rightarrow~ & 
      \star g_1 \CHAIN \ldots \CHAIN \star g_n: \top \ \AND\ \\
      &  & \star f_1 \CHAIN \ldots \CHAIN \star f_m: \top \per \\

\star g_1 \CHAIN \ldots \CHAIN \star g_n \DISAGREE
  \star f_1 \CHAIN \ldots \CHAIN \star f_m           & ~\rightarrow~ &
      \star g_1 \CHAIN \ldots \CHAIN \star g_n \DISAGREE
      \star f_1 \CHAIN \ldots \CHAIN \star f_m \per \\
      
\star g\DISAGREE                                     & ~\rightarrow~ &
\star g\DISAGREE \per \\

\star g_1 \CHAIN \ldots \CHAIN \star g_n:(\star g_{n+1}\DISAGREE)
                                                     & ~\rightarrow~ &
  \star g_1 \CHAIN \ldots \CHAIN \star g_n:(\star g_{n+1}\DISAGREE) \per \\
  
\star g_1 \CHAIN \ldots \CHAIN \star g_n 
  \left[\CHAIN\ f \left[\CHAIN\ p\right]\right] \DISAGREE 
  g\left[\CHAIN\ q \right]                           & ~\rightarrow~ &
    \star g_1 \CHAIN \ldots \CHAIN \star g_n: \top \per \\

\star g_1 \CHAIN \ldots \CHAIN \star g_n 
   \CHAIN\ g \left[\CHAIN\ p\right] \DISAGREE
   \star f_1 \CHAIN \ldots \CHAIN \star f_m 
   \left[\CHAIN\ f \left[\CHAIN\ q\right]\right] & ~\rightarrow~ & 
      \star g_1 \CHAIN \ldots \CHAIN \star g_n: \top \ \AND\ \\
      &  & \star f_1 \CHAIN \ldots \CHAIN \star f_m: \top \per
\end{lefteqnarrayfig}
\end{center}
\ \hrulefill
}
\caption[par-intro]{\label{par-intro}
  Rewrite rules that compute the parameter introduction step.}
\end{figure}
%%%%%%%%%%%%%%%%%%%%

%%This can be proved if we observe that the
%%time-invariant part of a concept expression $Q = E_1 \OR \ldots \OR
%%E_n$ depends only on the time-invariant parts of each $E_i, \forall
%%i=1\ldots n$.  The ({\em parameter introduction}) rule considers all
%%the possible syntactical cases of completion concerning time-invariant
%%concept expressions by using the $\Inv{\cdot}$ translation.

%%This can be proved if we observe that the
%%time-invariant concept expressions in \TLALCF\ are: $\top$, $\star g_1
%%\CHAIN \ldots \CHAIN \star g_n:\top$, $\star g_1 \CHAIN \ldots \CHAIN
%%\star g_n \AGREE \star f_1 \CHAIN \ldots\CHAIN \star f_m$, with
%%$n,m\geq 1$ (those of \TLF), $\star g_1 \CHAIN \ldots \CHAIN \star g_n
%%\DISAGREE \star f_1 \CHAIN \ldots \CHAIN \star f_m$, with $n,m\geq 1$,
%%$\star g_1 \CHAIN \ldots \CHAIN \star g_n:(\star g_{n+1}\DISAGREE)$,
%%an arbitrary conjunction, or disjunction of these terms. 

Before the presentation of the last normalization phase, which will
eliminate redundant nodes, it is now possible to check whether a
concept expression is satisfiable.
%%
\begin{proposition}[Concept satisfiability]
  A \TLALCF\ concept in CEF, $\langle
  \overline{X},\overline{\TC},\overline{Q@X}\rangle$, is satisfiable
  (with the proviso that the temporal constraints are satisfiable) if
  and only if the non-temporal concepts labeling each node in
  $\overline{X}$ are satisfiable. Checking satisfiability of a
  \TLALCF\ concept in CEF is a PSPACE-complete problem.
\end{proposition}
%%
\begin{proof}
  Is a direct consequence of the node independence established by
  proposition~\ref{node-independence}, which is true also for \TLALCF\ 
  concepts in CEF.
\end{proof}

The normalization procedure now goes on by rewriting unsatisfiable
concepts to $\bot$ and then computing the {\em essential graph form\/}
for satisfiable concepts.  This last phase is more complex than for
the other temporal languages considered in this paper essentially
because \ALCF\ can express the $\top$ concept by means of a concept
expression (e.g., $\top = A \OR \NOT A$). From this consideration it
follows that in \TLALCF\ a redundant node can be derived from a
complex concept expression (e.g., both $A \OR \NOT A$, and $\star g:A
\OR \star g:\NOT A$ are redundant nodes). The key idea is that all the
time-invariant information is present in the \NOW\ node thanks to the
CEF. Thus it is needed only to extract this information from the \NOW\ 
node by computing the disjunctive normal form of $Q_{\NOW}$, applying
the $\Inv{\cdot}$ translation, and then testing whether
$\Inv{Q_{\NOW}} \SUBSUMEDBY_{\footnotesize\ALCF} Q_i$, for a given
node $x_i$.
%%
\begin{definition}[Essential graph]{
    The subgraph of the CEF of a \TLALCF\ conceptual temporal
    constraint network $T = \langle \overline{X}, \overline{\TC},
    \overline{Q@X}\rangle $ obtained by deleting the nodes $x_i$ such
    that $\Inv{Q_{\NOW}} \SUBSUMEDBY_{\footnotesize\ALCF} Q_i$ -- with
    the exception of the \NOW\ node -- is called {\em essential graph}
    of $T$: (${\sl ess}\ \!T$).}
\label{ess-graph-alcf}
\end{definition}
%%
\begin{proposition}[Equivalence of essential graph]
  Every CEF concept can be reduced into an equivalent essential graph
  form (and, obviously, every concept can be reduced into an
  equivalent essential graph form).
\end{proposition}

%%%%%%%%%%%%%%%%%%%%%% TL-ALCF SUBSUMPTION %%%%%%%%%%%%%%%%%%%%%%
\subsubsection*{Subsumption}

The overall normalization procedure reduces the subsumption problem in
\TLALCF\ to the subsumption between ${\cal ALCF}$ concepts.
%%
\begin{theorem}[\TLALCF\ concept subsumption]\label{subsumption-theorem3}
  A concept $C_1$ subsumes a concept $C_2$ if and only if there exists
  an s-mapping from the essential graph of $C_1$ to the essential
  graph of $C_2$.
\end{theorem}
%%
The above theorem gives a sound and complete algorithm for computing
subsumption between \TLALCF\ concepts (the proof is the same as the
one for theorem~\ref{subsumption-theorem}). The subsumption problem is
now PSPACE-hard, since satisfiability and subsumption for \ALCF\ 
concepts were proven to be
PSPACE-complete~\cite{hollunder:nutt:dfki-90}.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Extensions %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Extending the Expressivity for States}
\label{full:language}

The following suggests how to extend the basic language to cope with
important issues in the representation of states. (i) Homogeneity
allows us to consider properties of the world -- peculiar to states --
which remain true in each subinterval of the interval in which they
hold.  (ii) Persistence guarantees that a state holding as an effect
of an action continues to hold unless there is no evidence of its
falsity at some time.  An approach to the {\em frame} problem is then
presented, showing a possible solution to one of the most (in)famous
problems in AI literature. The following subsections shall be
interested more in semantically characterizing actions and states than
on computational properties.  The extensions proposed now to the
temporal languages are for having a full fledged {\em Description
  Logic for time and action}.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% HOMOGENEITY %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{figure}
\begin{center}
\setlength{\unitlength}{0.175in}
\begin{picture}(18,3.5)(-1,0)
{\footnotesize 
\thicklines
\put(-1, 1){\vector( 1, 0){5}}
\put(4, 3){\vector( 1, 0){5}}
\put(18,1){\vector(-1, 0){9}}
\put(4, 1){\vector(-1, 0){5}}
\put(9, 3){\vector(-1, 0){5}}
\put(9, 1){\vector( 1, 0){9}}
\put(-1,1.4){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]\HOM{\tt OnTable(BLOCK)}}}
\put(4,3.5){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\tt Simple-Stack(BLOCK)}}}
\put(9,1.4){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]\HOM{\tt OnBlock(BLOCK)}}}
\put(0,0.3){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\it x}}}
\put(5,2.3){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]\NOW}}
\put(10,0.3){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\it y}}} }
\end{picture}
\end{center}
\caption[Stack-1]{\label{Stack-1}
Temporal dependencies in the definition of the {\tt Simple-Stack} 
action.}
\end{figure}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\subsection{Homogeneity} 
\label{homo}

In the temporal literature {\em homogeneity} characterizes the
temporal behavior of world states: when a state holds over an interval
of time $t$, it also holds over subintervals of $t$. Thus, if a block
is on the table for a whole day, one can conclude that it is also
on the table in the morning.  On the other hand, actions are not
necessarily homogeneous. In the linguistic literature a difference is
made between {\em activity} and {\em performance} verbs. The
distinction comes out in the fact that activity verbs do have
sub-events that are denoted by the same verb, whereas performance
verbs do not.  Generally, activity verbs represent ongoing events, for
example {\em to eat} and {\em to run}, and can be described as
homogeneous predicates; whereas performance verbs represent events
with a well defined granularity in time, such as {\em to prepare
  spaghetti}. Performance verbs are an example of anti-homogeneous
events: if they occur over an interval of time $t$, then they do not
occur over a subinterval of $t$, as they would not yet be completed.

The language is extended by introducing the {\em Homogeneity} operator:

\begin{Eqnarraycomm}
C,D & \rightarrow\ & \HOM C  & \mbox{(homogeneous concept)} 
\end{Eqnarraycomm}

\noindent The semantics of homogeneous concepts is easily given in terms of the
semantics of the temporal universal quantifier: $\HOM C \equiv
\ALLTIME x\ (x\ ({\sf =},{\sf s},{\sf d},{\sf f})\ \NOW)\per\ C@x$.
This means that $\HOM C$ is an homogeneous concept if and only if when
it holds at an interval it remains true at each subinterval. In
particular, $\ALLTIME x$ universally qualifies the temporal variable
$x$, while the temporal constraint $(x\ ({\sf =},{\sf s},{\sf d},{\sf
  f})\ \NOW)$ imposes that $x$ is a generic interval contained in
\NOW. Moreover, it is always true that $\HOM C\SUBSUMEDBY C$, i.e.,
$\HOM C$ is a more specific concept than $C$.

Let us consider as an example a more accurate definition of the {\tt
  Basic-Stack} action (see Section~\ref{expressivity}):

\vspazio\noindent
{\tt Simple{-}Stack}$ ~\doteq~
 \SOMETIME 
     (x\ y) (x\ {\sf m}\ \NOW)(\NOW\ {\sf m}\ y)\per\ 
        \mbox{\large(}
        \parbox[t]{26em}{$
           ({\tt \Parm BLOCK}: \HOM{\tt OnTable})@x\ \AND\ \\
           ({\tt \Parm BLOCK}:\HOM{\tt OnBlock})@y \mbox{\large)}
          $}
         $

\vspazio

\noindent Figure~\ref{Stack-1} shows the temporal dependencies of the
intervals in which the {\tt Simple-Stack} holds. The difference with the
{\tt Basic-Stack} action is the use of the homogeneity operator. In fact,
since the predicates {\tt OnTable} and {\tt OnBlock} denote states, their
homogeneity should be explicitly declared.  The assertion {\tt
  Simple-Stack}$(i,a)$ says that $a$ is an individual action of type {\tt
  Simple-Stack} occurred at interval $i$.  Moreover, the same assertion
implies that $a$ is related to a ${\tt \Parm BLOCK}$, say $b$, which is of
type {\tt OnTable} at some interval $j$ -- meeting $i$ -- {\em and} at all
intervals included in $j$, while it is of type {\tt OnBlock} at another
interval $l$ -- met by $i$ -- {\em and} at all intervals included in $l$:

\vspazio\noindent
{\tt Simple-Stack}$(i,a)\Longrightarrow \exists b\per\ 
   {\tt \Parm BLOCK}(a,b)\ \wedge \exists\ j,l\per\
   \parbox[t]{28em}{$   
     {\sf m}(j,i) \wedge {\sf m}(i,l) \wedge \\ 
     \forall\ \hat{\j},\hat{l}\per\ 
     \parbox[t]{26em}{$   
       ({\sf =},{\sf s},{\sf d},{\sf f})(\hat{\j},j) \wedge 
       ({\sf =},{\sf s},{\sf d},{\sf f})(\hat{l},l) \rightarrow\\
       {\tt OnTable}(\hat{\j},b) \wedge {\tt OnBlock}(\hat{l},b).
$}
$}
$\vspazio

\noindent Note that the {\tt Simple-Stack} action
subsumes the {\tt Instant\mbox{-}Stack} action, whose temporal
dependencies are depicted in Figure~\ref{Stack-2}:

\vspazio\noindent
{\tt Instant\mbox{-}Stack}$ ~ \doteq ~
   \SOMETIME
      (z\ y) (\NOW\ {\sf f}\ z)(\NOW\ {\sf m}\ y)\per\ 
        \mbox{\large(}
        \parbox[t]{26em}{$  
         ({\tt \Parm BLOCK}: \HOM{\tt OnTable})@z\ \AND\ \\
         ({\tt \Parm BLOCK}:\HOM{\tt OnBlock})@y 
         \mbox{\large)}
          $}
         $

\vspazio

\begin{figure}[t]
\begin{center}
\setlength{\unitlength}{0.175in}
\begin{picture}(18,3.5)(0,0)
{\footnotesize
\thicklines
\put(0, 1){\vector( 1, 0){9}}
\put(4, 3){\vector( 1, 0){5}}
\put(18,1){\vector(-1, 0){9}}
\put(9, 1){\vector(-1, 0){9}}
\put(9, 3){\vector(-1, 0){5}}
\put(9, 1){\vector( 1, 0){9}}
\put(0,1.4){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]\HOM{\tt OnTable(BLOCK)}}}
\put(4,3.5){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\tt Instant\mbox{-}Stack(BLOCK)}}}
\put(9,1.4){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]\HOM{\tt OnBlock(BLOCK)}}}
\put(1,0.3){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\it z}}}
\put(5,2.3){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]\NOW}}
\put(10,0.3){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\it y}}} }
\end{picture}
\end{center}
\caption[Stack-2]{\label{Stack-2}
Temporal dependencies in the definition of the {\tt Instant\mbox{-}Stack} 
action.}
\end{figure}

\noindent Subsumption holds because the class of intervals -- obtained by
homogeneity of the state {\tt OnTable} as defined in the {\tt
  Simple-Stack} action -- including $x$ and all its subintervals is a
subset of the class of intervals over which the block is known to be
on the table, according to the definition of {\tt
  Instant\mbox{-}Stack} -- this latter class includes all the
subintervals of $z$.

If the {\tt Instant\mbox{-}Stack} action had been defined without the
\HOM\ operator, then it would not specialize any more the {\tt
  Simple-Stack} action. In fact, according to such a weaker definition
of {\tt Instant\mbox{-}Stack}, specifying that the object is on the
table at $z$ does not imply that the object is on the table at
subintervals of $z$; in particular, it is not possible to deduce any
more that the object is on the table at $x$ and its subintervals, as
specified in the definition of {\tt Simple-Stack} action. Moreover,
the {\em weak} {\tt Instant\mbox{-}Stack} action type would not
specialize the {\em weak} {\tt Simple-Stack} action type -- i.e., {\tt
  Basic\mbox{-}Stack} -- too. Thus, homogeneity helps us to define
states and actions in a more accurate way, such that important
inferences are captured.

As seen above, the definition of homogeneity makes use of universal
temporal quantification.  Remember that subsumption in a
propositionally complete Description Logic with both existential and
universal temporal quantification is undecidable and it is still an
open problem if it becomes decidable in absence of
negation~\cite{bettini:tesi-93}. The homogeneity operator is a
restricted form of universal quantification. An even more restricted
form interests us here, where the concept $C$ in $\HOM C$ does not
contain any other temporal operator (called {\em simple homogeneous
  concept}).  The expressiveness of the resulting logic is enough, for
example, to correctly represent the homogeneous nature of states.
In~\cite{artale:bettini:franconi:94} an algorithm to compute
subsumption in \TLF\ augmented with the homogeneity operator is
proposed.  Even if a formal proof is still not available, good
arguments are discussed to conjecture its completeness. This would
also prove decidability of this logic and of the corresponding modal
logics.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% YSP %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\subsection{Persistence} 
\label{frame}

This Section shows how our framework can be successfully extended in a
general way to cope with {\em inertial} properties.  In the basic
temporal language, a property holding, say, as a post-condition of an
action at a {\em certain} interval, is not guaranteed to hold anymore
at other included or subsequent intervals.  This is the reason why we
propose an extended formalism, in which {\em states} can be
represented as homogeneous and persistent concepts.  As a motivation
for introducing the possibility of representing persistent properties
in the language, this Section considers how to solve the {\em frame
  problem}, and in particular the famous example of the Yale Turkey
Shooting Scenario~\cite{sandewall:94,allen:ferguson:jlc-94}, formerly
known as the {\em Yale Shooting Problem}.

An inertia operator ``$\PERS$'' is introduced here. Intuitively, $\PERS C$
is currently true if it was true at a preceding interval -- say $i$ --
and there is no evidence of the falsity of $C$ at any interval between
the current one and $i$. Thus, the property of an individual of being
of type $C$ {\em persists} over time, unless a contradiction arises.

%%%%%%%%%%%%%%%%%% Inertia Definition

The formalization of the inertia operator makes use of the epistemic
operator ${\bf K}$~\cite{donini:et:al:kr-92}, in which ${\bf K} C$
denotes the set of individuals {\it known} to be instances of the
concept $C$\footnote{An {\it epistemic interpretation} is a pair
  ($\I$,${\cal W}$) in which $\I$ is an interpretation and ${\cal W}$
  is a set of interpretations such that (${\bf K} C$)$^{\I,{\cal W}} =
  \bigcap_{{\cal J} \in {\cal W}}$($C^{{\cal J},{\cal W}}$).}.
%%
\begin{definition}[Inertia]
$
\PERS C(j,a)~~\mbox{\rm iff} \\
     \exists i\per\ 
     \parbox[t]{37em}{$
           start(i)\leq start(j)\ \wedge\ C(i,a)\ \wedge \\
           \forall h\per\ start(h)\geq end(i)\ \wedge\ end(h)\leq 
                          end(j)\ \rightarrow\ \NOT {\bf K}\NOT C(h,a)\per
      $}
$
\end{definition}
%%
\noindent where {\em start} and {\em end} are two functions giving
respectively the starting and the ending point of an interval --
conditions on endpoints are simpler and more readable than their
equivalents on interval relations; $\NOT {\bf K}\NOT C(h,a)$ means
that it is not known that $a$ is not of type $C$ at interval $h$.
Furthermore, the following relation holds: $\forall a,j\per\ 
C(j,a)\rightarrow \PERS C(j,a)$; i.e., $\PERS C$ subsumes $C$. The
above definition can be captured by a temporal language equipped with
the epistemic operator -- ${\bf K}$ -- and the homogeneity operator --
\HOM:

\begin{leftarray}
\PERS C  \equiv  C \OR 
\SOMETIME  (x\ y)\
  (x\ ({\sf b,m,o,fi,di})\ \NOW)(x\ ({\sf s,si})\ y) (y\ {\sf fi}\ \NOW)\per 
  (C@x \AND \HOM(\NOT {\bf K} \NOT C)@y)
\end{leftarray}

\begin{figure}
\begin{center}
\setlength{\unitlength}{0.175in}
\begin{picture}(24,4.5)(0,0.8)
\thicklines
\put( 0,4){\vector( 1, 0){4}}
\put( 0,4){\vector(-1, 0){0}}
\put(10,4){\vector(-1, 0){6}}
\put(14,4){\vector( 1, 0){4}}
\put(14,4){\vector(-1, 0){0}}
\put(12,2){\vector( 1, 0){6}}
\put(24,4){\vector(-1, 0){6}}
\put(24,2){\vector(-1, 0){6}}
{\footnotesize
\put( 0,4.5){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\tt Load(GUN)}}}
\put( 1,3.3){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\NOW}}}
\put(12.3,4.5){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\tt Fire(GUN,TARGET)}}}
\put(15,3.3){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\NOW}}}
\put(4.2,4.5){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\tt Loaded(GUN)}}}
\put(5.2,3.3){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\tt $x$}}}
\put(18.7,2.5){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\tt Dead(TARGET)}}}
\put(19.7,1.3){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\tt $y$}}}
\put(12,2.5){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\tt $\NOT$\PERS Loaded(GUN)}}}
\put(13,1.3){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\tt $x$}}}
\put(18.7,4.5){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\tt $\NOT$Loaded(GUN)}}}
\put(19.7,3.3){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\tt $z$}}}
\thinlines
\put(18, 1.8){\line(0,1){2.4}}
\put(18,2){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\circle{1.5}}}}
\put(17.5,0.8){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\it or}}}
}\end{picture}
\end{center}
\caption[ysp-1]{\label{ysp-1}
  Definitions of the actions {\tt Load} and {\tt Fire}.}
\end{figure}
%%%%%%%%%%%%%%%%%%%%%

Two action types are defined, {\tt Load} -- with the parameter {\tt \Parm GUN}
-- and {\tt Fire} -- with the parameters {\tt \Parm GUN} and {\tt \Parm
  TARGET} (Figure~\ref{ysp-1}):

\begin{leftarray}
{\tt Load} ~~ \doteq ~~ \SOMETIME {x}\ {(\NOW\ {\sf m}\ x)}\per\ {\tt \Parm
GUN}: {\tt Loaded}@x
\\
{\tt Fire} ~~ \doteq ~~ \SOMETIME 
  (x\ y\ z)\ \parbox[t]{28em}
  {$
  (\NOW\ {\sf f}\ x)(\NOW\ {\sf m}\ y) (\NOW\ {\sf m}\ z) \per \\
  ({\tt \Parm GUN}: {\tt \NOT\PERS Loaded}@x \OR 
   {\tt \Parm TARGET}:{\tt Dead}@y)\ \AND  
  {\tt \Parm GUN}: {\tt \NOT Loaded}@z
  $}
\end{leftarray}

\noindent The action {\tt Load} describes loading a gun.
The action {\tt Fire} describes firing the gun against a target:
effects of firing are that the gun becomes unloaded and either the
target is dead or the gun was not loaded -- possibly by inertia --
before firing. The Yale Shooting Problem considers the situation
described by the following set of assertions (ABox):

\begin{leftarray}
{\tt Load}(i,{\it load\mbox{-}action}),\ 
{\tt \Parm GUN}({\it load\mbox{-}action},{\it gun}),\ 
{\sf a}(j,i),\ {\tt Fire}(j,{\it fire\mbox{-}action}),\\
{\tt \Parm GUN}({\it fire\mbox{-}action},{\it gun}),\
{\tt \Parm TARGET}({\it fire\mbox{-}action},{\it fred}).
\end{leftarray}

\noindent i.e., at the beginning the {\it gun} is loaded; then, the action of
firing the {\it gun} against the target $fred$ is performed. According to the
semantics of the language, logical consequences of the knowledge base
$\Sigma$ are:

\begin{leftarray}
  \Sigma \models \exists i_1 \per\ {\sf m}(i,i_1) \wedge {\tt Loaded}(i_1,{\it gun})\\ 
  \Sigma \models \exists j_1 \per\ {\sf m}(j,j_1) \wedge {\tt \NOT
                                                         Loaded}(j_1,{\it gun})\\ 
  \Sigma \models \exists j_0 \per\ {\sf f}(j,j_0) \wedge {\tt \PERS
                                                         Loaded}(j_0,{\it gun})\\ 
  \Sigma \models \exists j_2 \per\ {\sf m}(j,j_2)\wedge {\tt Dead}(j_1,
                                                              {\it fred}).
\end{leftarray}

\noindent i.e., (see also Figure~\ref{ysp-2}) (i) the {\tt Load} action makes
the {\it gun} loaded; (ii) the {\tt Fire} action makes the {\it gun} unloaded
{\em at the end}; (iii) since there is no evidence to the contrary, the {\it gun} 
is still loaded at $j_0$ by inertia; (iv) since the gun is not unloaded at
$j_0$, the target $fred$ must be dead.

%% The inertia is characterized only at the extensional level since we are
%% interested in deducing new facts from the asserted ones,

%%%%%%%%%%%%%%%%%%%%%%%
\begin{figure}
\begin{center}
\setlength{\unitlength}{0.175in}
\begin{picture}(24,4.5)(0,1.3)
\thicklines
\put( 0,4){\vector( 1, 0){4}}
\put( 0,4){\vector(-1, 0){0}}
\put(10,4){\vector(-1, 0){6}}
\put(14,4){\vector( 1, 0){4}}
\put(14,4){\vector(-1, 0){0}}
\put(12,2){\vector( 1, 0){6}}
\put(24,4){\vector(-1, 0){6}}
\put(24,2){\vector(-1, 0){6}}
{\footnotesize
\put( 0,4.5){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\tt Load({\it gun})}}}
\put(13,4.5){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\tt Fire({\it gun},{\it fred})}}}
\put(4.2,4.5){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\tt Loaded({\it gun})}}}
\put(18.7,2.4){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\tt Dead({\it fred})}}}
\put(12,2.4){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\tt \PERS Loaded({\it gun})}}}
\put(18.7,4.5){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\tt $\NOT$Loaded({\it gun})}}}
\put( 1, 3.3){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\tt $i$}}}
\put( 5, 3.3){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\tt $i_1$}}}
\put(13, 1.3){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\tt $j_0$}}}
\put(15, 3.3){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\tt $j$}}}
\put(19, 3.3){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\tt $j_1$}}}
\put(19, 1.3){\makebox(0,0)[lb]{\raisebox{0pt}[0pt][0pt]{\tt $j_2$}}}
\thinlines
\put(18, 1.8){\line(0,1){2.4}}
}\end{picture}
\end{center}
\caption[ysp-2]{\label{ysp-2}
  Actions instances in the Yale Shooting Problem.}
\end{figure}
%%%%%%%%%%%%%%%%%%%%%%%

Since the inertia operator is useful to describe the behavior of {\em
  properties}, which are characterized as homogeneous concepts, a
simple way of representing persistence in the context of homogeneous
concepts is proposed.
%%
\begin{proposition}
  Let $P$ be a property -- i.e., $P \doteq \HOM P'$ is an homogeneous
  concept -- and $\Sigma$ a knowledge base such that $\Sigma \not
  \models P(j,a)$. $\PERS P(j,a)$ is true in $\Sigma$ -- i.e., $\Sigma
  \models \PERS P(j,a)$ -- if and only if two intervals $i,k$ exist
  such that: $\Sigma \models \mbox{\large (}start(i)\leq start(j)\ 
  \wedge\ P(i,a) \mbox{\large )}$ and $\Sigma \cup \set{ {\sf
      s}(i,k),\ {\sf f}(j,k),\ P(k,a)}$ is satisfiable.
\end{proposition}
%%
\begin{proof}
  The entailment test verifies the first part of the definition of
  inertia, while the satisfiability test verifies that, between the
  interval at which the system knows that the individual $a$ belongs
  to $P$ -- $i$ -- and the interval at which $P(a)$ is deduced by
  inertia -- $j$ -- does not exist an interval $h$ at which the system
  knows that $P(a)$ is false.  Indeed, such interval $h$ would be
  related to the interval $k$ by the relation {\sf in} and since it is
  supposed that $P$ is homogeneous, the knowledge base with $\NOT
  P(h,a) \wedge P(k,a) \wedge {\sf in}(h,k)$ would be inconsistent.
\end{proof}

\noindent The deduction $P(j,a) \rightarrow \PERS P(j,a)$
can be obtained as a particular case of the above stated proposition.

%%%%%%%%%%%%%%%%%%%%%%%% RELATED WORKS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Related Works}
\label{related}

The original formalism devised by Allen~\citeyear{allen:91} forms, in its
very basis, the foundation for our work. It is a predicate logic in which
interval temporal networks can be introduced, properties can be
asserted to {\em hold} over intervals, and events can be said to {\em
  occur} at intervals.  His approach is very general, but it suffers
from problems related to the semantic formalization of the predicates
{\tt hold} and {\tt occur}~\cite{blackburn:92}. Moreover,
computational properties of the formalism are not analyzed. The study
of this latter aspect was, on the contrary, our main concern.  

In the Description Logic literature, other approaches for representing
and reasoning with time and action were proposed. In the beginning the
approaches based on an explicit notion of time are surveyed, and then
the \Strips-like approaches are considered. This Section ends by
illustrating some of the approaches devoted to temporally extend the
situation calculus.

%%%%%%%%%%%%%%%%%%%%%% Bettini %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Bettini~\citeyear{bettini:dke-97} suggests a variable-free extension with
both existential and universal temporal quantification.  He gives
undecidability results for a class of temporal languages -- resorting
to the undecidability results of  Halpern and Shoham's temporal
logic -- and investigates approximated reasoning algorithms.
Basically, he extends the ${\cal ALCN}$ description logics with the
existential and universal temporal quantifiers, but, unlike our
formalism, explicit interval variables are not allowed. The temporal
quantification makes use of a set of temporal constraints on two
implicit intervals: the reference interval and the current one. In
this framework, the concept of ${\tt Mortal}$ can be defined as:

\vspazio\noindent
${\tt Mortal} ~ \doteq ~ 
     {\tt LivingBeing}~ \AND~ \ST {({\sf after})} 
     {({\bf not}~{\tt LivingBeing})}
$
\vspazio

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Schild %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

Schild~\citeyear{schild:ijcai-93} proposes the embedding of {\em
  point}-based tense operators in a propositionally closed Description
Logic.  He proved that satisfiability in ${\cal ALCT}$, the
point-based temporal extension of ${\cal ALC}$, interpreted on a
linear, unbounded and discrete temporal structure, is PSPACE-complete.
His ideas were applied by~\cite{fischer:92,neuwirth:93} in the
\Back\ system. Note that a point-based temporal ontology is
unable to express all the variety of relations between intervals.


%%%%%%%%%%%%%%%%%%%%%%%%%%% Baader & Laux %%%%%%%%%%%%%%%%%%%%%%%%%

Baader and Laux~\citeyear{baader:laux:ijcai-95} integrate modal operators
for time and belief in a terminological system looking for an adequate
semantics for the resulting combined language. The major point in this
paper is the possibility of using modal operators not only inside
concept expressions but also in front of concept definitions and
assertions. The following example shows the notion of {\tt
  Happy-father}, where different modalities interact:

\vspazio
\noindent
$
[{\tt BEL\mbox{-}JOHN}]{\Large (} {\tt Happy\mbox{-}father} \doteq 
   \Parboxa{
     \SOME {{\tt MARRIED\mbox{-}TO}}{({\tt Woman} \AND 
     [{\tt BEL\mbox{-}JOHN}]{\tt Pretty})} \AND \\
     \langle {\tt future} \rangle \ALL {{\tt CHILD}}{{\tt Graduate}}
     {\Large )}}
$
\vspazio

\noindent In this case, it is {\em John}'s belief that a 
{\tt Happy-father} is someone married to a woman believed to be pretty
by {\em John}, and whose children will be graduates sometime in the
future. The semantics has a Kripke-style: each modal operator is
interpreted as an accessibility relation on a set of possible worlds,
while the domain of objects is split into (possible) different domain
objects, each one depending on a given world. This latter choice
captures the case of different definitions for the same concept --
such as $[{\tt BEL\mbox{-}JOHN}](A \doteq B)$ and $[{\tt
  BEL\mbox{-}PETER}](A \doteq C)$ -- since the two formul\ae\ are
evaluated in different worlds. The main restriction is that all the
modal operators do not satisfy any specific axioms for belief or time.
On the other hand, the language is provided with a complete and
terminating algorithm that should serve, as the authors propose,
``...as a basis for satisfiability algorithms for more complex
languages''.

%%\vspazio

%%%%%%%%%%%%%%%%%%%%%%%%% DL-Survey %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

There are Description Logics intended to represent and reasoning about
actions following the \Strips\ tradition. Heinsohn, Kudenko, Nebel and
Profitlich~\citeyear{heinsohn:et:al:ijcai-93} describe the \Rat\ system,
used in the {\sc Wip} project at the German Research Center for AI
(DFKI).  They use a Description Logic to represent both the world
states and atomic actions.  A second formalism is added to compose
actions in plans and to reason about simple temporal relationships.
No explicit temporal constraints can be expressed in the language.
\Rat\ actions are defined by the change of the world state they cause,
and they are instantaneous as in the \Strips-like systems, while plans
are linear sequences of actions.  The most important service offered
by \Rat\ is the {\em simulated execution} of part of a plan, checking
if a given plan is {\em feasible} and, if so, computing the global
pre- and post-conditions.  The feasibility test is similar to the
usual consistency check for a concept description: they {\em
  temporally project} the pre- and post-conditions of individual
actions composing the plan, respectively backward and forward.  If
this does not lead to an inconsistent initial, final or intermediate
state, the plan is feasible and the global pre- and post-conditions
are determined as a side effect.

Devanbu and Litman~\citeyear{devanbu:litman:kr-91,devanbu:litman:ai-96}
describe the \Clasp\ system, a {\em plan-based} knowledge
representation system extending the notion of subsumption and
classification to plans, to build an efficient information retrieval
system. In particular, \Clasp\ was used to represent plan-like
knowledge in the domain of telephone switching software by extending
the use of the software information system {\sc
  lassie}~\cite{devanbu:et:al:acm-91}. \Clasp\ is designed for
representing and reasoning about large collections of plan
descriptions, using a language able to express temporal, conditional
and looping operators. Following the \Strips\ tradition, plan
descriptions are built starting from states and actions, both
represented by using the \Classic~\cite{brachman:et:al:sowa-91}
terminological language. Since plans constructing operators correspond
to regular expressions, algorithms for subsumption integrate work in
automata theory with work in concept subsumption. The temporal
expressive power of this system can capture to sequences, disjunction
and iterations of actions and each action is instantaneous.
Furthermore, state descriptions are restricted to a simple conjunction
of primitive \Classic\ concepts. Like \Rat, \Clasp\ checks if an
instantiated plan is well formed, i.e., the specified sequence of
individual actions are able to transform the given initial state into
the goal state by using the \Strips\ rules.

%%%%%%%%%%%%%%%%%%%%%%%% situation calculus %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%\vspazio

We end up by reporting on the efforts made by researchers in the
situation calculus field to overcome the strict sequential perspective
inherent to this framework.  Recent works enrich the original
framework to represent properties and actions having different truth
values depending not only on the situation but also on time. The work
of Reiter~\citeyear{reiter:kr-96}, moving from the results showed by
Pinto~\citeyear{pinto:phd-94} and by
Ternovskaia~\citeyear{ternovskaia:ecai-94}, provides a new axiomatization
of the situation calculus able to capture concurrent actions,
properties with continuous changes, and natural exogenous actions --
those under nature's control. The notion of {\em fluent} -- which
models properties of the world -- and {\em situation} are maintained.
Each action is instantaneous and responsible for changing the actual
situation to the subsequent one. Concurrent actions are simply sets of
instantaneous actions that must be coherent, i.e., the action's
collection must be non empty and all the actions occur at the same
time. Pinto~\citeyear{pinto:phd-94} and Reiter~\citeyear{reiter:kr-96}
introduce the time dimension essentially to capture both the
occurrence of the natural actions, due to known laws of physics --
i.e., the ball bouncing at times prescribed by motion's equations --
and the dynamic behavior of physical objects -- i.e., the position of
a falling ball. This is realized by introducing a time argument for
each action function, while properties of the world are divided into
two different classes: classical fluents that hold or do not hold
throughout situations, and {\em continuous parameters\/} that may
change their value during the time spanned by the given situation.

More devoted to have a situation calculus with a time interval
ontology is the work of Ternovskaia~\citeyear{ternovskaia:ecai-94}. In
order to describe {\em processes} -- i.e., actions extended in time --
she introduces durationless actions that initiate and terminate those
processes. As a matter of fact, processes become fluents, with
instantaneous events -- {\em Start(Fluent)} and {\em Finish(Fluent)}
-- which respectively make true or false the corresponding fluent, and
with persistence assumptions that make the fluent true during the
interval. For example, in a blocks world the {\em picking-up} process
is treated as a fluent with {\em Start(picking-up(x))} and {\em
  Finish(picking-up(x))} instantaneous actions that enable or falsify
the {\em picking-up} fluent.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% CONCLUSIONS %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Conclusions} 
\label{conclusion}

The main objective of this paper was the design of a class of logical
formalisms for uniformly representing time, actions and plans.
According to this framework, an action has a duration in time, it can
have parameters, which are the ties with the temporal evolution of the
world, and it is possibly associated over time with other actions.  A
model-theoretic semantics including both a temporal and an object
domain was developed, for giving both a meaning to the language
formul\ae\ and a well founded definition of the various reasoning
services, allowing us to prove soundness and completeness of the
corresponding algorithms. The peculiar computational properties of
this logic make it an effective representation and reasoning tool for
plan recognition purposes. An action taxonomy based on subsumption can
be set up, and it can play the role of a plan library for plan
retrieval tasks.

This paper contributes to exploration of the decidable realm of
interval-based temporal extensions of Description Logics. It presented
complete procedures for subsumption reasoning with \TLF, \TLUFU\ and
\TLALCF.  In addition, the subsumption problem for \TLF\ was proven an
NP-complete problem. The subsumption procedures are based on an
interpretation preserving transformation that operates a separation
between the temporal and the non-temporal parts of the formalism.
Thus, the calculus can adopt distinct standard procedures developed in
the Description Logics community and in the temporal constraints
community. To obtain decidable languages the key idea was to restrict
the temporal expressivity by eliminating the universal quantification
on temporal variables.  While a propositionally complete Description
Logic with both existential and universal temporal quantification is
undecidable, it is still an open problem if it becomes decidable in
absence of negation. With the introduction of the homogeneity operator
investigation of the impact of a restricted form of temporal
universal quantification in the language \TLF\ was begun.

Several extensions were proposed to the basic temporal language.  With
the possibility to specify homogeneous predicates the temporal
behavior of world states can be described in a more natural way, while
the introduction of the non-monotonic inertial operator gives rise to
some forms of temporal prediction.  Another extension -- not
considered in this paper -- deals with the possibility of relating an
action to more elementary actions, {\em decomposing} it in partially
ordered steps~\cite{artale:franconi:dl-95}. This kind of reasoning is
found in hierarchical planners like {\sc Nonlin}~\cite{tate:77}, {\sc
  Sipe}~\cite{wilkins:88} and {\sc
  Forbin}~\cite{dean:firby:miller:90}.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Acknowledgements %%%%%%%%%%%%%%%%%%%%%%%%

\acks{This paper is a substantial extension and revision
  of~\cite{artale:franconi:kr-94}.  The work was partially supported
  by the Italian National Research Council (CNR) project ``Ontologic
  and Linguistic Tools for Conceptual Modeling'', and by the
  ``Foundations of Data Warehouse Quality'' ({\em DWQ\/}) European
  ESPRIT IV Long Term Research (LTR) Project 22469.  The first author
  wishes to acknowledge also LADSEB-CNR of Padova and the University
  of Firenze for having supported part of his work. Some of the work
  carried on for this paper was done while the second author was
  working at ITC-irst, Trento. This work owes a lot to our colleagues
  Claudio Bettini and Alfonso Gerevini, for having introduced us many
  years ago to the {\em temporal maze}.  Special thanks to Achille C.
  Varzi, for taking time to review the technical details of the paper
  and for his insightful comments on the philosophy of events, and to
  Fausto Giunchiglia, for useful discussions and feedback.  Thanks to
  Paolo Bresciani, Nicola Guarino, Eugenia Ternovskaia and Andrea
  Schaerf for enlightening comments on earlier drafts of the paper.
  Werner Nutt and Luciano Serafini helped us to have a deeper insight
  into logic.  We would also like to thank Carsten Lutz for the
  helpful discussions we had with him about temporal representations.
  Many anonymous referees checked out many errors of previous versions
  of the paper.  All the errors of the paper are, of course, our own.}

%%%%%%%%%%%%%%%%%%%%% references %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\bibliographystyle{theapa}

%%%%%%%%%%%%%%%%%%%%% bibtex references %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\vskip 0.2in
%\bibliography{references-time}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% Insert .bbl file here

\begin{thebibliography}{}

\bibitem[\protect\BCAY{Allen}{Allen}{1991}]{allen:91}
Allen, J.~F. \BBOP1991\BBCP.
\newblock \BBOQ Temporal reasoning and planning\BBCQ\
\newblock In Allen, J.~F., Kautz, H.~A., Pelavin, R.~N., \BBA\ Tenenberg,
  J.~D.\BEDS, {\Bem Reasoning about Plans}, \BCH~1, \BPGS\ 2--68. Morgan
  Kaufmann.

\bibitem[\protect\BCAY{Allen \BBA\ Ferguson}{Allen \BBA\
  Ferguson}{1994}]{allen:ferguson:jlc-94}
Allen, J.~F.\BBACOMMA\  \BBA\ Ferguson, G. \BBOP1994\BBCP.
\newblock \BBOQ Actions and events in interval temporal logic\BBCQ\
\newblock {\Bem Journal of Logic and Computation}, {\Bem 4\/}(5).
\newblock Special Issue on Actions and Processes.

\bibitem[\protect\BCAY{Artale, Bettini, \BBA\ Franconi}{Artale
  et~al.}{1994}]{artale:bettini:franconi:94}
Artale, A., Bettini, C., \BBA\ Franconi, E. \BBOP1994\BBCP.
\newblock \BBOQ Homogeneous concepts in a temporal description logic\BBCQ\
\newblock In F.Baader, M.Lenzerini, W.Nutt, \BBA\ P.F.Patel-Schneider\BEDS,
  {\Bem Workshop Notes of the Int. Workshop on Description Logics, DL-94},
  \BPGS\ 36--41\ Bonn, Germany. DFKI, Saarbr\"ucken.
\newblock Tech. Rep. DFKI-D-94-10.

\bibitem[\protect\BCAY{Artale \BBA\ Franconi}{Artale \BBA\
  Franconi}{1994}]{artale:franconi:kr-94}
Artale, A.\BBACOMMA\  \BBA\ Franconi, E. \BBOP1994\BBCP.
\newblock \BBOQ A computational account for a description logic of time and
  action\BBCQ\
\newblock In J.Doyle, E.Sandewall, \BBA\ P.Torasso\BEDS, {\Bem Proc.\ of the
  4$^{~th}$ International Conference on Principles of Knowledge Representation
  and Reasoning}, \BPGS\ 3--14\ Bonn, Germany. Morgan Kaufmann.

\bibitem[\protect\BCAY{Artale \BBA\ Franconi}{Artale \BBA\
  Franconi}{1995}]{artale:franconi:dl-95}
Artale, A.\BBACOMMA\  \BBA\ Franconi, E. \BBOP1995\BBCP.
\newblock \BBOQ Hierarchical plans in a description logic of time and
  action\BBCQ\
\newblock In A.Borgida, M.Lenzerini, D.Nardi, \BBA\ B.Nebel\BEDS, {\Bem
  Workshop Notes of the Int. Workshop on Description Logics. DL-95}, \BPGS\
  1--5\ Roma, Italy.
\newblock Tech. Rep. 07.95. Also in the Workshop Notes of the IJCAI-95 Workshop
  on ``The Next Generation of Plan Recognition Systems: Challanges for and
  Insight from Related Areas of {AI}'', Montr\'eal, 1995.

\bibitem[\protect\BCAY{Baader, B\"urckert, Heinsohn, Hollunder, M\"uller,
  Nebel, Nutt, \BBA\ Profitlich}{Baader et~al.}{1990}]{baader:et:al:proposal-90}
Baader, F., B\"urckert, H.-J., Heinsohn, J., Hollunder, B., M\"uller, J.,
  Nebel, B., Nutt, W., \BBA\ Profitlich, H.-J. \BBOP1990\BBCP.
\newblock \BBOQ Terminological knowledge representation: a proposal for a
  terminological logic\BBCQ\
\newblock Technical memo\ TM-90-04, DFKI, Saarbr\"ucken, Germany.

\bibitem[\protect\BCAY{Baader \BBA\ Laux}{Baader \BBA\
  Laux}{1995}]{baader:laux:ijcai-95}
Baader, F.\BBACOMMA\  \BBA\ Laux, A. \BBOP1995\BBCP.
\newblock \BBOQ Terminological logics with modal operator\BBCQ\
\newblock In {\Bem Proc.\ of the 13$^{~th}$ IJCAI}, \BPGS\ 808--814\ Montreal,
  Canada.

\bibitem[\protect\BCAY{Bettini}{Bettini}{1993}]{bettini:tesi-93}
Bettini, C. \BBOP1993\BBCP.
\newblock {\Bem Temporal Extensions of Terminological Languages}.
\newblock Ph.D.\ thesis, Computer Science Department, University of Milan,
  Italy.

\bibitem[\protect\BCAY{Bettini}{Bettini}{1997}]{bettini:dke-97}
Bettini, C. \BBOP1997\BBCP.
\newblock \BBOQ Time dependent concepts: Representation and reasoning using
  temporal description logics\BBCQ\
\newblock {\Bem Data \& Knowledge Engineering}, {\Bem 22\/}(1), 1--38.

\bibitem[\protect\BCAY{Blackburn}{Blackburn}{1992}]{blackburn:92}
Blackburn, P. \BBOP1992\BBCP.
\newblock \BBOQ Fine grained theories of time\BBCQ\
\newblock In {\Bem Working Papers of the $4^{th}$ Intl. Workshop on {\em
  Semantics of Time, Space, Movement, and Spatio-Temporal Reasoning}}, \BPGS\
  299--320.

\bibitem[\protect\BCAY{Brachman, McGuiness, Patel-Schneider, Resnick, \BBA\
  Borgida}{Brachman et~al.}{1991}]{brachman:et:al:sowa-91}
Brachman, R.~J., McGuiness, D.~L., Patel-Schneider, P.~F., Resnick, L.~A.,
  \BBA\ Borgida, A. \BBOP1991\BBCP.
\newblock \BBOQ Living with {\sc classic}: When and how to use a {\sc
  kl-one}-like language\BBCQ\
\newblock In Sowa, J.\BED, {\Bem Principles of Semantic Networks}. Morgan
  Kaufmann.

\bibitem[\protect\BCAY{Buchheit, Donini, \BBA\ Schaerf}{Buchheit
  et~al.}{1993}]{buchheit:et:al:jair-93}
Buchheit, M., Donini, F.~M., \BBA\ Schaerf, A. \BBOP1993\BBCP.
\newblock \BBOQ Decidable reasoning in terminological knowledge representation
  systems\BBCQ\
\newblock {\Bem Information Systems}, {\Bem 1}, 109--138.

\bibitem[\protect\BCAY{Calvanese, Lenzerini, \BBA\ Nardi}{Calvanese
  et~al.}{1994}]{calvanese:et:al:kr-94}
Calvanese, D., Lenzerini, M., \BBA\ Nardi, D. \BBOP1994\BBCP.
\newblock \BBOQ A unified framework for class-based representation
  formalisms\BBCQ\
\newblock In {\Bem Proc.\ of the 4$^{~th}$ International Conference on
  Principles of Knowledge Representation and Reasoning}\ Bonn, Germany.

\bibitem[\protect\BCAY{Cohen, Borgida, \BBA\ Hirsh}{Cohen
  et~al.}{1992}]{borgida:et:al:aaai-92}
Cohen, W., Borgida, A., \BBA\ Hirsh, H. \BBOP1992\BBCP.
\newblock \BBOQ Computing least common subsumers in description logics\BBCQ.
\newblock \BPGS\ 754--760\ San Jose, CA.

\bibitem[\protect\BCAY{{De Giacomo} \BBA\ Lenzerini}{{De Giacomo} \BBA\
  Lenzerini}{1996}]{degiacomo:lenzerini:kr-96}
{De Giacomo}, G.\BBACOMMA\  \BBA\ Lenzerini, M. \BBOP1996\BBCP.
\newblock \BBOQ Tbox and abox reasoning in expressive description logics\BBCQ\
\newblock In {\Bem Proc.\ of the 5$^{~th}$ International Conference on
  Principles of Knowledge Representation and Reasoning}, \BPGS\ 316--327\
  Boston, MA. Morgan Kaufmann.

\bibitem[\protect\BCAY{{De Giacomo} \BBA\ Lenzerini}{{De Giacomo} \BBA\
  Lenzerini}{1995}]{degiacomo:lenzerini:ijcai-95}
{De Giacomo}, G.\BBACOMMA\  \BBA\ Lenzerini, M. \BBOP1995\BBCP.
\newblock \BBOQ What's in an aggregate: Foundations for description logics with
  tuples and sets\BBCQ\
\newblock In {\Bem Proc.\ of the 13$^{~th}$ IJCAI}\ Montreal, Canada.

\bibitem[\protect\BCAY{Dean, Firby, \BBA\ Miller}{Dean
  et~al.}{1990}]{dean:firby:miller:90}
Dean, T., Firby, J., \BBA\ Miller, D. \BBOP1990\BBCP.
\newblock \BBOQ Hierarchical planning involving deadlines, travel time and
  resources\BBCQ\
\newblock {\Bem Computational Intelligence}, {\Bem 6\/}(1).

\bibitem[\protect\BCAY{Devanbu \BBA\ Litman}{Devanbu \BBA\
  Litman}{1991}]{devanbu:litman:kr-91}
Devanbu, P.~T.\BBACOMMA\  \BBA\ Litman, D.~J. \BBOP1991\BBCP.
\newblock \BBOQ Plan-based terminological reasoning\BBCQ\
\newblock In {\Bem Proc.\ of the 2$^{~nd}$ International Conference on
  Principles of Knowledge Representation and Reasoning}, \BPGS\ 128--138\
  Cambridge, MA.

\bibitem[\protect\BCAY{Devanbu \BBA\ Litman}{Devanbu \BBA\
  Litman}{1996}]{devanbu:litman:ai-96}
Devanbu, P.~T.\BBACOMMA\  \BBA\ Litman, D.~J. \BBOP1996\BBCP.
\newblock \BBOQ Taxonomic plan reasoning\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 84}, 1--35.

\bibitem[\protect\BCAY{Devanbu, Brachman, Selfridge, \BBA\ Ballard}{Devanbu
  et~al.}{1991}]{devanbu:et:al:acm-91}
Devanbu, P., Brachman, R., Selfridge, P., \BBA\ Ballard, B. \BBOP1991\BBCP.
\newblock \BBOQ {LASSIE} -- a knowledge-based software information system\BBCQ\
\newblock {\Bem Communication of the ACM}, {\Bem 34\/}(5).

\bibitem[\protect\BCAY{Donini, Hollunder, Lenzerini, Spaccamela, Nardi, \BBA\
  Nutt}{Donini et~al.}{1992}]{donini:et:al:ai-92}
Donini, F.~M., Hollunder, B., Lenzerini, M., Spaccamela, A.~M., Nardi, D.,
  \BBA\ Nutt, W. \BBOP1992\BBCP.
\newblock \BBOQ The complexity of existential quantification in concept
  languages\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 53}, 309--327.

\bibitem[\protect\BCAY{Donini, Lenzerini, Nardi, \BBA\ Nutt}{Donini
  et~al.}{1995}]{donini:et:al:tr-95}
Donini, F.~M., Lenzerini, M., Nardi, D., \BBA\ Nutt, W. \BBOP1995\BBCP.
\newblock \BBOQ The complexity of concept languages\BBCQ\
\newblock \BTR\ RR-95-07, DFKI, Germany.
\newblock A preliminary version appears in Proc. of the $2^{nd}$ International
  Conference on Principles of Knowledge Representation and Reasoning (KR-91).

\bibitem[\protect\BCAY{Donini, Lenzerini, Nardi, \BBA\ Schaerf}{Donini
  et~al.}{1994}]{donini:et:al:jlc-94}
Donini, F.~M., Lenzerini, M., Nardi, D., \BBA\ Schaerf, A. \BBOP1994\BBCP.
\newblock \BBOQ Deduction in concept languages: from subsumption to instance
  checking\BBCQ\
\newblock {\Bem Journal of Logic and Computation}, {\Bem 4\/}(4), 423--452.

\bibitem[\protect\BCAY{Donini, Lenzerini, Nardi, Schaerf, \BBA\ Nutt}{Donini
  et~al.}{1992}]{donini:et:al:kr-92}
Donini, F.~M., Lenzerini, M., Nardi, D., Schaerf, A., \BBA\ Nutt, W.
  \BBOP1992\BBCP.
\newblock \BBOQ Adding epistemic operators to concept languages\BBCQ\
\newblock In {\Bem Proc.\ of the 3$^{~rd}$ International Conference on
  Principles of Knowledge Representation and Reasoning}, \BPGS\ 342--353\
  Cambridge, MA.

\bibitem[\protect\BCAY{Fikes \BBA\ Nilsson}{Fikes \BBA\
  Nilsson}{1971}]{fikes:nilsson:71}
Fikes, R.~E.\BBACOMMA\  \BBA\ Nilsson, N. \BBOP1971\BBCP.
\newblock \BBOQ {STRIPS}: a new approach to the application of theorem proving
  as problem solving\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 2}, 198--208.

\bibitem[\protect\BCAY{Fischer}{Fischer}{1992}]{fischer:92}
Fischer, M. \BBOP1992\BBCP.
\newblock \BBOQ The integration of temporal operators into a terminological
  representation system\BBCQ\
\newblock Kit-report~99, Technische Universtit\"at Berlin, Germany.

\bibitem[\protect\BCAY{Gerevini \BBA\ Schubert}{Gerevini \BBA\
  Schubert}{1994}]{gerevini:schubert:ai-94}
Gerevini, A.\BBACOMMA\  \BBA\ Schubert, L. \BBOP1994\BBCP.
\newblock \BBOQ On point-based temporal disjointness\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 70}, 347--361.

\bibitem[\protect\BCAY{Halpern \BBA\ Moses}{Halpern \BBA\
  Moses}{1985}]{halpern:moses:ijcai-85}
Halpern, J.~Y.\BBACOMMA\  \BBA\ Moses, Y. \BBOP1985\BBCP.
\newblock \BBOQ A guide to the modal logic of knowledge and belief: Preliminary
  draft\BBCQ\
\newblock In {\Bem Proc.\ of the 9$^{~th}$ IJCAI}, \BPGS\ 480--490\ Los
  Angeles, CA.

\bibitem[\protect\BCAY{Halpern \BBA\ Shoham}{Halpern \BBA\
  Shoham}{1991}]{halpern:shoham:91}
Halpern, J.~Y.\BBACOMMA\  \BBA\ Shoham, Y. \BBOP1991\BBCP.
\newblock \BBOQ A propositional modal logic of time intervals\BBCQ\
\newblock {\Bem Journal of ACM}, {\Bem 38\/}(4), 935--962.

\bibitem[\protect\BCAY{Heinsohn, Kudenko, Nebel, \BBA\ Profitlich}{Heinsohn
  et~al.}{1992}]{heinsohn:et:al:ijcai-93}
Heinsohn, J., Kudenko, D., Nebel, B., \BBA\ Profitlich, H. \BBOP1992\BBCP.
\newblock \BBOQ {RAT}: representation of actions using terminological
  logics\BBCQ\
\newblock \BTR, DFKI, Saarbr\"{u}cken, Germany.

\bibitem[\protect\BCAY{Hollunder \BBA\ Nutt}{Hollunder \BBA\
  Nutt}{1990}]{hollunder:nutt:dfki-90}
Hollunder, B.\BBACOMMA\  \BBA\ Nutt, W. \BBOP1990\BBCP.
\newblock \BBOQ Subsumption algorithms for concept languages\BBCQ\
\newblock \BTR\ RR-90-04, DFKI, Germany.

\bibitem[\protect\BCAY{Kautz}{Kautz}{1991}]{kautz:91}
Kautz, H.~A. \BBOP1991\BBCP.
\newblock \BBOQ A formal theory of plan recognition and its
  implementation\BBCQ\
\newblock In Allen, J.~F., Kautz, H.~A., Pelavin, R.~N., \BBA\ Tenenberg,
  J.~D.\BEDS, {\Bem Reasoning about Plans}, \BCH~2, \BPGS\ 69--126. Morgan
  Kaufmann.

\bibitem[\protect\BCAY{Lifschitz}{Lifschitz}{1987}]{lifschitz:strips:87}
Lifschitz, V. \BBOP1987\BBCP.
\newblock \BBOQ On the semantics of {\sc strips}\BBCQ\
\newblock In {\Bem The 1986 Workshop on Reasoning about Actions and Plans},
  \BPGS\ 1--10. Morgan Kaufman.

\bibitem[\protect\BCAY{{McCarthy} \BBA\ Hayes}{{McCarthy} \BBA\
  Hayes}{1969}]{McCarthy:Hayes:69}
{McCarthy}, J.\BBACOMMA\  \BBA\ Hayes, P.~J. \BBOP1969\BBCP.
\newblock \BBOQ Some philosophical problems from the standpoint of {A}rtificial
  {I}ntelligence\BBCQ\
\newblock In Meltzer, B.\BBACOMMA\  \BBA\ Michie, D.\BEDS, {\Bem Machine
  Intelligence}, \lowercase{\BVOL}~4, \BPGS\ 463--502\ Edinburgh, UK. Edinburgh
  University Press.

\bibitem[\protect\BCAY{Nebel}{Nebel}{1990}]{nebel:ai-90}
Nebel, B. \BBOP1990\BBCP.
\newblock \BBOQ Terminological reasoning is inherently intractable\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 43}, 235--249.

\bibitem[\protect\BCAY{Nebel}{Nebel}{1991}]{nebel:cycles-91}
Nebel, B. \BBOP1991\BBCP.
\newblock \BBOQ Terminological cycles: Semantics and computational
  properties\BBCQ\
\newblock In Sowa, J.~F.\BED, {\Bem Principles of Semantic Networks}, \BCH~11,
  \BPGS\ 331--362. Morgan Kaufmann.

\bibitem[\protect\BCAY{Neuwirth}{Neuwirth}{1993}]{neuwirth:93}
Neuwirth, A. \BBOP1993\BBCP.
\newblock \BBOQ Inferences for temporal object descriptions in a terminological
  representation system: Design and implementation\BBCQ\
\newblock Kit-report\ 107, Technische Universtit\"at Berlin, Germany.

\bibitem[\protect\BCAY{Pinto}{Pinto}{1994}]{pinto:phd-94}
Pinto, J.~A. \BBOP1994\BBCP.
\newblock {\Bem Temporal Reasoning in the Situation Calculus}.
\newblock Ph.D.\ thesis, Department of Computer Science, University of Toronto.

\bibitem[\protect\BCAY{Reiter}{Reiter}{1996}]{reiter:kr-96}
Reiter, R. \BBOP1996\BBCP.
\newblock \BBOQ Natural actions, concurrency and continuous time in the
  situation calculs\BBCQ\
\newblock In {\Bem Proc.\ of the 5$^{~th}$ International Conference on
  Principles of Knowledge Representation and Reasoning}\ Boston, MA.

\bibitem[\protect\BCAY{Renz \BBA\ Nebel}{Renz \BBA\
  Nebel}{1997}]{nebel:renz:97}
Renz, J.\BBACOMMA\  \BBA\ Nebel, B. \BBOP1997\BBCP.
\newblock \BBOQ On the complexity of qualitative spatial reasoning: a maximal
  tractable fragment of the region connection calculus\BBCQ\
\newblock In {\Bem Proc.\ of the 14$^{~th}$ IJCAI}, \BPGS\ 522--527\ Nagoya,
  Japan.

\bibitem[\protect\BCAY{Sandewall}{Sandewall}{1994}]{sandewall:94}
Sandewall, E. \BBOP1994\BBCP.
\newblock {\Bem Features and Fluents. The Representation of Knowledge about
  Dynamical Systems}, \lowercase{\BVOL}~I.
\newblock Oxford University Press.

\bibitem[\protect\BCAY{Sandewall \BBA\ Shoham}{Sandewall \BBA\
  Shoham}{1994}]{sandewall:shoham:ai-94}
Sandewall, E.\BBACOMMA\  \BBA\ Shoham, Y. \BBOP1994\BBCP.
\newblock \BBOQ Non-monotonic temporal reasoning\BBCQ\
\newblock In Gabbay, D.\BED, {\Bem Handbook of Artificial Intelligence and
  Logic programming}. Oxford University Press.

\bibitem[\protect\BCAY{Schaerf}{Schaerf}{1994}]{aschaerf:dke-94}
Schaerf, A. \BBOP1994\BBCP.
\newblock \BBOQ Reasoning with individuals in concept languages\BBCQ\
\newblock {\Bem Data \& Knowledge Engineering}, {\Bem 13\/}(2), 141--176.

\bibitem[\protect\BCAY{Schild}{Schild}{1991}]{schild:ijcai-91}
Schild, K.~D. \BBOP1991\BBCP.
\newblock \BBOQ A correspondence theory for terminological logics: Preliminary
  report\BBCQ\
\newblock In {\Bem Proc.\ of the 12$^{~th}$ IJCAI}, \BPGS\ 466--471\ Sidney,
  Australia.

\bibitem[\protect\BCAY{Schild}{Schild}{1993}]{schild:ijcai-93}
Schild, K.~D. \BBOP1993\BBCP.
\newblock \BBOQ Combining terminological logics with tense logic\BBCQ\
\newblock In {\Bem Proceedings of the 6$^{th}$ Portuguese Conference on
  Artificial Intelligence, EPIA'93}.

\bibitem[\protect\BCAY{Schmidt-Schau{\ss} \BBA\ Smolka}{Schmidt-Schau{\ss}
  \BBA\ Smolka}{1991}]{schmidt-schauss:smolka:ai-91}
Schmidt-Schau{\ss}, M.\BBACOMMA\  \BBA\ Smolka, G. \BBOP1991\BBCP.
\newblock \BBOQ Attributive concept descriptions with complements\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 48\/}(1), 1--26.

\bibitem[\protect\BCAY{Schmiedel}{Schmiedel}{1990}]{schmiedel:90}
Schmiedel, A. \BBOP1990\BBCP.
\newblock \BBOQ A temporal terminological logic\BBCQ\
\newblock In {\Bem Proc.\ of AAAI-90}, \BPGS\ 640--645\ Boston, MA.

\bibitem[\protect\BCAY{Smolka}{Smolka}{1992}]{smolka:jlp-92}
Smolka, G. \BBOP1992\BBCP.
\newblock \BBOQ Feature constraint logics for unification grammar\BBCQ\
\newblock {\Bem Journal of Logic Programming}, {\Bem 12}, 51--87.

\bibitem[\protect\BCAY{Tate}{Tate}{1977}]{tate:77}
Tate, A. \BBOP1977\BBCP.
\newblock \BBOQ Generating project networks\BBCQ\
\newblock In {\Bem Proc.\ of the 5$^{~th}$ IJCAI}, \BPGS\ 888--893\ Cambridge,
  MA.

\bibitem[\protect\BCAY{Ternovskaia}{Ternovskaia}{1994}]{ternovskaia:ecai-94}
Ternovskaia, E. \BBOP1994\BBCP.
\newblock \BBOQ Interval situation calculus\BBCQ\
\newblock In {\Bem Workshop Notes of the ECAI-94 Workshop ``Logic and Change"},
  \BPGS\ 153--164\ Amsterdam.

\bibitem[\protect\BCAY{{van Beek} \BBA\ Cohen}{{van Beek} \BBA\
  Cohen}{1990}]{van:Beek:90}
{van Beek}, P.\BBACOMMA\  \BBA\ Cohen, R. \BBOP1990\BBCP.
\newblock \BBOQ Exact and approximate reasoning about temporal relations\BBCQ\
\newblock {\Bem Computational Intelligence}, {\Bem 6}, 132--144.

\bibitem[\protect\BCAY{{van Beek} \BBA\ Manchak}{{van Beek} \BBA\
  Manchak}{1996}]{van:Beek:jair-96}
{van Beek}, P.\BBACOMMA\  \BBA\ Manchak, D.~W. \BBOP1996\BBCP.
\newblock \BBOQ The design and experimental analysis of algorithms for temporal
  reasoning\BBCQ\
\newblock {\Bem Journal of Artificial Intelligence Research}, {\Bem 4}, 1--18.

\bibitem[\protect\BCAY{van Dalen}{van Dalen}{1994}]{dalen:94}
van Dalen, D. \BBOP1994\BBCP.
\newblock {\Bem Logic and Structure}.
\newblock Springer-Verlag.

\bibitem[\protect\BCAY{Venema}{Venema}{1990}]{venema:90}
Venema, Y. \BBOP1990\BBCP.
\newblock \BBOQ Expressiveness and completeness of an interval tense
  logic\BBCQ\
\newblock {\Bem Notre Dame Journal of Formal Logic}, {\Bem 31\/}(4), 529--547.

\bibitem[\protect\BCAY{Weida}{Weida}{1996}]{weida:phd-96}
Weida, R. \BBOP1996\BBCP.
\newblock {\Bem Closed Terminologies and Temporal reasoning in Descriptions for
  Plan Recognition}.
\newblock Ph.D.\ thesis, Department of Computer Science, Columbia University,
  New York, NY.

\bibitem[\protect\BCAY{Weida \BBA\ Litman}{Weida \BBA\
  Litman}{1992}]{weida:litman:kr-92}
Weida, R.\BBACOMMA\  \BBA\ Litman, D. \BBOP1992\BBCP.
\newblock \BBOQ Terminological reasoning with constraint networks and an
  application to plan recognition\BBCQ\
\newblock In {\Bem Proc.\ of the 3$^{~rd}$ International Conference on
  Principles of Knowledge Representation and Reasoning}, \BPGS\ 282--293\
  Cambridge, MA.

\bibitem[\protect\BCAY{Weida \BBA\ Litman}{Weida \BBA\
  Litman}{1994}]{weida:litman:caia-94}
Weida, R.\BBACOMMA\  \BBA\ Litman, D. \BBOP1994\BBCP.
\newblock \BBOQ Subsumption and recognition of heterogeneous constraint
  networks\BBCQ\
\newblock In {\Bem Proceedings of CAIA-94}.

\bibitem[\protect\BCAY{Wilkins}{Wilkins}{1988}]{wilkins:88}
Wilkins, D. \BBOP1988\BBCP.
\newblock {\Bem Practical planning}.
\newblock Morgan Kaufmann, San Mateo CA.

\end{thebibliography}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\label{lastpage}

\end{document}

