\documentclass[10pt]{article}

\usepackage{latexsym}
\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{avier}
\usepackage{url}
\usepackage{nopageno}

\addtolength{\voffset}{-1.25cm}
\addtolength{\textheight}{2.5cm}
\addtolength{\hoffset}{-0.5cm}
\addtolength{\textwidth}{1cm}

%--------------------------------------------------------
% New Environments
%--------------------------------------------------------

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Theorem like environments 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newtheorem{theoremi}{Theorem}[section]
\newenvironment{theorem}
   {\begin{theoremi}\rm}{\end{theoremi}}

\newtheorem{definitioni}[theoremi]{Definition} 
\newenvironment{definition}
   {\begin{definitioni}\rm}{\end{definitioni}}

\newtheorem{propositioni}[theoremi]{Proposition}
\newenvironment{proposition}
   {\begin{propositioni}\rm}{\end{propositioni}}

\newtheorem{lemmai}[theoremi]{Lemma} 
\newenvironment{lemma}
   {\begin{lemmai}\rm}{\end{lemmai}}

\newtheorem{corollaryi}[theoremi]{Corollary}  
\newenvironment{corollary}
   {\begin{corollaryi}\rm}{\end{corollaryi}}

\newtheorem{claimi}[theoremi]{Claim}
\newenvironment{claim}
   {\begin{claimi}\rm}{\end{claimi}}

\newtheorem{conjecturei}[theoremi]{Conjecture} 
\newenvironment{conjecture}
   {\begin{conjecturei}\rm}{\end{conjecturei}}

\newtheorem{exercisei}[theoremi]{Exercise}
\newenvironment{exercise}
   {\begin{exercisei}\rm}{\end{exercisei}}

\newtheorem{questioni}[theoremi]{Open Question}
\newenvironment{question}
   {\begin{questioni}\rm}{\end{questioni}}

\newtheorem{conventioni}[theoremi]{Convention}
\newenvironment{convention}
   {\begin{conventioni}\rm}{\end{conventioni}}

\newtheorem{facti}[theoremi]{Fact} 
\newenvironment{fact}
   {\begin{facti}\rm}{\end{facti}}

\newtheorem{problemi}[theoremi]{Problem}
\newenvironment{problem}
   {\begin{problemi}\rm}{\end{problemi}}

\newtheorem{examplei}[theoremi]{Example}
\newenvironment{remark}
   {\begin{remarki}\rm}{\end{remarki}}

\newtheorem{remarki}[theoremi]{Remark}
\newenvironment{example}
   {\begin{examplei}\rm}{\end{examplei}}

\newtheorem{notationi}[theoremi]{Notation}
\newenvironment{notation}
   {\begin{notationi}\rm}{\end{notationi}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Non numbered environments
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Proof
\newenvironment{proof}
   {\begin{trivlist}\item[]{\sc Proof.}}
   {\hfill {\sc qed}\end{trivlist}}

% Outline of Proof
\newenvironment{outline}
   {\begin{trivlist}\item[]{\sc Outline of Proof.}}
   {\hfill {\sc qed}\end{trivlist}}

% Proof of <argument> 
\newenvironment{proofof}[1]
   {\begin{trivlist}\item[\hskip\labelsep{\sc Proof~of~{#1}.\ }]}
   {\hspace*{\fill} {\sc qed}\end{trivlist}}


% Claims and Proofs of claims inside a proof 
%
% Use claim only inside a proof and start always with claimfirst. 
% Then the claims are numbered inside the proof.

\newtheorem{claim2}{Claim}
\newenvironment{claimnext}
   {\begin{claim2}\rm}
   {\end{claim2}}
\newenvironment{claimfirst}
   {\setcounter{claim2}{0}\begin{claim2}\rm}
   {\end{claim2}} 
\newenvironment{pfclaim}
   {\begin{trivlist}\item[]{\sc Proof of Claim.}}
   {\hfill {\mbox{$\dashv$}}\end{trivlist}}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% To-be-suplied environment
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcounter{tbsnr}
\newenvironment{tbs}
{\addtocounter{tbsnr}{1}\par\bigskip \noindent\fbox{\thetbsnr}
\hspace*{\fill}\begin{minipage}{10cm}\tt}
%\typein{OPPASSEN GEBLAZEN}}
{\end{minipage}\hspace*{\fill}\bigskip}
\newcommand{\tb}[1]{\begin{tbs}{#1}\end{tbs}}


%--------------------------------------------------------
% New Commands
%--------------------------------------------------------


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Operators
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Hybrid
\newcommand{\atnom}{@}
\newcommand{\down}{\downarrow \! }

% Modal
\newcommand{\modop}{\Diamond}
\newcommand{\Modop}{\Box}

% Multimodal
\newcommand{\mmodop}[1]{\tup{#1}}
\newcommand{\Mmodop}[1]{[#1]}

% Difference
\newcommand{\dmodop}{\mathsf{D}}
\newcommand{\Dmodop}{\overline{\mathsf{D}}}

% Universal
\newcommand{\umodop}{\mathsf{E}}
\newcommand{\Umodop}{\mathsf{A}}

% Temporal
\newcommand{\fmodop}{\mathsf{F}}
\newcommand{\Fmodop}{\mathsf{G}}
\newcommand{\pmodop}{\mathsf{P}}
\newcommand{\Pmodop}{\mathsf{H}}
\newcommand{\until}{\mathsf{Until}}
\newcommand{\since}{\mathsf{Since}}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Signature, Language
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Signature
\newcommand{\NOM}{\mathsf{NOM}}
\newcommand{\ATOM}{\mathsf{ATOM}}
\newcommand{\PROP}{\mathsf{PROP}}
\newcommand{\REL}{\mathsf{REL}}
\newcommand{\SVAR}{\mathsf{SVAR}}
\newcommand{\SSYM}{\mathsf{SSYM}}
\newcommand{\sig}{\tup{\PROP,\NOM,\SVAR}}

% Language
\newcommand{\lang}{\mathcal{L}}

% Set of Propositional Symbols
\newcommand{\IP}{\mathsf{I}\hspace{-1pt}\mathsf{P}}

% Set of Propositional Symbols of a Formula
\newcommand{\IPv}[1]{\IP(#1)}

% Set of Subformulas of a Formula
\newcommand{\SF}[1]{\mathsf{SF}(#1)}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Games 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Universal Player
\newcommand{\Abelard}{$\forall$belard\xspace}

% Existential Player
\newcommand{\Eloise}{$\exists$loise\xspace}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Frames, Models, Structures
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% valuation
\newcommand{\val}{V}

% assignment
\newcommand{\ass}{g}

% denotation of a nominal
\newcommand{\den}[1]{\mathbf{#1}}

% \fram{F}{W}{R} becomes F=<W,R>
\newcommand{\fram}[3]{{\fra{#1}}=\tup{#2, #3}}

% \framk{F}{W}{R}{I} becomes F=<W,R_k>_{k \in I}
\newcommand{\framk}[4]
   {{\fra{#1}} = \tup{#2,#3_k}_{k \in #4}}

% Class of frames
\newcommand{\class}[1]{\mathsf{#1}}

% \model{M} gives you a model
\newcommand{\model}[1]{{\fra{#1}}}

% \krmod{M}{F} gives you a kripke model M over frame F
\newcommand{\krmod}[2]
   {{\fra{#1}}=\tup{{\fra{#2}},\val}}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Some Models
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\fra}[1]{{\mathfrak{#1}}}
\newcommand{\gA}{\fra{A}}
\newcommand{\gB}{\fra{B}}
\newcommand{\gC}{\fra{C}}
\newcommand{\gF}{\fra{F}}
\newcommand{\gG}{\fra{G}}
\newcommand{\gI}{\fra{I}}
\newcommand{\gL}{\fra{L}}
\newcommand{\gM}{\fra{M}}
\newcommand{\gN}{\fra{N}}
\newcommand{\gP}{\fra{P}}
\newcommand{\gR}{\fra{R}}
\newcommand{\gS}{\fra{S}}
\newcommand{\gT}{\fra{T}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Bisimulations
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Standar Bisimulation
\newcommand{\bis}{\;\underline{\leftrightarrow}\;}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Consequence and Satisfacion relations
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% forces symbol ||-
\newcommand{\forces}{\Vdash}

% models symbol |= provided by latex
%\newcommand{\models}

% theorem symbol |- 
\newcommand{\theo}{\vdash}

% Global satisfacion
\newcommand{\glomodels}{\models^*}

% Consequence Operator
\newcommand{\Cn}{\mathop{\rm Cn}} 

% Theory of a set of worlds
\newcommand{\Th}{\mathop{\rm Th}} 


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Translations
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Standard Translation
\newcommand{\ST}{\mathsf{ST}}

% Hybrid Translation
\newcommand{\HT}{\mathsf{HT}}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Special Sets
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Natural Numbers
\newcommand{\IN}{\mathbb{N}}

% Real Numbers
\newcommand{\IR}{\mathbb{R}}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Some Constructions 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Tuples \tup{x,y} = <x,y>
\newcommand{\tup}[1]{\langle #1 \rangle}

% Sets \cset{x,y} = {x,y}
\newcommand{\cset}[1]{\{ #1 \}}

% Sets with condition \csetsc{y}{xRy} = {y | xRy}
\newcommand{\csetsc}[2]{\{ #1  \; | \; #2 \}}

% Sets with domain and condition \csetc{y}{A}{xRy} = {y \in A | xRy}
\newcommand{\csetc}[3]{\{ #1 \in #2 \; | \; #3 \}}

% Double brackets
\newcommand{\dbra}[1]{[ \! [ #1 ] \! ]}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Arrows
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Named Arrow
\newcommand{\nmto}[1]{\stackrel{#1}{\to}}

% Right Zigzag morphism
\newcommand{\rzzm}{\twoheadrightarrow}
% Named Right Zigzag morphism
\newcommand{\nmrzzm}[1]{\stackrel{#1}{\rzzm}}

% Left Zigzag morphism
\newcommand{\lzzm}{\twoheadleftarrow}
% Named Left Zigzag morphism
\newcommand{\nmlzzm}[1]{\stackrel{#1}{\lzzm}}

% Injective Arrow
\newcommand{\inj}{\rightarrowtail}
% Named Injective Arrow
\newcommand{\nminj}[1]{\stackrel{#1}{\inj}}

% Surjective Arrow
\newcommand{\surj}{\twoheadrightarrow}
% Named Surjective Arrow
\newcommand{\nmsurj}[1]{\stackrel{#1}{\surj}}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Operators on classes of algebras
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\oper}[1]{\mathbf{#1}}

%subalgebras
\newcommand{\Sub}{\oper{S}}     

%homomorphic images
\newcommand{\Hom}{\oper{H}}     

%products
\newcommand{\Pro}{\oper{P}}     

%variety
\newcommand{\Var}{\oper{V}}     

%isomorphic copies
\newcommand{\Ism}{\oper{I}}     

%embedding algebras
\newcommand{\Emb}{\oper{Emb}}   


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Operators on frame classes
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%bounded morphic images
\newcommand{\Zig}{\oper{H_f}}   

%disjoint unions
\newcommand{\Dis}{\oper{P_f}}   

%generated subframes
\newcommand{\Gen}{\oper{S_f}}   


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Modal and Hybrid Languages
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\ML}[1]{\mathit{ML}(#1)}
\newcommand{\HL}[1]{\mathcal{HL}\!(#1)}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% First Order Languages
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\Lomom}{L_{\omega\omega}}
\newcommand{\Ltf}{L_{\mathit{tf}}}
\newcommand{\Ltwo}{L^2_2(v_0,v_1)}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Others
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Metalanguage existential
\newcommand{\Exists}{\exists \hspace{-0.45em} \exists}

% Metalanguage universal
\newcommand{\Forall}{\forall \hspace{-0.45em} \forall}

% Restriction of a struction to a set
\newcommand{\restr}{\upharpoonright}

% Equal by definition
\newcommand{\deq}
   {\mathrel{\stackrel{\scriptscriptstyle\mathchar"7001}{=}}}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% New Macros.

\newcommand{\mpreceq}{\preccurlyeq}
\newcommand{\ALC}{\mathcal{ALC}}
\newcommand{\ALCR}{\mathcal{ALCR}}
\newcommand{\ALCO}{\mathcal{ALCO}}
\newcommand{\FORM}{\mathsf{FORM}}
\newcommand{\myH}{\mathcal{H}}
\newcommand{\HI}{\mathcal{H}_m(\atnom\modop, \atnom)}
\newcommand{\HII}{\mathcal{H}_m(\NOM,\atnom)}
\newcommand{\HIII}{\mathcal{H}_m(\atnom\modop,\atnom,\umodop)}
\newcommand{\HIV}{\mathcal{H}_m(\NOM,\atnom,\umodop)}
\newcommand{\LHI}{\lang[\HI]}
\newcommand{\LHII}{\lang[\HII]}
\newcommand{\LHIII}{\lang[\HIII]}
\newcommand{\LHIV}{\lang[\HIV]}
\newcommand{\dd}{\!:\!}
\newcommand{\I}{\mathcal{I}}

\title{Accounting for Assertional Information}

\author{
\begin{tabular}{c}
Carlos Areces \\
\small ILLC, University of Amsterdam\\
%\small Plantage Muidergracht 24 \\
%\small 1018 TV Amsterdam, The Netherlands\\
\small \url{carlos@wins.uva.nl}\\
\small \url{http://www.illc.uva.nl/~carlos}
\end{tabular}
}

\date{}

\begin{document}
\maketitle              

%\noindent \textbf{Abstract.} In this talk we will tighten the
%connection existing between modal and description languages by
%considering hybrid logics.  Hybrid logics are modal logic extended
%with operators for explicit reference to elements in the model.  This
%new operators let us neatly account for assertional information
%(A-Boxes), a link which was missing in the original bridge between
%modal and description logic built by Schild in \cite{schi:corr91}.
%\medskip

\noindent \emph{Description logics} are specialized languages for the
representation and structuring of knowledge, specially tailored to
obtain efficient decision methods for different ``reasoning tasks.''
Nowadays, description logics are generally considered to be variations
of first-order logic---either restrictions or restrictions plus some
added operators.  These variations are mainly motivated by the
undecidability of the inference problem for first-order logic, but
also they are rooted in a desire to preserve the structure of the
knowledge being represented, and to understand a finer grained notion
of ``reasoning.''  In most description languages the knowledge about a
given situation is characterized as either

\begin{itemize} \vspace{-2pt}
\item \emph{terminological information}: definitions of
the basic and derived notions and of how they are interrelated.  This
information is ``generic'' or ``global,'' been true in every model of
the situation and of every individual in the situation.  Or\vspace{-2pt}

\item \emph{assertional information}: which record ``specific'' or
``local'' information, been true of certain particular individuals in
the situation.
\end{itemize}

\noindent All known information about a given situation is then
modeled as a pair $\tup{T,A}$, where $T$ is a set of formulas
concerning terminological information (the T-Box) and $A$ is a set of
formulas concerning assertional information (the A-Box).
\medskip


\noindent \emph{Hybrid languages} on the other hand, are extensions of
modal languages that use special atomic formulas (called
\emph{nominals}) to name states. The first hybrid languages were
introduced by Prior \cite{prio:past67} in his investigations on tense
logic. Basically, the simplest hybrid language is obtained by
extending the set of atomic symbols of the modal language with a new
sort of nominals.  Furthermore, we require that nominals are true at
exactly one state in any model.  In this way, a nominal ``names'' a
state by being true there and nowhere else.

A wide range of hybrid languages have been studied, including
different kinds of sort (paths, intervals), nominal variables which
can be bound in different ways, etc., but we will restrict ourselves
to very simple hybrid languages like the one described above.


\medskip
\noindent In this talk we explore the connection between Hybrid and
Description Languages.  It is well known that the description language
${\cal ALC}$ (see \cite{schm:attr91}) is a notational variant of
multi-modal logic (see \cite{schi:corr91}).  But this relation only
holds at the level of right hand sides of definitions in T-boxes.  A
full account of definitions is missing and, crucially, in many
applications it is often important to perform A-Box (or assertional)
reasoning as well --- that is, to reason about how concepts apply to
particular individuals.

Hybrid Logics help us fill this gap.  Building on work done in
\cite{arec:hybr99}, we will define the appropriate hybrid
logics to account for full terminological axioms and assertional
information, study notions of bisimulations to characterize the
expressive power of some of the most frequent description languages
and transfer complexity results.
\medskip    

\noindent
This is joint work with Maarten de Rijke, ILLC, University of Amsterdam.

{\small
\begin{thebibliography}{1}
\renewcommand{\itemsep}{-1pt}

\bibitem{arec:hybr99}
C.~Areces, P.~Blackburn, and M.~Marx.
\newblock Hybrid logics. {C}haracterization, interpolation and complexity.
\newblock Submitted to the {\em Journal of Symbolic Logic}, February 1999.

\bibitem{prio:past67}
A.~Prior.
\newblock {\em Past, Present and Future}.
\newblock Clarendon Press, Oxford, 1967.

\bibitem{schi:corr91}
K.~Schild.
\newblock A correspondence theory for terminological logics.
\newblock In {\em Proceedings of the 12th IJCAI}, pages 466--471, 1991.

\bibitem{schm:attr91}
M.~Schmidt-Schauss and G.~Smolka.
\newblock Attributive concept descriptions with complements.
\newblock {\em Artificial Intelligence}, 48:1--26, 1991.

\end{thebibliography}}

\end{document}

% Local Variables: 
% mode: latex
% TeX-master: t
% End: