\documentclass[11pt,twoside]{article}
\usepackage{latexsym}
\usepackage{jair}
\usepackage{theapa}
 
% \jairheading{1}{1993}{1-15}{6/91}{9/91}
\jairheading{14}{2001}{137-166}{9/00}{4/01}
\ShortHeadings{Reasoning within Fuzzy DLs}
{Straccia}
 
\firstpageno{137}
 
 
 % \newif\ifcopy
 % \copytrue   % non commentato se usare citazione
 % %\copyfalse   % non commentato se non usare citazione
 
 %\newcommand{\mycopyrightspace}[1]{%
 %    \myfootnotetext{#1}}
 
% \input{preamble}


%%%%% carlo's defs

%\parskip 6pt


%%%%%
\newcommand{\al}{\mbox{${\cal AL}$}}
\newcommand{\argon}{\mbox{\sc Argon}}


\newcommand{\wrt}{{w.r.t.}}
\newcommand{\ii}[1]{\mbox{$(#1)$}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  environment definitions
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newtheorem{thm}{Theorem}
\newtheorem{cor}{Corollary}
\newtheorem{lem}{Lemma}
\newtheorem{claim}{Claim}
\newtheorem{axiom}{Axiom}
\newtheorem{prop}{Proposition}
\newtheorem{defn}{Definition}
\newtheorem{exmp}{Example}
\newtheorem{algo}{Algorithm}


\newenvironment{pf}
{\nd {\em Proof:\/} }{ }

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  mathematical symbols definitions
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   %%%%%%%%%%%%%%%%%%
   %% General symbols
   %%%%%%%%%%%%%%%%%%
   
\def\qed{\relax\ifmmode\hskip2em \Box\else\unskip\nobreak\hskip1em
$\Box$\fi}

\newcommand{\myref}[1]{$(\ref{#1})$}

\newcommand{\ok}{\hfill $\dashv$}
\newcommand{\okdef}{ \hfill \rule{1mm}{2mm}}
\newcommand{\okproof}{ \hfill {\tt Q.E.D.} \vspace*{0.5cm}}
%\newcommand{\okex}{ \hfill \rule{2mm}{2mm}}
\newcommand{\okex}{ \hfill $\Box$}

\newcommand{\range}[2]{{[#1,#2]}}
\newcommand{\rangeg}[2]{{(#1,#2]}}


\newcommand{\lsb}{\mbox{$[\! [$}} 
\newcommand{\rsb}{\mbox{$]\! ]$}}
\newcommand{\fuzzyp}[2]{\mbox{$\langle #1 \, #2\rangle$}}
%\newcommand{\fuzzyp}[2]{\mbox{$\langle #1 , #2\rangle$}}
\newcommand{\fuzzy}[3]{\mbox{$\langle #1 #3 #2\rangle$}}
%\newcommand{\fuzzyp}[2]{\mbox{$(#1 \, #2)$}}
%\newcommand{\fuzzyp}[2]{\mbox{${#1}_{|#2}$}}
% \newcommand{\crisp}[1]{\mbox{$\overline{#1}$}}
\newcommand{\crisp}[1]{\mbox{$\sharp{#1}$}}

\newcommand{\cass}[2]{\mbox{$#1$:$#2$}}
\newcommand{\rass}[3]{\mbox{$(#1,#2)$:$#3$}}

\newcommand{\csigned}[2]{\mbox{${#1}^{#2}$}}
%\newcommand{\vcsigned}[3]{\mbox{$\langle{#1},{#3 \in #2}\rangle$}}
\newcommand{\replacein}[3]{#1\unify{#2}{#3}}



\newcommand{\fval}{\lambda}
%\newcommand{\vgen}[1]{{|#1|}}
\newcommand{\vgen}[1]{{\mu_{#1}}}
\newcommand{\vgeni}[1]{{|#1|_{\I}}}
\newcommand{\vgenv}[2]{{|#1|_{#2}}}

\newcommand{\T}{{\tt T}}
\newcommand{\NT}{{\tt N\!T}}

%%% 2 valued

\newcommand{\istruec}[2]{ {\highi{#1}(#2)} = t }
\newcommand{\isfalsec}[2]{ {\highi{#1}(#2)} = f }
\newcommand{\istruer}[3]{ {\highi{#1}(#2,#3)} = t }
\newcommand{\isfalser}[3]{ {\highi{#1}(#2,#3)} = f }
\newcommand{\exthighi}[1]{\lsb {#1}^{\cal I}\rsb}

%%%%%

%\newcommand{\defs}{\stackrel{\rm def.}{=}}
\newcommand{\defs}{=_{\mu}}

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

   %%%%%%%%%%%%%%%%%%
   %% DL syntax:
   %%%%%%%%%%%%%%%%%%
   
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

      %%%%%%%%%%%%%%%%%%
      %% DL operators:
      %%%%%%%%%%%%%%%%%%
%\subsection{DL operators}
      
\newcommand{\andc}{\sqcap}
\newcommand{\all}{\forall}
\newcommand{\some}{\exists}
\newcommand{\notc}{\neg}
\newcommand{\orc}{\sqcup}
\newcommand{\csome}{\exists}
\newcommand{\sing}[1]{\{ #1 \}}
\newcommand{\oneof}[1]{\{ #1 \}}
\newcommand{\bottomc}{\perp}
\newcommand{\topc}{\top}
\newcommand{\notr}{\neg}
\newcommand{\compr}{\circ}
% \newcommand{\impc}{\Rightarrow}

\newcommand{\impc}{\mbox{$<\!\!\!\cdot$}}


%\newcommand{\impcf}{\mapsto}
% \newcommand{\impcf}{\mbox{\raisebox{.6ex}{{\tiny \, $\sim$}}}{\, \! \! \! \! \! \to}}
% \newcommand{\impcf}{\mbox{\raisebox{.27ex}{{\tiny \, $\sim$}}}{\, \! \! 
% \! \! \! \impc}}

\newcommand{\impcf}{\mbox{$\prec\!\!\!\cdot$}}

\newcommand{\defc}{\colon =}
% \newcommand{\defc}{\Leftrightarrow}

\newcommand{\defcf}{\colon \! \approx}

% \newcommand{\defcf}{\, \mbox{\raisebox{.27ex}{{\tiny $\sim$}}}{\! 
% \! \! \! \! \!  \: {\defc}}}

\newcommand{\hornc}{\Leftarrow}
% \newcommand{\horncf}{\leftarrow}
\newcommand{\horncf}{\mbox{\raisebox{.27ex}{{\tiny \ \ $\sim$}}}{\, \! \! \! 
\! \! \! \hornc}}


%\newcommand{\impc}{\sqsubseteq}

%\newcommand{\andc}{\andf}
%\newcommand{\all}{\forall}
%\newcommand{\some}{\exists}
%\newcommand{\notc}{\notf}
%\newcommand{\orc}{\orf}
%\newcommand{\csome}{\exists}
%\newcommand{\sing}[1]{\{ #1 \}}
%\newcommand{\oneof}[1]{\{ #1 \}}
%\newcommand{\bottomc}{\perp}
%\newcommand{\topc}{\top}
%\newcommand{\notr}{\notf}
%\newcommand{\compr}{\circ}


\newcommand{\andf}{\wedge}
\newcommand{\orf}{\vee}
%\newcommand{\notf}{\sim}
\newcommand{\notf}{\neg}
\newcommand{\impf}{\rightarrow}

\newcommand{\CL}{\mbox{\tt Cl}}

\newcommand{\subc}{\sqsubseteq}
\newcommand{\subr}{\sqsubseteq}
%\newcommand{\subt}{\sqsubseteq}
\newcommand{\subt}{\Rightarrow}


\newcommand{\primdef}{\mbox{$\ < \! \! \! \cdot \ $}} 
\newcommand{\eqd}{\stackrel {.}{=}}

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

      %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
      %% DL syntactical relational symbols:
      %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


% \newcommand{\KB}{{\mathcal{K}}}
% \newcommand{\KB}{{\Sigma}}
\newcommand{\KB}{{K}}
\newcommand{\FKB}{{\Sigma}}
%\newcommand{\ass}{{\mbox{$\mathcal{A}$}}}
\newcommand{\ass}{{\mbox{$\alpha$}}}
%\newcommand{\spec}{{\mbox{$\mathcal{T}$}}}
\newcommand{\spec}{{\mbox{$\tau$}}}
\newcommand{\assf}{{\mbox{$\psi$}}}
% \newcommand{\specf}{{\mbox{$\tau$}}}

\newcommand{\specf}{\tilde{\tau}}


\newcommand{\cons}{{\mbox{$\alpha$}}}
\newcommand{\consf}{{\mbox{$\psi$}}}

  
\newcommand{\GDL}{\vdash}
\newcommand{\weakproof}{\mbox{$|\!\!\!\sim$}}    

\newcommand{\ruleA}{$(A)$}
\newcommand{\ruleBa}{$(B1)$} 
\newcommand{\ruleBb}{$(B2)$}
\newcommand{\rulePB}{$(PB)$}


\newcommand{\unify}[2]{[#1/#2]}


%%%%%

%\newcommand{\notrule}{\rightarrow_{\notc}}
%\newcommand{\andrule}{\rightarrow_{\andc}}
%\newcommand{\orrule}{\rightarrow_{\orc}}
%\newcommand{\existsrule}{\rightarrow_{\csome}}
%\newcommand{\allrule}{\rightarrow_{\all}}
%\newcommand{\unifyrule}{\rightarrow_{[/]}}

\newcommand{\notrule}{{\notc}}
\newcommand{\andrule}{{\andc}}
\newcommand{\orrule}{{\orc}}
\newcommand{\existsrule}{{\csome}}
\newcommand{\allrule}{{\all}}
%\newcommand{\unifyrule}{\rightarrow_{[/]}}

\newcommand{\imprule}{{\impcf}}
\newcommand{\hornrule}{{\horncf}}


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

   %%%%%%%%%%%%%%%%%%
   %% DL semantics:
   %%%%%%%%%%%%%%%%%%

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

      %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
      %% DL semantical relational symbols:
      %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\subs}{\sqsubseteq}
\newcommand{\subsf}{\preceq}
% \newcommand{\subs}{\preceq}

%\newcommand{\subsT}{\sqsubseteq_{T} }
%\newcommand{\tsubsT}{\sqsubseteq_{T}^{t} }
%\newcommand{\fsubsT}{\sqsubseteq_{T}^{f} }

\newcommand{\weakmod}{\mbox{$|\!\!\!\approx$}}
\newcommand{\crispentail}{\mbox{$|\!\!\!\equiv$}}

\newcommand{\entail}{\models}
\newcommand{\notentail}{\not \!\! \entail}
\newcommand{\entailfunc}{\models_{(\cdot)}}
\newcommand{\entailffunc}{\weakmod_{(\cdot)}}
\newcommand{\entailf}{\weakmod}
\newcommand{\notentailf}{\,\mbox{$\not \!\! \entailf$}}
\newcommand{\entailfv}{\models_{4}}
\newcommand{\entailtv}{\models_{2}}


\newcommand{\equivf}{\cong}

\newcommand{\truef}[1]{ {t \in \highi{#1}} }
\newcommand{\falsef}[1]{ {f \in \highi{#1}} }
\newcommand{\nottruef}[1]{ {t \not \in \highi{#1}} }
\newcommand{\notfalsef}[1]{ {f \not \in \highi{#1}} }
\newcommand{\emptyf}[1]{ {\highi{#1} = \emptyset} }
\newcommand{\notemptyf}[1]{ {\highi{#1} \neq \emptyset} }


 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  useful macros
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
   %%%%%%%%%%%%%%%%%%
   %% General macros
   %%%%%%%%%%%%%%%%%%     
     
\newcommand{\tvdash}[1]{\leadsto_{#1}} 
\newcommand{\dD}[1]{{\bf #1}}

\newcommand{\tuplett}[2]{(#1, #2)}
\newcommand{\tuplettt}[3]{(#1, #2, #3)}
\newcommand{\tupletttt}[4]{(#1, #2, #3, #4)}
 
\newcommand{\bfl}{\begin{flushleft}}
\newcommand{\efl}{\end{flushleft}}

\newcommand{\ie}{{\em i.e.}}
\newcommand{\eg}{{\em e.g.}}

\newcommand{\stringproof}{\underline{{\em Proof:\/}} \mbox{ \ }}

\newcommand{\myvskip}{\vspace{2em}}  
  
%\newif\iftodo
%\todofalse    % do print todo stuff
%\todotrue     % do not print todo stuff

\newcommand{\todo}[1]
{\iftodo 
  \vspace{0ex} 
  \fbox{\parbox{\textwidth}{#1}} 
  \vspace{0ex} 
  \noindent 
\else{}
\fi}  

%\newif\ifinputMac
%\inputMactrue    % if true then load file from Mac OS
%\inputMacfalse   % if false then load file from Unix OS

%\newcommand{\inputMac}[2]
%{\ifInputMac 
%  {#1} 
% \else{#2}
%\fi}  


\newcommand{\comment}[1]
{\iftodo 
  \vspace{0ex} 
    \begin{center}
      \fbox{\parbox{\textwidth}{#1}} 
    \end{center} 
    \vspace{0ex} 
    \noindent
\else{}
\fi}

\newcommand{\nd}{\noindent}

%\def\picture #1 by #2 (#3){
%  \vbox to #2{
%    \hrule width #1 height 0pt depth 0pt
%    \vfill
%    \special{picture #3} % this is the low-level interface
%    }
%  }

%\def\scaledpicture #1 by #2 (#3 scaled #4){{
%  \dimen0=#1 \dimen1=#2
%  \divide\dimen0 by 1000 \multiply\dimen0 by #4
%  \divide\dimen1 by 1000 \multiply\dimen1 by #4
%  \picture \dimen0 by \dimen1 (#3 scaled #4)}
%  }

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
     
      %%%%%%%%%%%%%%%%%%%%%%%%%%%%
      %% DL macros for syntax:
      %%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\Oplus}{{\Os} \cup \{ \Qp \}}
\newcommand{\Os}{{\cal O}}
\newcommand{\V}{{\cal V}}
\newcommand{\Ob}{{\cal O}^{+}}
\newcommand{\Abox}{{\cal A}}
\newcommand{\Tbox}{{\cal T}}
\newcommand{\GKB}{{\Sigma}}


\newcommand{\sequent}[2]{#1 \rightarrow #2}

\newcommand{\ruleal}[3]
{ \raisebox{2ex}[0pt][0pt]{{\scriptsize #1 }   }
\begin{tabular}[b]{c}
   $#2$ \\ \hline
   $#3$
\end{tabular}
}

\newcommand{\rulebl}[4]
{ \raisebox{2ex}[0pt][0pt]{{\scriptsize #1 }   }   
\begin{tabular}[b]{c|c}
\multicolumn{2}{c}{$#2$} \\ \hline
   $#3$ & $#4$ 
\end{tabular}
}

\newcommand{\rulear}[3]
{ 
\begin{tabular}[b]{c}
   $#2$ \\ \hline
   $#3$
\end{tabular}
\raisebox{2ex}[0pt][0pt]{  {\scriptsize #1 }}
}

\newcommand{\rulebr}[4]
{ 
\begin{tabular}[b]{c|c}
\multicolumn{2}{c}{$#2$} \\ \hline
   $#3$ & $#4$  
\end{tabular}
 \raisebox{2ex}[0pt][0pt]{  {\scriptsize #1}}
}
     

%%% four-valued %%%%%

\newcommand{\KBfv}[1]{#1}
\newcommand{\GfvKB}{\Sigma}
\newcommand{\GfvIKB}[1]{{\Sigma}_{#1}}
\newcommand{\GfvQ}{{Q}}
\newcommand{\GS}{{\GfvKB}}

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

      %%%%%%%%%%%%%%%%%%%%%%%%%%%%
      %% DL macros for semantics:
      %%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\I}{{\cal I}}
\newcommand{\tI}{\tilde{{\cal I}}}
\newcommand{\J}{{\cal J}}
\newcommand{\W}{{\cal W}}
\newcommand{\tT}{\tilde{T}}

\newcommand{\highi}[1]{{#1}^{\cal I} }
\newcommand{\highv}[2]{{#1}^{#2} }
%\newcommand{\poshighi}[1]{{#1}^{\cal I}_{+} }
%\newcommand{\neghighi}[1]{{#1}^{\cal I}_{-} }
\newcommand{\poshighi}[1]{\lsb{#1}^{\cal I}\rsb^{+} }
\newcommand{\neghighi}[1]{\lsb{#1}^{\cal I}\rsb^{-} }
\newcommand{\genhighi}[1]{\lsb{#1}^{\cal I}\rsb }

%\newcommand{\vhighi}[2]{{\cal I}_{#1}^{#2} }
%\newcommand{\varhighi}[3]{{#1}^{{\cal I}_{#2}^{#3}} }
\newcommand{\vhighi}[2]{\lsb{#1}^{#2}\rsb^{+} }
\newcommand{\varhighi}[3]{\lsb{#1}^{#2}\rsb^{-} }

\newcommand{\inDI}[2]{ {#1 \in \highi{#2}} }
\newcommand{\notinDI}[2]{ {#1 \not \in \highi{#2}} }
\newcommand{\inDvI}[4]{ {#1 \in \varhighi{#2}{#3}{#4}} }
\newcommand{\notinDvI}[4]{ {#1 \not \in \varhighi{#2}{#3}{#4}} }

\newcommand{\truec}[2]{ {t \in \highi{#1}(#2)} }
\newcommand{\falsec}[2]{ {f \in \highi{#1}(#2)} }
\newcommand{\truer}[3]{ {t \in \highi{#1}(#2,#3)} }
\newcommand{\falser}[3]{ {f \in \highi{#1}(#2,#3)} }
\newcommand{\nottruec}[2]{ {t \not \in \highi{#1}(#2)} }
\newcommand{\notfalsec}[2]{ {f \not \in \highi{#1}(#2)} }
\newcommand{\nottruer}[3]{ {t \not \in \highi{#1}(#2,#3)} }
\newcommand{\notfalser}[3]{ {f \not \in \highi{#1}(#2,#3)} }
\newcommand{\emptyc}[2]{ {\highi{#1}(#2) = \emptyset} }
\newcommand{\emptyr}[3]{ {\highi{#1}(#2,#3) = \emptyset} }
\newcommand{\notemptyc}[2]{ {\highi{#1}(#2) \neq \emptyset} }
\newcommand{\notemptyr}[3]{ {\highi{#1}(#2,#3) \neq \emptyset} }

\newcommand{\vtruec}[3]{ {t \in \highv{#1}{#2}(#3)} }
\newcommand{\vfalsec}[3]{ {f \in \highv{#1}{#2}(#3)} }
\newcommand{\vtruer}[4]{ {t \in \highv{#1}{#2}(#3,#4)} }
\newcommand{\vfalser}[4]{ {f \in \highv{#1}{#2}(#3,#4)} }
\newcommand{\vnottruec}[3]{ {t \not \in \highv{#1}{#2}(#3)} }
\newcommand{\vnotfalsec}[3]{ {f \not \in \highiv{#1}{#2}(#3)} }
\newcommand{\vnottruer}[4]{ {t \not \in \highv{#1}{#2}(#3,#4)} }
\newcommand{\vnotfalser}[4]{ {f \not \in \highv{#1}{#2}(#3,#4)} }
\newcommand{\vemptyc}[3]{ {\highv{#1}{#2}(#3) = \emptyset} }
\newcommand{\vemptyr}[4]{ {\highv{#1}{#2}(#3,#4) = \emptyset} }
\newcommand{\vnotemptyc}[3]{ {\highv{#1}{#2}(#3) \neq \emptyset} }
\newcommand{\vnotemptyr}[4]{ {\highv{#1}{#2}(#3,#4) \neq \emptyset} }

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  commonly used names
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\section{commonly used names}

\newcommand{\almirtl}{${\cal ALENO}_{1}{\cal R}^{-1}$}
\newcommand{\alesrinv}{${\cal ALEO}_{1}{\cal R}^{-1}$}
\newcommand{\alcfv}{${\cal ALC}_{4}$}
\newcommand{\alc}{${\cal ALC}$}
\newcommand{\alcp}{${\cal ALC}^+$}
\newcommand{\alco}{${\cal ALCO}$}

\newcommand{\alcfvc}{$\mbox{}^{*}\!{\cal ALC}_{4}^{c}$}
\newcommand{\alcc}{${\cal ALC}^{c}$}
\newcommand{\alcmir}{${\cal AL}{\tt MIR}$}


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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  style parameters
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\setarraystretch}{\renewcommand{\arraystretch}{1.5}}
\newcommand{\resetarraystretch}{\renewcommand{\arraystretch}{1.0}}

\newcommand{\setarrayrow}[1]{\renewcommand{\arraystretch}{#1}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%  END OF PREAMBLE
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


 
\newif\iftodo
% \todofalse    % do print todo stuff
\todotrue     % do not print todo stuff

 
 %---------------------------------------------------------------------------
 
\title{Reasoning within 
         Fuzzy Description Logics}  
  
     \author{\name Umberto Straccia \email straccia@iei.pi.cnr.it \\
             \addr I.E.I - C.N.R.,  Via G. Moruzzi, 1 \\
             I-56124 Pisa (PI), ITALY}
			 
\begin{document}
 
 \maketitle

%%%%%%% abstract %%%%%%%%

\begin{abstract}
Description Logics (DLs) are suitable, well-known, logics for managing 
structured knowledge.  They allow reasoning about individuals and well 
defined concepts, \ie~set of individuals with common properties.  The 
experience in using DLs in applications has shown that in many cases 
we would like to extend their capabilities.  In particular, their use 
in the context of Multimedia Information Retrieval (MIR) leads to the 
convincement that such DLs should allow the treatment of the inherent 
imprecision in multimedia object content representation and retrieval.

In this paper we will present a fuzzy extension of \alc, combining 
Zadeh's fuzzy logic with a classical DL. In particular, concepts 
becomes fuzzy and, thus, reasoning about imprecise concepts is 
supported.  We will define its syntax, its semantics, describe its 
properties and present a constraint propagation calculus for reasoning 
in it.
\end{abstract}

%\tableofcontents

%------------------------------ INTRODUCTION -------------------

\section{Introduction}

The representation of uncertainty and imprecision has received a 
considerable attention in the Artificial Intelligence community in an 
attempt to extend existing knowledge representation systems to deal 
with the imperfect nature of real world information (which is likely 
the rule rather than an exception).  An impressive work has been 
carried out in the last decades, resulting in a number of concepts 
being investigated, a number of problems being identified and a number 
of solutions being developed \cite{Bacchus90,Dubois96,Kruse91,Pearl88}.

For most knowledge representation formalisms, First-Order Logic (FOL) 
has been the basis: its basic units --individuals, their properties, 
and the relationship between them-- naturally capture the way in which 
people encode their knowledge.  Unfortunately, it is severely limited 
both \ii{i} by its ability to represent our uncertainty about the 
world --due to lack of knowledge about the real world a fact can 
only estimated to be true to \eg\ a probability degree; 
and \ii{ii} by its ability to represent inherently imprecise 
knowledge--indeed, there are concepts, like hot, for which no exact 
definition exists and, thus, a fact like ``$35^{\circ}$ Celsius is 
hot", rather being true or false, has a truth-value in between true 
and false.

In the last decade a substantial amount of work has been carried out 
in the context of {\em Description Logics} (DLs).\footnote{Description 
Logics have also been referred to as Terminological Logics, Concept 
Logics, KL-ONE-like languages.  The web page of the description logic 
community is found at address {\tt http://dl}{\tt.kr.org/dl}.}  DLs 
are a logical reconstruction of the so-called frame-based knowledge 
representation languages, with the aim of providing a simple 
well-established Tarski-style declarative semantics to capture the 
meaning of the most popular features of structured representation of 
knowledge.  A main point is that DLs are considered as to be 
attractive logics in knowledge based applications as they are a good 
compromise between expressive power and computational complexity.

Nowadays, a whole family of knowledge representation systems has been 
build using DLs, which differ with respect to their expressiveness, 
their complexity and the completeness of their algorithms, and they 
have been used for building a variety 
of applications \cite{Peltason91,Brachman92,Baader91d,Horrocks98}.

Experience in using DLs in applications has also shown that in many 
cases we would like to extend the representational and reasoning 
capabilities of them.  In particular, the use of DLs in the context of 
Multimedia Information Retrieval (MIR) points out the necessity of 
extending DLs with capabilities which allow the treatment of the 
inherent imprecision in multimedia object representation and retrieval 
\cite{Meghini96,Meghini97b,Meghini98a}.  In fact, classical DLs are 
insufficient for describing {\em real} multimedia retrieval 
situations, as the retrieval is usually not only a yes-no question: 
\ii{i} the representations of multimedia objects' content and queries 
which the system (and the logic) have access to are inherently 
imperfect; and \ii{ii} the relevance of a multimedia object to a query 
can thus be established only up to a limited degree.  Because of this, 
we need a logic in which, rather than deciding {\it tout court} 
whether a multimedia object satisfies a query or not, we are able to 
{\em rank} the retrieved objects according to how strongly the system 
believes in their relevance to a query.

To this end, we will extend DLs with \emph{fuzzy} capabilities.  The 
choice of fuzzy set theory as a way of endowing a DL with the 
capability to deal with imprecision is not uncommon 
\cite{daSilva94,Tresp98,Yen91a} and can be motivated

\begin{itemize}
\item
from a semantics point of view, as fuzzy logics capture the notion of 
imprecise concept, \ie~a concept for which a clear and precise 
definition is not possible.  Fuzzy concepts play a key role in 
\eg~content descriptions of multimedia objects (most of human's 
concepts are imprecise).  For instance, in the context of images, the 
(semantic) content of an image region $r$ may be described by means of 
a fuzzy statement like ``$r$ is about a Ferrari'' and establish that this 
sentence has truth-value $0.8$, \ie\ $r$ is likely about a Ferrari;
\item
from a proof theoretical point of view, as there exist well-known techniques for
reasoning in fuzzy logics \cite{ChenJ96,Lee72,Xiaochun95}. 

% This is not the case for
% alternative logics, such as, for instance, probabilistic
% DLs~\cite{Heinsohn94,Jager94,Sebastiani94a} (exception is \cite{}). In
% particular,~\cite{Halpern90} shows that probabilistic reasoning is
% computationally more difficult than non-probabilistic reasoning, and in most
% cases a complete axiomatization is missing . This will not be our case.
\end{itemize}

\nd In the following we will present a quite general fuzzy DL, in the 
sense that it is based on the DL \alc, a significant and expressive 
representative of the various DLs.  This allows us to adapt it easily 
to the different DLs presented in the literature.  Another important 
point is that we will show that the additional expressive power has no 
impact from a computational complexity point of view.  This is 
certainly important as the nice trade-off between computational 
complexity and expressive power of DLs contributes to their 
popularity.

Note that our fuzzy extension for the management of imprecise 
knowledge is complementary to other DL extensions for the management 
of uncertainty, \eg\ probabilistic extension 
\cite{Heinsohn94,Jager94,Koller97,Sebastiani94a} with some exceptions 
like shown by Hollunder (1994) %\cite{Hollunder94} 
where a possibilistic DL has been considered.  
Even though these probabilistic extensions enlarge the applicability 
of DLs they do not address the issue of reasoning about individuals 
and imprecise concepts, as imprecise knowledge and uncertain knowledge 
are ``orthogonal'' \cite{Dubois94a}.  Moreover, reasoning in a 
probabilistic framework is generally a harder task, from a 
computational point of view, than the relative non probabilistic case 
and in most cases a complete axiomatization is missing 
\cite{Halpern90,Roth96}.  As a consequence, the computational problems 
have to be addressed carefully \cite{Koller97}.

We will proceed as follows.  In the following section we first 
introduce \alc.  In Section~\ref{dlf} we extend \alc \ to the fuzzy 
case and discuss some properties in Section~\ref{pr}, while in 
Section~\ref{decalc} we will present a constraint propagation calculus 
for reasoning in it.  Section~\ref{concl} concludes and presents some 
topics for further research.

% The following work substantially extends and modifies 
% \cite{Straccia98} both from a semantics and algorithms point of view.


%------------------------------ FUZZY DESCRIPTION LOGICS -------

\section{A Quick Look to \alc}

\nd The specific DL we will extend with fuzzy capabilities is \alc, a 
significant representative of DLs.  At first, we will introduce 
classical \alc, while in Section \ref{dlf} our fuzzy extension of \alc 
\ will be presented.

We assume three alphabets of symbols, called {\em primitive concepts} 
(denoted by $A$), {\em primitive roles} (denoted by $R$) and {\em 
individuals} (denoted by $a$ and $b$).\footnote{Through this work we 
assume that every metavariable has an optional subscript or 
superscript.}

% \paragraph{Concept and Role:}
\subsection{Concept and Role}
Concepts are expressions that collect the properties, described by 
means of roles, of a set of individuals.  From a FOL point of view, 
concepts can be seen as unary predicates, whereas roles are 
interpreted as binary predicates.

A {\em concept} (denoted by $C$ or $D$)  of the language
\alc \  is build out of primitive concepts according to the following syntax
rules:   
 
\[  
\begin{array}{ccrl}  
C,D & \longrightarrow 
 & \topc     |     &  \mbox{(top concept)} \\
&& \bottomc  |     &  \mbox{(bottom concept)} \\
&& A         |     &  \mbox{(primitive concept)} \\  
&& C \andc D |     &  \mbox{(concept conjunction)} \\  
&& C \orc D  |     &  \mbox{(concept disjunction)} \\  
&& \notc C   |     &  \mbox{(concept negation)} \\  
&& \all R.C  |     &  \mbox{(universal quantification)} \\   
&& \csome R.C      &  \mbox{(existential quantification)} .  
\end{array}  
\] 

% \paragraph{Interpretation:}
\subsection{Interpretation}
DLs have a clean, model-theoretic semantics, based on the
notion of interpretation. An {\em interpretation} $\I$ is a pair 
$\I = (\highi{\Delta}, \highi{\cdot})$ consisting of
a non empty set $\highi{\Delta}$ (called the {\em domain}) and of an
{\em interpretation function\/} $\highi{\cdot}$ mapping different
individuals into different elements of $\highi{\Delta}$ (called {\em 
unique name assumption}), primitive concepts into subsets of $\highi{\Delta}$ and 
primitive roles into subsets of  $\highi{\Delta} \times \highi{\Delta}$. 
The interpretation of complex concepts is defined as usual:

\[
\begin{array}{rcl}  
\highi{\topc} &  = & \highi{\Delta} \\
\highi{\bottomc} & = & \emptyset \\
\highi{(C \andc D)} & = & 
    \highi{C} \cap
    \highi{D}\\ 
\highi{(C \orc D)} & = & 
    \highi{C} \cup
    \highi{D} \\ 
\highi{(\notc C)} & = & \highi{\Delta} \setminus \highi{C} \\ 
\highi{(\forall R.C)} & = &  
\{ d \in \highi{\Delta} : \forall d'.
 (d,d')  \not \in \highi{R} \mbox{ or } d' \in \highi{C}\} \\ 
\highi{(\exists R.C)} & = & 
  \{ d \in \highi{\Delta} :  \exists d'.
 (d,d')  \in \highi{R}  \mbox{ and } d' \in \highi{C}\} .
\end{array}
\]

\nd
Note that each concept $C$ and role $R$ can be mapped into 
an equivalent open first-order formula $F_C(x)$ and 
$F_R(x,y)$, respectively:

\begin{eqnarray}
F_{\topc}(x)         & = & {\sf T} \label{foltrue} \\ 
F_{\bottomc}(x)      & = & {\sf F} \label{folfalse} \\ 
F_A(x)            & = & A(x) \label{folatomic} \\
F_R(x,y)          & = & R(x,y) \label{folrole} \\
F_{C \andc D}(x)  & = & F_C(x) \andf F_D(x) \label{foland} \\
F_{C \orc D}(x)   & = & F_C(x) \orf F_D(x) \label{folor} \\
F_{\notc C}(x)    & = & \notf F_C(x) \label{folnot} \\
F_{\all R.C}(x)   & = & \forall y. \notf F_R(x,y) \orf F_C(y) \label{folall} \\
F_{\csome R.C}(x) & = & \exists y. F_R(x,y) \andf F_C(y)  \label{folcsome},
\end{eqnarray}

\nd
where {\sf T} and {\sf F} are two formulae representing the truth-value ``true" and ``false",
respectively (\eg~${\sf T} = p \orf \notf p$ and ${\sf F} = p \andf \notf p$, for some letter
$p$).

Two concepts $C$ and $D$ are said to be 
{\em equivalent} (denoted by $C \equiv D$) when $\highi{C} = \highi{D}$ for all interpretations
$\cal I$. Note that, \eg~$\topc \equiv \neg\bottomc$; $C \andc D \equiv \notc (\notc C \orc \neg D)$,
and $(\csome R.C) \equiv (\neg\all R.\neg C)$.

% \paragraph{Assertion:}
\subsection{Assertion}
An {\em assertion} (denoted by $\ass$) is an expression of type 
$\cass{a}{C}$ (``$a$ is $C$'', also ``$a$ is an instance of $C$''), or 
an expression of type $\rass{a}{b}{R}$ (``$(a,b)$ is $R$'', also 
``$(a,b)$ is an instance of $R$'').  For instance, \cass{\sf tom}{\sf 
Tall \andc Student} asserts that Tom is a tall student, whereas 
\rass{\sf tim}{\sf tom}{{\sf Friend}} asserts that Tom is a friend of 
Tim.  A \emph{primitive assertion} is either an assertion of the form 
$\cass{a}{A}$, where $A$ is a primitive concept, or an assertion of 
the form $\rass{a}{b}{R}$.  From a semantics point of view, an 
interpretation $\I$ {\em satisfies} $\cass{a}{C}$ (resp.\ 
$\rass{a}{b}{R}$) iff $\highi{a} \in \highi{C}$ (resp.\ $ 
(\highi{a},\highi{b}) \in \highi{R}$).


% \paragraph{Terminological Axiom}
\subsection{Terminological Axiom}
A \emph{terminological axiom} (denoted by $\spec$) is either a concept 
specialisation or a concept definition.  A {\em concept 
specialisation} is an expression of the form $A \impc C$, where $A$ is 
a primitive concept and $C$ is a concept.  A specialisation allows 
stating the existence of a specialisation (``more specific than'') 
relation between concepts.  For instance, ${\sf Ferrari} \impc {\sf 
SportCar} \andc \csome {\sf Ownedby}.{\sf CarFanatic}$ states that a 
Ferrari is a sport car that is owned by a car fanatic.  On the other 
hand, a \emph{concept definition} is an expression of the form $A \defc 
C$, where $A$ is a primitive concept and $C$ is a concept.  A concept 
definition allows stating the equivalence between concepts.  For 
instance, ${\sf Tennis} \defc {\sf SportKind} \andc (\csome {\sf 
HasSportTool}.\topc) \andc (\all {\sf HasSportTool}.{\sf 
TennisRacket})$ states that tennis is identified by a kind of sport 
having a tennis racket as a sport tool.  From a semantics point of view, 
an interpretation $\I$ {\em satisfies} a concept specialisation $A 
\impc C$ iff $\highi{A} \subseteq \highi{C}$.  Similarly, an 
interpretation $\I$ {\em satisfies} a concept definition $A \defc C$ 
iff $\highi{A} = \highi{C}$.

% \paragraph{Knowledge Base, Entailment and Subsumption:}
\subsection{Knowledge Base, Entailment and Subsumption}
A finite set $\KB$ of assertions and terminological axioms will be called a 
{\em Knowledge Base} (KB).  With $\KB_A$ we will denote the set of 
assertions in $\KB$, whereas with $\KB_T$ we will denote the set 
of terminological axioms in $\KB$, also called a \emph{terminology}.  
A KB $\KB$ is {\em purely assertional} if $\KB_T = \emptyset$.  
Further, we will assume that a terminology $\KB_T$ is such that no 
concept $A$ appears more than once on the left hand side of a 
terminological axiom $\spec \in \KB_T$ and that no cyclic 
definitions are present in $\KB_T$.\footnote{We will say that $A$ 
{\em directly uses} primitive concept $B$ in $\KB_T$, if there is 
$\spec \in \KB_T$ such that $A$ is on the left hand side of 
$\spec$ and $B$ occurs in the right hand side of $\spec$.  Let {\em 
uses} be the transitive closure of the relation directly uses in 
$\KB_T$.  $\KB_T$ is {\em cyclic} iff there is $A$ such that 
$A$ uses $A$ in $\KB_T$.} 

We will say that an interpretation $\I$ {\em satisfies} ({\em is a 
model of}\/) a KB $\KB$ iff $\I$ satisfies each element in $\KB$.  A 
KB $\KB$ {\em entails} an assertion $\ass$ (denoted by $\KB \entail 
\ass$) iff every model of $\KB$ also satisfies $\ass$.  Furthermore, 
let $\KB_{T}$ be a terminology and let $C,D$ be two concepts.  We 
will say that $D$ \emph{subsumes} $C$ with respect to (w.r.t.) $\KB_{T}$ 
(denoted by $C \subs_{\KB_{T}} D$) iff for every model $\I$ of 
$\KB_{T}$, $\highi{C} \subseteq \highi{D}$ holds.

The problem of determining whether $\KB \entail \ass$ is called {\em 
entailment problem}; the problem of determining whether $C 
\subs_{\KB_{T}} D$ is called {\em subsumption problem}; and the 
problem of determining whether $\KB$ is satisfiable is called {\em 
satisfiability problem}.


It is well known \cite{Buchheit93,Donini94c,Nebel90a} that  in \alc

\begin{eqnarray}
	\KB \entail \rass{a}{b}{R} & \mbox{iff} &  \rass{a}{b}{R} \in \KB   
	\label{pb8} \\
	\KB \entail \cass{a}{C} & \mbox{iff} & \KB \cup \{\cass{a}{\notc C}\} \mbox{ is not satisfiable}  
	\label{pbb8} \\
	C \subs_{\emptyset} D & \mbox{iff} & \cass{a}{C} \entail \cass{a}{D}, \mbox{ for a new $a$}
	\label{pbb7} \\
	C \subs_{\KB_{T}} D & \mbox{iff} & C' \subs_{\emptyset} D' 
	\label{pb7}
\end{eqnarray}

\nd where $C'$ and $D'$ are build from $C$ and $D$ by expanding the 
terminology $\KB_{T}$ to $\KB_{T}''$ and substituting every primitive 
concept occurring in $C$ or $D$, which is defined in $\KB_{T}''$, with 
its defining term in $\KB_{T}''$.  The \emph{expansion of a KB} $\KB$ 
works as follows \cite{Nebel90a}.

\begin{enumerate}
	\item \emph{Elimination of concept specialisation}: each concept 
	specialisation $A \impc C \in \KB_{T}$ is replaced with a concept 
	definition $A \defc C \andc A^{*}$, where $A^{*}$ is a new 
	primitive concept.  $A^{*}$ stands for the absent part of the 
	definition of $A$.  Let $\KB'_{T}$ be the terminology, which 
	is obtained by replacing all concept specialisation by concept 
	definitions.
	
	\item \emph{Expansion of $\KB'_{T}$}: every defined concept (\ie\ 
	the first argument of a concept definition) which occurs in the 
	defining term of a concept definition (\ie\ the second argument of 
	a concept definition) is substituted by its defining term.  This 
	process is iterated until there remain only undefined concepts in 
	the second arguments of concept definitions. This yields a 
	terminology $\KB''_{T}$.

	\item \emph{Expansion of $\KB_{A}$}: every primitive concept 
	occurring in $\KB_{A}$ which is defined in $\KB''_{T}$ is 
	substituted by its defining term in $\KB''_{T}$. This yields $\KB_{A}'$.
\end{enumerate}

\nd The transformation has the nice property that $\KB \entail \ass$ 
iff $\KB_{A}' \entail \ass'$, where $\ass'$ is obtained by replacing 
every primitive concept occurring in $\ass$, which is defined in 
$\KB''_{T}$, with its defining term in $\KB''_{T}$.  While this allows 
us to restrict our attention to purely assertional KBs only, it is 
worth noting that the expansion process can be exponential 
\cite{Nebel88}.

From \ii{\ref{pb8}}--\ii{\ref{pb7}}, it follows that the above 
problems can be reduced to the satisfiability problem.  There exists a 
well known technique based on constraint propagation solving this 
problem \cite{Schmidt-Schauss91,Buchheit93b,Donini94c}.

We conclude with an example.

\begin{exmp} \label{exfirst}
Consider the following terminology $\KB_{T}$.

\[
\begin{array}{lcl}
{\sf SportKind} & \impc & \topc \\
{\sf SportTool} & \impc & \topc \\
{\sf IndividualSport} & \impc & {\sf SportKind} \\
{\sf TeamSport} & \impc & {\sf SportKind} \\
{\sf Basketball} & \impc & {\sf SportTool} \\
{\sf TennisRacket} & \impc & {\sf SportTool} \\
% {\sf TeamSportVideo} & \defc &  
%                 \begin{array}[t]{l}
%                    {\sf SportVideo} \andc \\
%                    (\csome {\sf KindOfSport}.\topc) \andc \\ 
%                    (\all {\sf KindOfSport}.{\sf TeamSport})
%                  \end{array} \\
%{\sf IndividualSportVideo} & \defc &  
%                 \begin{array}[t]{l}
%                    {\sf SportVideo} \andc \\
%                    (\csome {\sf KindOfSport}.\topc) \andc \\ 
%                    (\all {\sf KindOfSport}.{\sf IndividualSport})
%                  \end{array} \\
{\sf Basket} & \defc &  
                \begin{array}[t]{l}
                   {\sf SportKind} \andc \\
                   (\csome {\sf KindOfSport}.\topc) \andc \\ 
                   (\all {\sf KindOfSport}.{\sf TeamSport}) \andc \\
%                    {\sf TeamSportVideo} \andc \\
                   (\csome {\sf HasSportTool}.\topc) \andc \\ 
                   (\all {\sf HasSportTool}.{\sf Basketball})
                 \end{array}   \\
{\sf Tennis} & \defc &  
                \begin{array}[t]{l}
                  {\sf SportKind} \andc \\
                  (\csome {\sf KindOfSport}.\topc) \andc \\ 
                  (\all {\sf KindOfSport}.{\sf IndividualSport}) \andc \\
%                   {\sf IndividualSportVideo} \andc \\
                  (\csome {\sf HasSportTool}.\topc) \andc \\ 
                  (\all {\sf HasSportTool}.{\sf TennisRacket})
                 \end{array}                                       
\end{array}
\]
%\[
%\begin{array}{lcl}
%{\sf TennisVideo} & \defc &  
%                \begin{array}[t]{l}
%                   {\sf IndividualSportVideo} \andc \\
%                   (\csome {\sf HasSportTool}.{\sf TennisRacket}) \andc \\ 
%                   (\all {\sf HasSportTool}.{\sf TennisRacket})
%                 \end{array}
%\end{array}
%\]

\nd
Suppose that there are two video sequences {\sf v1}, {\sf v2}, 
which are about basket and tennis, respectively. We may represent the
semantic content of them through

\[
\begin{array}{l}
\KB_{{\sf v1}} = \{\cass{{\sf v1}}{\sf Video \andc \csome About.Basket}\}  \\
\KB_{{\sf v2}} = \{\cass{{\sf v2}}{\sf Video \andc \csome About.Tennis}\} .
\end{array}
\]

\nd Consider $\KB = \KB_{T} \cup \KB_{{\sf v1}} \cup \KB_{{\sf v2}}$.  
If we are interested in retrieving videos about sport, we may query 
$\KB$ through the query concept ${\sf Q} = {\sf Video \andc \csome 
About.SportKind}$ and the answer will be the list containing both {\sf 
v1} and {\sf v2}, as $\KB \entail \cass{\sf v1}{\sf Q}$ and $\KB 
\entail \cass{{\sf v2}}{\sf Q}$ hold.

On the other hand, if we are looking 
for individual sport videos, then, given the query concept
${\sf Q'} = {\sf Video \andc \csome About.\csome KindOfSport.IndividualSport}$,
it follows that only video {\sf v2} will be retrieved. In fact,
$\KB \notentail \cass{v1}{\sf Q'}$ and
$\KB \entail    \cass{v2}{\sf Q'}$ hold.
\okex
\end{exmp}


%-------------------------------------------------------

%---- DLs four-valued fuzzy
\section{A Fuzzy DL}
\label{dlf}

\nd Our fuzzy extension directly relates to Zadeh's work on fuzzy 
sets~\cite{Zadeh65}.  A {\em fuzzy set} $S$ with respect to an 
universe $U$ is characterised by a {\em membership function} 
$\vgen{S}:U \rightarrow [0,1]$, assigning an $S$-membership degree, 
$\vgen{S}(u)$, to each element $u$ in $U$.  $\vgen{S}(u)$ gives us an 
estimation of the belonging of $u$ to $S$.  Typically, if $\vgen{S}(u) 
= 1$ then $u$ definitely belongs to $S$, while $\vgen{S}(u) = 0.8$ 
means that $u$ is ``likely'' to be an element of $S$.  Moreover, 
according to Zadeh, the membership function has to satisfy three 
well known restrictions: for all $u\in U$ and for all fuzzy sets 
$S_{1},S_{2}$ with respect to $U$

\[
\begin{array}{lcl}
\vgen{S_{1} \cap S_{2}}(u) & = & \min\{\vgen{S_{1}}(u), \vgen{S_{2}}(u)\} \\
\vgen{S_{1} \cup S_{2}}(u) & = & \max\{\vgen{S_{1}}(u), \vgen{S_{2}}(u)\} \\
\vgen{\overline{S_{1}}}(u) & = & 1 - \vgen{S_{1}}(u) \   ,
\end{array}
\]

\nd where $\overline{S_{1}}$ is the complement of $S_{1}$ in $U$.  
Alternative restrictions on membership functions have been proposed in 
the literature, but it is not our aim to investigate them here (the 
interested reader may consult \eg~Dubois \& Prade, 1980).%\cite{Dubois80}).  

A justification 
of the choice of the $\min$ and the $\max$ was given by Bellman and 
Giertz (1973), %\cite{Bellman73}, 
which have shown that under certain 
reasonable conditions $\min$ and $\max$ are the unique possible choice 
for set intersection and set union, respectively.

When we switch to fuzzy logics, the notion of degree of membership 
$\vgen{S}(u)$ of an element $u \in U$ w.r.t.\ the fuzzy set $S$ over 
$U$ is regarded as the \emph{truth-value} of the statement \emph{``u 
is $S$''}.  Accordingly, in our fuzzy DL, \ii{i} a concept $C$, rather 
than being interpreted as a classical set, will be interpreted as a 
fuzzy set and, thus, concepts become {\em imprecise}; and, 
consequently, \ii{ii} the statement ``$a$ is $C$'', \ie \ 
$\cass{a}{C}$, will have a truth-value in $[0,1]$ given by the 
degree of membership of being the individual $a$ a member of the fuzzy 
set $C$.

%-----------------------------

% \paragraph{Fuzzy Interpretation:}
\subsection{Fuzzy Interpretation}
\nd A {\em fuzzy interpretation} is now a pair $\I = (\highi{\Delta}, 
\highi{\cdot})$, where $\highi{\Delta}$ is, as for the crisp case, the 
{\em domain}, whereas $\highi{\cdot}$ is an {\em interpretation 
function} mapping

\begin{enumerate}
\item
individuals as for the crisp case, \ie~$\highi{a} \neq \highi{b}$, if $a \neq b$;
\item
a concept $C$ into a membership function 
$\highi{C}\colon\highi{\Delta} \rightarrow \range{0}{1}$;
\item
a role $R$ into a membership function
$\highi{R}\colon\highi{\Delta} \times \highi{\Delta} \rightarrow \range{0}{1}$.
\end{enumerate}

\nd If $C$ is a concept then $\highi{C}$ will naturally be interpreted 
as the {\em membership degree function} of the fuzzy concept (set) $C$ 
\wrt~$\I$, \ie~if $d \in \highi{\Delta}$ is an object of the domain 
$\highi{\Delta}$ then $\highi{C}(d)$ gives us the degree of being the 
object $d$ an element of the fuzzy concept $C$ under the 
interpretation $\I$.  Similarly for roles.  Additionally, the 
interpretation function $\highi{\cdot}$ has to satisfy the following 
equations: for all $d \in \highi{\Delta}$,

\[
\begin{array}{lll}
\highi{\topc}(d) & = & 1 \\
\highi{\bottomc}(d) & = & 0 \\ 
\highi{(C \andc D)}(d) & = & \min\{\highi{C}(d), \highi{D}(d)\} \\
\highi{(C \orc D)}(d) & = & \max\{\highi{C}(d), \highi{D}(d)\} \\
\highi{(\notc C)}(d) & = & 1 - \highi{C}(d) \\
\highi{(\all R.C)}(d) & = & 
\inf_{d'\in\highi{\Delta}}\{\max\{1-\highi{R}(d,d'), \highi{C}(d')\}\} \\
\highi{(\csome R.C)}(d) & = & 
\sup_{d'\in\highi{\Delta}} \{\min\{\highi{R}(d,d'), \highi{C}(d')\}\}. 
\end{array}
\]

\nd These equations are the standard interpretation of conjunction, 
disjunction, negation and quantification, respectively 
(see Lee, 1972; Tresp \& Molitor, 1998).
%\cite{Lee72,Tresp98}, too).  

Note that the semantics of $\csome R.C$
   
\begin{equation} \label{alcsome}
\begin{array}{lll}
\highi{(\csome R.C)}(d) & = & 
\sup_{d'\in\highi{\Delta}} \{\min\{\highi{R}(d,d'), \highi{C}(d')\}\}
\end{array}
\end{equation}

\nd is the result of viewing $\csome R.C$ as the open first order 
formula $\exists y.  F_{R}(x,y) \andf F_{C}(y)$ (see \myref{folcsome}) 
and the existential quantifier $\exists$ is viewed as a disjunction 
over the elements of the domain.  Similarly,

\begin{equation} \label{alcall}
\begin{array}{lll}
\highi{(\all R.C)}(d) & = & 
\inf_{d'\in\highi{\Delta}}\{\max\{1-\highi{R}(d,d'), \highi{C}(d')\}\}
\end{array}
\end{equation}

\nd is related to the open first 
order formula $\forall y.  \notf F_{R}(x,y) \orf F_{C}(y)$ (see 
\myref{folall}), where the universal quantifier $\all$ is 
viewed as a conjunction over the elements of the domain.

We will say that two concepts $C$ and $D$ are said to be {\em 
equivalent} (denoted by $C \equivf D$) when $\highi{C} = \highi{D}$ 
for all interpretations $\cal I$.  As for the crisp non fuzzy case, 
dual relationships between concepts hold: \eg~$\topc \equivf \notc 
\bottomc$, $(C \andc D) \equivf \notc (\notc C \orc \notc D)$ and 
$(\all R.C) \equivf \notc (\csome R.\notc C)$.



%-----------------------------

% \paragraph{Fuzzy Assertion:}
\subsection{Fuzzy Assertion}

\nd A {\em fuzzy assertion} (denoted by $\assf$) is an expression 
having one of the following form $\fuzzy{\ass}{n}{\geq}$ or 
$\fuzzy{\ass}{m}{\leq}$, where $\ass$ is an \alc \ assertion, $n \in 
(0,1]$ and $m \in [0,1)$.  From a semantics point of view, a fuzzy 
assertion $\fuzzy{\ass}{n}{\leq}$ constrains the truth-value of $\ass$ 
to be less or equal to $n$ (similarly for $\geq$).  Consequently, \eg\ 
$\fuzzy{\cass{{\sf v1}}{\sf Video \andc \csome 
About.Basket}}{0.8}{\geq}$ states that video {\sf v1} is likely about 
basket.  Formally, an interpretation $\I$ {\em satisfies} a fuzzy 
assertion $\fuzzy{\cass{a}{C}}{n}{\geq}$ (resp.  
$\fuzzy{\rass{a}{b}{R}}{n}{\geq}$) iff $\highi{C}(\highi{a}) \geq n$ 
(resp.  $\highi{R}(\highi{a},\highi{b}) \geq n$).  Similarly, an 
interpretation $\I$ {\em satisfies} a fuzzy assertion 
$\fuzzy{\cass{a}{C}}{n}{\leq}$ (resp.  
$\fuzzy{\rass{a}{b}{R}}{n}{\leq}$) iff $\highi{C}(\highi{a}) \leq n$ 
(resp.  $\highi{R}(\highi{a},\highi{b}) \leq n$).  Two fuzzy 
assertions $\assf_1$ and $\assf_2$ are said to be {\em equivalent} 
(denoted by $\assf_1 \equivf \assf_2$) iff they are satisfied by the 
same set of interpretations.  Notice that the combination of both 
$\fuzzy{\cass{a}{C}}{m}{\geq}$ and $\fuzzy{\cass{a}{C}}{n}{\leq}$, 
with $m\leq n$, restricts the truth-value of $\cass{a}{C}$ in between 
$\range{m}{n}$.  Moreover, $\fuzzy{\cass{a}{\notc C}}{n}{\geq} \equivf 
\fuzzy{\cass{a}{C}}{1-n}{\leq}$.  A \emph{primitive fuzzy assertion} 
is a fuzzy assertion involving a primitive assertion.

One might wonder why we do not allow expressions of the form 
$\fuzzy{\ass}{n}{>}$ or the form $\fuzzy{\ass}{n}{<}$.  The reason 
simply relies on the observation that it is quite hard to imagine 
situations in which we are able to assert such {\em strict} $>,<$ 
relations.  So we will leave them out for ease.\footnote{Of course, 
the whole can easily be extended in case we would like to consider 
these two types of assertions too.}

Note that in the work of Straccia (1998), %\cite{Straccia98} 
no fuzzy assertion of the form $\fuzzy{\ass}{n}{\leq}$ is allowed.


%--------------------------------------------------------------------------
% \paragraph{Fuzzy Terminological Axiom:}  \label{semffvALCspec}
\subsection{Fuzzy Terminological Axiom}  \label{semffvALCspec}
%--------------------------------------------------------------------------

\nd Fuzzy terminological axioms we will consider are a natural 
extension of classical terminological axioms to the fuzzy case.  From 
a syntax point of view, a \emph{fuzzy terminological axiom} (denoted 
by $\specf$) is either a fuzzy concept specialisation or a fuzzy 
concept definition.  A {\em fuzzy concept specialisation} is an 
expression of the form $A \impcf C$, where $A$ is a primitive concept 
and $C$ is a concept.  On the other hand, a \emph{fuzzy concept 
definition} is an expression of the form $A \defcf C$, where $A$ is a 
primitive concept and $C$ is a concept.  From a semantics point of 
view, we consider the natural extension of classical set inclusion to 
the fuzzy case \cite{Zadeh65}.  A fuzzy interpretation $\I$ {\em 
satisfies} a fuzzy concept specialisation $A \impcf C$ iff

\begin{equation} \label{alcffvspec}
\forall d \in\highi{\Delta}, \highi{A}(d) \leq \highi{C}(d) ,
\end{equation}

\nd
whereas $\I$ {\em satisfies} a fuzzy 
concept definition $A \defcf C$ iff

\begin{equation} \label{alcffvdef}
\forall d \in\highi{\Delta}, \highi{A}(d) = \highi{C}(d) .
\end{equation}

\nd Note that in the work of Straccia (1998) %\cite{Straccia98} 
a fuzzy specialisation is 
``non-standard''.  Indeed, Straccia (1998) considered %\cite{Straccia98} 
 fuzzy specialisations 
of the form $\fuzzy{A \impf C}{n}{\geq}$ where $\highi{(A \impf C)}  
=  \min_{d\in\highi{\Delta}} \{\max\{1-\highi{A}(d), 
\highi{C}(d)\}\}$.  A drawback of this formulation is that it is not 
clear where the $n$ in $\fuzzy{A \impf C}{n}{\geq}$ comes from, \ie\ 
who defines the value $n$ and how it is determined.  We prefer to rely 
here on the standard interpretation of fuzzy subsets.

%------------------------------------------------------------------------

% \paragraph{Fuzzy Knowledge Base, Fuzzy Entailment and Fuzzy Subsumption:}
\subsection{Fuzzy Knowledge Base, Fuzzy Entailment and Fuzzy Subsumption}

\nd A \emph{fuzzy knowledge base} is a finite set of fuzzy assertions 
and fuzzy terminological axioms.  As for the crisp case, with 
$\FKB_A$ we will denote the set of fuzzy assertions in $\FKB$, with 
$\FKB_T$ we will denote the set of fuzzy terminological axioms in 
$\FKB$ (the terminology), if $\FKB_T = \emptyset$ then $\FKB$ is 
{\em purely assertional}, and we will assume that a terminology 
$\FKB_T$ is such that no concept $A$ appears more than once on the 
left hand side of a fuzzy terminological axiom $\specf \in \FKB_T$ 
and that no cyclic definitions are present in $\FKB_T$.

An interpretation $\I$ {\em satisfies} (is {\em a model of}\/) a set 
of fuzzy $\FKB$ iff $\I$ satisfies each element of $\FKB$.  A fuzzy KB 
$\FKB$ {\em fuzzy entails} a fuzzy assertion $\assf$ (denoted by $\FKB 
\entailf \assf$) iff every model of $\FKB$ also satisfies $\assf$. 

Furthermore, let $\FKB_{T}$ be a terminology and let $C,D$ be two 
concepts.  We will say that $D$ \emph{fuzzy subsumes} $C$ w.r.t.\ 
$\FKB_{T}$ (denoted by $C \subsf_{\FKB_{T}} D$) iff for every model 
$\I$ of $\FKB_{T}$, $\forall d \in\highi{\Delta}, \highi{C}(d) \leq 
\highi{D}(d)$ holds.

Finally, given a fuzzy KB $\FKB$ and an assertion $\ass$, it is of 
interest to compute $\ass$'s best lower and upper truth-value bounds.  
To this end we define the {\em greatest lower bound} of $\ass$ 
\wrt~$\FKB$ (denoted by $glb(\FKB, \ass)$) to be $\sup\{n: \FKB 
\entailf \fuzzy{\ass}{n}{\geq}\}$.  Similarly, we define the {\em 
least upper bound} of $\ass$ with respect to $\FKB$ (denoted by 
$lub(\FKB, \ass)$) to be $\inf\{n: \FKB \entailf 
\fuzzy{\ass}{n}{\leq}\}$ ($\sup\emptyset = 0, \inf\emptyset = 1$).
Determining the $lub$ and the $glb$ is 
called the \emph{Best Truth-Value Bound} (BTVB) problem.


%------------------------------ PROPERTIES -------
\section{Some Properties} \label{pr}
%------------------------------ PROPERTIES -------

\nd In this section we discuss some properties of our fuzzy 
logic.  Several properties described by Straccia (2000b) %\cite{Straccia00a} 
for the propositional case are easily extended to our first order case too. 

% \paragraph{Concept Equivalence:}
\subsection{Concept Equivalence}
The first ones are straightforward: $\notc \topc \equivf \bottomc$, $ 
C \andc \topc \equivf C$, $C \orc \topc \equivf \topc$, $C \andc 
\bottomc \equivf \bottomc$, $ C \orc \bottomc \equivf C$, $\notc \notc 
C \equivf C$, $\notc (C \andc D) \equivf \notc C \orc \notc D$, $\notc 
(C \orc D) \equivf \notc C \andc \notc D$, $C_{1} \andc (C_{2} \orc 
C_{3}) \equivf (C_{1} \andc C_{2}) \orc (C_{1} \andc C_{3})$ and 
$C_{1} \orc (C_{2} \andc C_{3}) \equivf (C_{1} \orc C_{2}) \andc 
(C_{1} \orc C_{3})$.  For concepts involving roles, we have $\all R.C 
\equivf \notc \csome R. \notc C$, $\all R.\topc \equivf \topc$, 
$\csome R.\bottomc \equivf \bottomc$ and $(\all R.C) \andc (\all R.D) 
\equivf \all R.(C \andc D)$.  Please, note that we do not have $C 
\andc \notc C \equivf \bottomc$, nor we have $C \orc \notc C \equivf 
\topc$ and, thus, $(\csome R. C) \andc (\all R.\notc C) \not \equivf 
\bottomc$ and $(\csome R. C) \orc (\all R.\notc C) \not \equivf \topc$ 
hold.  In general we can only say that $\highi{(C \andc \notc C)}(d) 
\leq 0.5$, for any interpretation ${\mathcal I}$ and $d \in 
\highi{\Delta}$ and, similarly, $\highi{(C \orc \notc C)}(d) \geq 
0.5$, \ie\ $lub(\emptyset,\cass{a}{\notc C \andc C}) = 0.5$ and 
$glb(\emptyset,\cass{a}{\notc C \orc C}) = 0.5$, respectively.

% \paragraph{Entailment Relation:} 
\subsection{Entailment Relation} 
Of course, $\Sigma \entailf 
\fuzzy{\ass}{n}{\geq}$ iff $glb(\Sigma,\ass) \geq n$, and similarly 
$\Sigma \entailf \fuzzy{\ass}{n}{\leq}$ iff $lub(\Sigma,\ass) \leq 
n$ hold. Concerning roles, note that
$\Sigma \entailf \fuzzy{\rass{a}{b}{R}}{n}{\geq}$ iff
$\fuzzy{\rass{a}{b}{R}}{m}{\geq} \in \Sigma$ with $ m \geq n$. 
Therefore, 


\begin{equation}\label{lubglbrole}  
\begin{array}{lcl}
glb(\Sigma,R(a,b)) & = & \max\{n:\fuzzy{R(a,b)}{n}{\geq} \in \Sigma\}
\end{array}
\end{equation}

\nd while the same is not true for the $\leq$ case.  While 
$\fuzzy{\rass{a}{b}{R}}{m}{\leq} \in \Sigma$ and $m \leq n$ imply 
$\Sigma \entailf \fuzzy{\rass{a}{b}{R}}{n}{\leq}$, the converse is 
false (\eg\ $\{\fuzzy{\cass{a}{\all R.A}}{1}{\geq}, 
\fuzzy{\cass{b}{A}}{0}{\leq} 
\}\entailf\fuzzy{\rass{a}{b}{R}}{0}{\leq})$).

Furthermore, from $\Sigma \entailf \fuzzy{\cass{a}{C}}{n}{\leq}$ iff 
$\Sigma \entailf \fuzzy{ \cass{a}{\notc C}}{1-n}{\geq}$,

\[
\begin{array}{lcl}
1-lub(\Sigma,C(a)) 
& = & 1 - \inf\{n: \Sigma \entailf \fuzzy{\cass{a}{C}}{n}{\leq}\} \\
& = & \sup\{1-n: \Sigma \entailf \fuzzy{\cass{a}{C}}{n}{\leq}\} \\
& = & \sup\{n: \Sigma \entailf \fuzzy{\cass{a}{C}}{1-n}{\leq}\} \\
& = & \sup\{n: \Sigma \entailf \fuzzy{\cass{a}{\notc C}}{n}{\geq}\} \\
& = & glb(\Sigma,\cass{a}{\notc C}) .
\end{array}
\]

\nd
follows. Therefore,

\begin{equation}\label{lubglb}
\begin{array}{lcl}
lub(\Sigma,\cass{a}{ C}) & = & 1 - glb(\Sigma,\cass{a}{\notc C}),
\end{array}
\end{equation}

\nd \ie~$lub$ can be determined through $glb$ (and vice-versa).  
The same reduction to $glb$ does not hold for 
$lub(\Sigma,\rass{a}{b}{R})$ as $\rass{a}{b}{\notr R}$ is not an 
expression of our language.\footnote{Of course, 
$lub(\Sigma,\rass{a}{b}{R}) = 1 - glb(\Sigma,\rass{a}{b}{\notr R})$ 
holds, where $\highi{(\notr R)}(d,d') = 1- \highi{R}(d,d')$.}

{\em Modus ponens on concepts} is supported: if $m > 1-n$ then $\{ 
\fuzzy{\cass{a}{C}}{m}{\geq}$, $\fuzzy{\cass{a}{\notc C \orc 
D}}{n}{\geq}\} \entailf$ $\fuzzy{\cass{a}{D}}{n}{\geq}$ holds.

{\em Modus ponens on roles} is supported: if $m > 1-n$ then 
$\{\fuzzy{\rass{a}{b}{R}}{m}{\geq}$, $\fuzzy{\cass{a}{\all 
R.D}}{n}{\geq}\}$ $\entailf \fuzzy{\cass{a}{D}}{n}{\geq}$ and 
$\{\fuzzy{\cass{a}{\csome R. C}}{m}{\geq}$, $\fuzzy{\cass{a}{\all 
R.D}}{n}{\geq}\}$ $\entailf \fuzzy{\cass{a}{\csome R. (C \andc 
D)}}{\min\{n,m\}}{\geq}$ hold.  Moreover, $\{\fuzzy{\cass{a}{\all 
R.C}}{m}{\geq}$, $\fuzzy{\cass{a}{\all R.D}}{n}{\geq} \}$ $\entailf 
\fuzzy{\cass{a}{\all R.(C \andc D)}}{\min\{n,m\}}{\geq}$ holds.

\emph{Modus ponens on specialisation} is supported.  The following 
degree bounds propagation through a taxonomy is supported.  If $C 
\subsf_{\FKB} D$ then \ii{i} $\FKB \cup 
\{\fuzzy{\cass{a}{C}}{n}{\geq}\} \entailf 
\fuzzy{\cass{a}{D}}{n}{\geq}$; and \ii{ii} $\FKB \cup 
\{\fuzzy{\cass{a}{D}}{n}{\leq}\} \entailf 
\fuzzy{\cass{a}{C}}{n}{\leq}$ hold.

Note that, according to Straccia (1998) %\cite{Straccia98}

\[
\mbox{ if } m > 1-n \mbox{ then } \{\fuzzy{\cass{a}{A}}{m}{\geq}, 
\fuzzy{A \impf C}{n}{\geq}\} \entailf 
\fuzzy{\cass{a}{C}}{n}{\geq}  .
\]

\nd A drawback of the above property is that whatever the degree $m$ 
is (as long as $m > 1-n$), from $\fuzzy{\cass{a}{A}}{m}{\geq}$ and 
$\fuzzy{A \impf C}{n}{\geq}$ we infer $\fuzzy{\cass{a}{C}}{n}{\geq}$, 
where $n$ is a priori fixed value.

% \paragraph{Soundness of the Semantics:}
\subsection{Soundness of the Semantics}
Our fuzzy semantics is {\em sound} \wrt~crisp semantics.  In fact, let 
$\FKB$ be a fuzzy KB in which no $\fuzzy{\rass{a}{b}{R}}{n}{\leq}$ 
occurs.  We leave these fuzzy assertions out, as role negation is not 
present in crisp \alc.  Let us consider the following transformation 
$\crisp{(\cdot)}$ of fuzzy assertions into assertions, where 
$\crisp{(\cdot)}$ takes the ``crisp'' assertional part of a fuzzy 
assertion:

\begin{eqnarray*}
    \crisp{\fuzzy{\ass}{n}{\geq}} & \mapsto  & \ass \\
    \crisp{\fuzzy{\cass{a}{C}}{n}{\leq}} & \mapsto  & \cass{a}{\notc C}.
\end{eqnarray*}

\nd We extend $\crisp{(\cdot)}$ to fuzzy terminological axioms as 
follows: $\crisp{\specf} = \spec$.  Finally, $\crisp{\FKB}= 
\{\crisp{\psi}: \psi \in \Sigma\} \cup \{\crisp{\specf}: \specf \in 
\Sigma_{T}\}$.

It is quite easily to verify that

\begin{prop} \label{p2}
Let $\FKB$ be a fuzzy KB in which no $\fuzzy{\rass{a}{b}{R}}{n}{\leq}$ 
occurs and let $\assf$ be a fuzzy assertion $\fuzzy{\ass}{n}{\geq}$.  
If $\FKB \entailf \fuzzy{\ass}{n}{\geq}$ then $\crisp{\FKB} \entail 
\crisp{\psi}$ (\ie~\emph{there cannot be fuzzy entailment without 
entailment in \alc}).  \ok
\end{prop}

\begin{pf}
Consider a classical interpretation $\I$ satisfying $\crisp{\FKB}$.  
$\I$ is also a fuzzy interpretation such that $\highi{C}(d) \in 
\{0,1\}$, $\highi{R}(d,d') \in \{0,1\}$ hold.  By induction on the 
structure of a concept $C$ it can be shown that $\I$ (classically) 
satisfies $\cass{a}{C}$ iff $\highi{C}(\highi{a})= 1$.  Similarly for 
roles.  Therefore, $\I$ is a fuzzy interpretation satisfying $\FKB$.  
By hypothesis, $\I$ satisfies $\fuzzy{\ass}{n}{\geq}$ and $n> 0$.  
Therefore, the truth-value of $\ass$ under $\I$ is $1$, \ie\ $\I$ 
satisfies $\ass$.  \qed
\end{pf}

\nd For the general case, $\FKB$ has to be satisfiable as 
$\fuzzy{\rass{a}{b}{R}}{n}{\leq}$ may introduce an inconsistency, \eg\ 
$\{\fuzzy{\rass{a}{b}{R}}{0.3}{\leq}, 
\fuzzy{\rass{a}{b}{R}}{0.4}{\geq}\}\entailf 
\fuzzy{\cass{a}{A}}{1}{\geq}$, but $\{\rass{a}{b}{R}\} \not \entail 
\cass{a}{A}\}$.

The converse of Proposition~\ref{p2} does not hold in general. 

\begin{exmp} \label{ex2}
Let $\FKB$ be the set $\FKB = \{ \fuzzy{\cass{a}{A \orc 
B}}{0.6}{\leq}, \fuzzy{\cass{a}{A}}{0.3}{\geq} \}$.  It follows that 
$\crisp{\FKB} = \{\cass{a}{\notc (A \orc B)}, \cass{a}{A}\}$ which is 
unsatisfiable.  Therefore, it can easily be verified that $\crisp{\FKB} \entail 
\cass{a}{B}$, but $\FKB \notentailf \fuzzy{\cass{a}{B}}{n}{\geq}$, for 
all $n >0$.  \okex
\end{exmp}

\nd Once we restrict the attention to normalised fuzzy assertions, a 
converse relation follows immediately \cite{Lee72,Straccia00a}.

Indeed, we say that a fuzzy assertion $\psi$ is 
\emph{KB-normalised\/} iff

\begin{enumerate}
    \item  if $\psi$ is $\fuzzy{\ass}{n}{\geq}$ then $n > 0.5$;
    \item  if $\psi$ is $\fuzzy{\ass}{n}{\leq}$ then $n < 0.5$.
\end{enumerate}

\nd
We say that a fuzzy assertion $\psi$ is \emph{query-normalised\/} iff 

\begin{enumerate}
    \item  if $\psi$ is $\fuzzy{\ass}{n}{\geq}$ then $n \leq 0.5$; 
    \item  if $\psi$ is $\fuzzy{\ass}{n}{\leq}$ then $n \geq 0.5$.
\end{enumerate}

\nd Note that the definitions for KB-normalisation and 
query-normalisation are dual.  The following proposition follows from 
\cite{Lee72,Straccia00a} and relies on the fact that 
$\fuzzy{\ass}{n}{\geq}$ and $\fuzzy{\ass}{m}{\leq}$ are together 
inconsistent, if $n > 0.5$ and $m < 0.5$.  In particular, 
Straccia (2000b) %\cite{Straccia00a} 
shows that if $\FKB$ and $\psi$ are a normalised 
fuzzy propositional KB and a query-normalised fuzzy proposition, then 
Then $\FKB \entailf \psi$ iff $\crisp{\FKB} \entail \crisp{\psi}$.  
The proof is given by showing that from a deduction proving $\FKB 
\entailf \psi$ a deduction proving $\crisp{\FKB} \entail \crisp{\psi}$ 
can be build and vice-versa.  The extension to our case is 
straightforward as \eg\ for $n, m > 0.5$, $\fuzzy{\cass{a}{\all 
R.C}}{n}{\geq}, $\fuzzy{\rass{a}{b}{R}}{m}{\geq}$ \entailf 
\fuzzy{\cass{b}{C}}{n}{\geq}$ iff $\cass{a}{\all R.C}, \rass{a}{b}{R} 
\entail \cass{b}{C}$ holds (the other first-order cases involving 
$\all$ and $\csome$ are similar).

\begin{prop} \label{p3}
Let $\FKB$ be a fuzzy KB in which no $\fuzzy{\rass{a}{b}{R}}{n}{\leq}$ 
occurs and each $\psi \in \Sigma$ is KB-normalised.  Let $\psi$ be a 
query-normalised fuzzy assertion.  Then $\FKB \entailf \psi$ iff 
$\crisp{\FKB} \entail \crisp{\psi}$.  \ok
\end{prop}

\begin{exmp} \label{ex3}
Let $\FKB$ be the set $\FKB = \{ \fuzzy{\cass{a}{A \andc 
B}}{0.4}{\leq}, \fuzzy{\cass{a}{A}}{0.6}{\geq}\}$.  Let $\psi$ be 
$\fuzzy{\cass{a}{B}}{0.7}{\leq}$.  Each fuzzy assertion in $\FKB$ is 
KB-normalised and $\psi$ is query-normalised.  It follows that 
$\crisp{\FKB}= \{\cass{a}{\notc (A \andc B)},\cass{a}{A}\}$ and 
$\crisp{\psi}= \cass{a}{\notc B}$.  It is easily verified that $\FKB 
\entailf \psi$ and that $\crisp{\FKB} \entail \crisp{\psi}$, thereby 
confirming Proposition~\ref{p3}.  \okex
\end{exmp}

% \paragraph{Subsumption:}
\subsection{Subsumption}

At first, as for the classical case and with the same method seen 
before, subsumption between two concepts $C$ and $D$ w.r.t.\ a 
terminology $\FKB_{T}$, \ie\ $C \subsf_{\FKB_{T}} D$, can be reduced 
to the case of an empty terminology, \ie\ $C' \subsf_{\emptyset} D'$.

\begin{exmp} \label{zadehspecex}
Suppose we have two images {\sf i1} and {\sf i2} each being a snapshot 
of the car traffic on a major street of an European city.  An 
underlying image analysis tool recognizes, among all the recognised 
objects, that in image {\sf i1} there is a Ferrari, while in image 
{\sf i2} there is a Porsche.  Furthermore, a semantic image indexing 
tool establishes that, to some degree $n$ image {\sf i1} is 
\emph{about} a Ferrari, whereas to some degree $m$ image {\sf i2} is 
\textit{about} a Porsche.  Please note that, as a weight of a keyword 
in text is a quantitative description of the aboutness of the text 
\wrt\ the keyword, a truth-degree gives a quantitative description of 
the \emph{aboutness} of an images \wrt\ an object, \ie\ the aboutness 
is handled as an imprecise concept.  So, let us consider

\[
\begin{array}{lcl}
\FKB & = & 
   \{\fuzzy{\cass{{\sf i1}}{{\sf \csome About. Ferrari}}}{0.6}{\geq},
   \fuzzy{\cass{{\sf i2}}{{\sf \csome About. Porsche}}}{0.8}{\geq}, \\
   && \ {\sf Ferrari} \impcf {\sf Car}, {\sf Porsche} \impcf {\sf Car}\}  .
\end{array}
\]

\nd
where the axioms specify that both a Ferrari and a Porsche are a car.
According to the expansion process, $\FKB$ will be replaced by 

\[
\begin{array}{lcl}
\FKB' & = & 
   \{\fuzzy{\cass{{\sf i1}}{{\sf \csome About. Ferrari}}}{0.6}{\geq},
   \fuzzy{\cass{{\sf i2}}{{\sf \csome About. Porsche}}}{0.8}{\geq}, \\
   && \ {\sf Ferrari} \defcf {\sf Car} \andc {\sf Ferrari}^{*}, 
   {\sf Porsche} \defcf {\sf Car} \andc {\sf Porsche}^{*}\},
\end{array}
\]

\nd
which will be simplified to

\[
\begin{array}{lcl}
\FKB'' & = & 
   \{\fuzzy{\cass{{\sf i1}}{{\sf \csome About. ({\sf Car} \andc {\sf 
   Ferrari}^{*})}}}{0.6}{\geq}, \\
   && \fuzzy{\cass{{\sf i2}}{{\sf \csome About. ({\sf Car} \andc {\sf 
   Porsche}^{*})}}}{0.8}{\geq}\}.
\end{array}
\]

\nd Now, if we are looking for images which are about cars, then 
from $\FKB$ we may infer that $\FKB$ $\entailf$ $\fuzzy{\cass{{\sf 
i1}}{{\sf \csome About.  Car}}}{0.6}{\geq}$ and $\FKB \entailf 
\fuzzy{\cass{{\sf i2}}{{\sf \csome About.  Car}}}{0.8}{\geq}$.  
Furthermore, it is easily verified that $\FKB''$ $\entailf$ 
$\fuzzy{\cass{{\sf i1}}{{\sf \csome About.  Car}}}{0.6}{\geq}$ and 
$\FKB'' \entailf \fuzzy{\cass{{\sf i2}}{{\sf \csome About.  
Car}}}{0.8}{\geq}$ hold as well.  Indeed, for any fuzzy assertion $\assf$, 
$\FKB \entailf \assf$ iff $\FKB'' \entailf \assf$ holds. \okex
\end{exmp}

\nd 
We conclude this section with the analogue of Example~\ref{exfirst} 
for the fuzzy case..

\begin{exmp} \label{exfirstbis}
{\em Consider the terminology $\KB_{T}$ and the query concept {\sf Q} 
in Example~\ref{exfirst}.  Let us define $\FKB_{T}$ as the fuzzy KB 
derived from $\KB_{T}$ in which each terminological axiom $\spec$ has 
been replaced with the fuzzy terminological axiom $\specf$.  Moreover, 
let us suppose that an underlying semantic video indexing tool furnishes the 
following semantic descriptions of the two videos {\sf v1} and {\sf 
v2}.

\[
\begin{array}{l}
\FKB_{{\sf v1}} = \{\fuzzy{\cass{{\sf v1}}{{\sf Video}}}{1}{\geq}, 
                    \fuzzy{\cass{{\sf v1}}{{\sf \csome 
                    About.Basket}}}{0.9}{\geq}\}  \\
\FKB_{{\sf v2}} = \{\fuzzy{\cass{{\sf v2}}{{\sf Video}}}{1}{\geq},
                    \fuzzy{\cass{{\sf v2}}{{\sf \csome 
                    About.Tennis}}}{0.6}{\geq}\}   ,
\end{array}
\]

\nd \ie~video {\sf v1} is about basket with degree $0.9$, whereas 
video {\sf v2} is about tennis with degree $0.6$.  Let us consider 
$\FKB = \FKB_{T} \cup \FKB_{{\sf v1}} \cup \FKB_{{\sf v2}}$.  It is 
easily verified that $glb(\FKB,\cass{{\sf v1}}{{\sf Q}}) = 0.9$, 
whereas $glb(\FKB,\cass{{\sf v2}}{{\sf Q}}) = 0.6$ hold.  
Therefore, video {\sf v1} will be ranked before video {\sf v2} after 
the retrieval process.  } \okex
\end{exmp}

%------------------------------ Decision Algorithms -------

\section{Decision Algorithms in Fuzzy \alc} \label{decalc}

\nd Deciding whether $\FKB \entailf \fuzzy{\ass}{n}{\geq}$ or $\FKB 
\entailf \fuzzy{\ass}{m}{\leq}$ requires a calculus.  Without loss of 
generality we will consider purely assertional fuzzy KBs only.

We will develop a calculus in the style of the constraint propagation 
method, as this method is usually proposed in the context of 
DLs \cite{Buchheit93}.  The calculus extends the fuzzy 
propositional calculus described by  Chen and Kundu (1996) and 
by Straccia (2000b) %\cite{ChenJ96,Straccia00a} 
to our fuzzy DL case.  We first address the entailment problem, then the 
subsumption problem and finally the BTVB problem.  Both the 
subsumption problem and the BTVB problem will be reduced to the 
entailment problem.

%------------------------------ Deciding fuzzy implication -------
\subsection{A Decision Procedure for the Entailment Problem} \label{calc}
%------------------------------ 

\nd Consider a new alphabet of {\em \alc \ variables}.  An 
interpretation is extended to variables by mapping these into elements 
of the interpretation domain.  An {\em \alc \ object} (denoted by $w$) 
is either an individual or a variable.\footnote{In the following, if 
there is no ambiguity, \alc \ variables and \alc \ objects are called 
variables and objects, respectively.}

A {\em constraint} (denoted by $\cons$) is an expression of the form 
$\cass{w}{C}$ or $\cass{(w,w')}{R}$, where $w, w'$ are objects, $C$ is 
an \alc \ concept and $R$ is a role.  A {\em fuzzy constraint} 
(denoted by $\consf$) is an expression having one of the following 
four forms:
$
\fuzzy{\cons}{n}{\geq},
\fuzzy{\cons}{n}{>}, 
\fuzzy{\cons}{n}{\leq},  
\fuzzy{\cons}{n}{<} 
$.
% \[
% \fuzzy{\cons}{n}{\geq}, \ \
% \fuzzy{\cons}{n}{>}, \ \
% \fuzzy{\cons}{n}{\leq}, \ \ 
% \fuzzy{\cons}{n}{<}. 
% \]
Note that assertions and fuzzy assertions are constraints and 
fuzzy constraints, respectively.

The definitions of satisfiability of a constraint, a fuzzy constraint, 
a set of constraints, a set of fuzzy constraints, primitive constraint 
and primitive fuzzy constraint are obvious.


It is quite easily verified that the fuzzy entailment problem can be 
reduced to the unsatisfiability problem of a set of fuzzy constraints:

\begin{eqnarray} 
\FKB \entailf \fuzzy{\ass}{n}{\geq} & \mbox{ iff } &
       \FKB \cup \{\fuzzy{\ass}{n}{<}\} \mbox{ not satisfiable} \\ \label{entailcond}
\FKB \entailf \fuzzy{\ass}{n}{\leq} & \mbox{ iff } &
       \FKB \cup \{\fuzzy{\ass}{n}{>}\} \mbox{ not satisfiable}. \label{entailcondB}
\end{eqnarray} 



\nd Our calculus, determining whether a finite set $S$ of fuzzy constraints 
is satisfiable or not, is based on a set of constraint propagation 
rules transforming a set $S$ of fuzzy constraints into ``simpler" 
satisfiability preserving sets $S_i$ until either all $S_i$ contain a 
clash (indicating that from all the $S_i$ no model of $S$ can be 
build) or some $S_i$ is completed and clash-free, that is, no rule can 
be further be applied to $S_i$ and $S_i$ contains no clash (indicating 
that from $S_i$ a model of $S$ can be build).

A set of fuzzy constraints $S$ contains a {\em clash} iff it contains 
either one of the constraints in Table~\ref{clashcons}
\begin{table}[h]
\begin{center}
\begin{tabular}{l}
$\fuzzy{\cass{w}{\bottomc}}{n}{\geq}$,  where $n >0$ \\ 
$\fuzzy{\cass{w}{\topc}}{n}{\leq}$,  where $n < 1$  \\
$\fuzzy{\cass{w}{\bottomc}}{n}{>}$,  %\\
$\fuzzy{\cass{w}{\topc}}{n}{<}$,   %\\
$\fuzzy{\cass{w}{C}}{0}{<}$,  %\\
$\fuzzy{\cass{w}{C}}{1}{>}$ %\\  
\end{tabular}
\end{center}
\caption{Clashes} \label{clashcons}
\end{table}
or $S$ contains a conjugated pair of fuzzy constraints.
Each entry in Table~\ref{tabconj} 
\begin{table}[h]
\[
\begin{array}{|c|||c|c|} \hline
                       & \fuzzy{\cons}{m}{<}      &  \fuzzy{\cons}{m}{\leq}  \\ \hline \hline
\fuzzy{\cons}{n}{\geq}  & n\geq m                 &  n>m  \\ \hline
\fuzzy{\cons}{n}{>}     & n\geq m                 &  n\geq m  \\ \hline
\end{array}
\]
\caption{Conjugated Pairs} \label{tabconj}
\end{table}
says us under which condition
the row-column pair of fuzzy constraints is a {\em conjugated pair}.
Given a fuzzy constraint $\consf$, with $\consf^c$ we indicate a 
conjugate of $\consf$ (if there exists one).  Notice that a conjugate 
of a fuzzy constraint may be not unique, as there could be 
infinitely many.  For instance, both $\fuzzy{\cass{a}{C}}{0.6}{<}$ and 
$\fuzzy{\cass{a}{C}}{0.7}{\leq}$ are conjugates of 
$\fuzzy{\cass{a}{C}}{0.8}{\geq}$.

\nd
Concerning the rules, for each connective 
$\andc, \orc, \notc, \all, \csome$ there is a rule for each relation 
$\geq, >,\leq,<$, \ie~there are 20 rules. 
The rules have the form:

\begin{equation}
\begin{array}{c}
\Phi \rightarrow \Psi \mbox{  if } \Gamma
\end{array}
\end{equation}

\nd where $\Phi$ and $\Psi$ are sequences of fuzzy constraints and 
$\Gamma$ is a condition.  A rule fires only if \emph{the condition 
$\Gamma$ holds, if the current set $S$ of fuzzy constraints contains 
fuzzy constraints matching the precondition $\Phi$ and the consequence 
$\Psi$ is not already in $S$}.  After firing, the constraints from 
$\Psi$ are added to $S$.  The rules are the following:

\renewcommand{\arraystretch}{1.25}

\begin{equation} \label{setrules}
\begin{tabular}{ll}
(${\notrule}_{\geq}$) & 
    $\fuzzy{\cass{w}{\notc C}}{n}{\geq} \rightarrow \fuzzy{\cass{w}{C}}{1-n}{\leq}$ \\
(${\notrule}_{>}$) & 
    $\fuzzy{\cass{w}{\notc C}}{n}{>} \rightarrow \fuzzy{\cass{w}{C}}{1-n}{<}$ \\
(${\notrule}_{\leq}$) &
    $\fuzzy{\cass{w}{\notc C}}{n}{\leq} \rightarrow \fuzzy{\cass{w}{C}}{1-n}{\geq}$ \\
(${\notrule}_{<}$) &
    $\fuzzy{\cass{w}{\notc C}}{n}{<} \rightarrow \fuzzy{\cass{w}{C}}{1-n}{>}$ 
\end{tabular}
\end{equation}

\[
\begin{tabular}{ll}
(${\andrule}_{\geq}$) &  $\fuzzy{\cass{w}{C \andc D}}{n}{\geq}  \rightarrow
                          \fuzzy{\cass{w}{C}}{n}{\geq}, \fuzzy{\cass{w}{D}}{n}{\geq}$ \\
(${\andrule}_{>}$) &  $\fuzzy{\cass{w}{C \andc D}}{n}{>}  \rightarrow
                          \fuzzy{\cass{w}{C}}{n}{>}, \fuzzy{\cass{w}{D}}{n}{>}$ \\
(${\orrule}_{\leq}$) & $\fuzzy{\cass{w}{C \orc D}}{n}{\leq} \rightarrow 
                         \fuzzy{\cass{w}{C}}{n}{\leq}, \fuzzy{\cass{w}{D}}{n}{\leq}$ \\
(${\orrule}_{<}$) & $\fuzzy{\cass{w}{C \orc D}}{n}{<} \rightarrow 
                         \fuzzy{\cass{w}{C}}{n}{<}, \fuzzy{\cass{w}{D}}{n}{<}$                         
\end{tabular}
\]

\[
\begin{tabular}{ll}
(${\orrule}_{\geq}$) & $\fuzzy{\cass{w}{C \orc D}}{n}{\geq} \rightarrow
                         \fuzzy{\cass{w}{C}}{n}{\geq} \ | \ \fuzzy{\cass{w}{D}}{n}{\geq}$ \\
(${\orrule}_{>}$) & $\fuzzy{\cass{w}{C \orc D}}{n}{>} \rightarrow
                         \fuzzy{\cass{w}{C}}{n}{>} \ | \ \fuzzy{\cass{w}{D}}{n}{>}$ \\
(${\andrule}_{\leq}$) & $\fuzzy{\cass{w}{C \andc D}}{n}{\leq} \rightarrow
                         \fuzzy{\cass{w}{C}}{n}{\leq} \ | \ \fuzzy{\cass{w}{D}}{n}{\leq}$ \\
(${\andrule}_{<}$) & $\fuzzy{\cass{w}{C \andc D}}{n}{<} \rightarrow
                         \fuzzy{\cass{w}{C}}{n}{<} \ | \ \fuzzy{\cass{w}{D}}{n}{<}$
\end{tabular}
\]

\[
\begin{tabular}{ll}
(${\allrule}_{\geq}$) &  $\fuzzy{\cass{w_1}{\all R.C}}{n}{\geq},
                          \consf^c \rightarrow
                          \fuzzy{\cass{w_2}{C}}{n}{\geq}$ \\
   & \hspace*{.5cm} if $\consf$ is $\fuzzy{\cass{(w_1,w_2)}{R}}{1-n}{\leq}$  \\
(${\allrule}_{>}$) &  $\fuzzy{\cass{w_1}{\all R.C}}{n}{>},
                          \consf^c \rightarrow
                          \fuzzy{\cass{w_2}{C}}{n}{>}$ \\
   & \hspace*{.5cm} if $\consf$ is $\fuzzy{\cass{(w_1,w_2)}{R}}{1-n}{<}$  \\


(${\existsrule}_{\leq}$) & $\fuzzy{\cass{w_1}{\csome R.C}}{n}{\leq},
                            \consf^c \rightarrow
                            \fuzzy{\cass{w_2}{C}}{n}{\leq}$ \\ 
   & \hspace*{.5cm} if $\consf$ is $\fuzzy{\cass{(w_1,w_2)}{R}}{n}{\leq}$ \\

(${\existsrule}_{<}$) & $\fuzzy{\cass{w_1}{\csome R.C}}{n}{<},
                            \consf^c \rightarrow
                            \fuzzy{\cass{w_2}{C}}{n}{<}$ \\ 
   & \hspace*{.5cm} if $\consf$ is $\fuzzy{\cass{(w_1,w_2)}{R}}{n}{<}$
\end{tabular}
\]

\[
\begin{tabular}{ll}
(${\existsrule}_{\geq}$) & $\fuzzy{\cass{w}{\csome R.C}}{n}{\geq} \rightarrow
                           \fuzzy{\cass{(w,x)}{R}}{n}{\geq}, \fuzzy{\cass{x}{C}}{n}{\geq}$ \\
   & \hspace*{.5cm} if $x$  new variable and there is no $w'$ such that both \\
   & \hspace*{.5cm} $\fuzzy{\cass{(w,w')}{R}}{n}{\geq}$ and $\fuzzy{\cass{w'}{C}}{n}{\geq}$ 
    are already in the constraint set \\

(${\existsrule}_{>}$) & $\fuzzy{\cass{w}{\csome R.C}}{n}{>} \rightarrow
                           \fuzzy{\cass{(w,x)}{R}}{n}{>}, \fuzzy{\cass{x}{C}}{n}{>}$ \\
   & \hspace*{.5cm} if $x$  new variable and there is no $w'$ such that both \\
   & \hspace*{.5cm} $\fuzzy{\cass{(w,w')}{R}}{n}{>}$ and $\fuzzy{\cass{w'}{C}}{n}{>}$ 
    are already in the constraint set \\

(${\allrule}_{\leq}$) & $\fuzzy{\cass{w}{\all R.C}}{n}{\leq} \rightarrow 
                        \fuzzy{\cass{(w,x)}{R}}{1-n}{\geq}, \fuzzy{\cass{x}{C}}{n}{\leq}$ \\
   & \hspace*{.5cm} if $x$  new variable and there is no $w'$ such that both \\
   & \hspace*{.5cm} $\fuzzy{\cass{(w,w')}{R}}{1-n}{\geq}$ and $\fuzzy{\cass{w'}{C}}{n}{\leq}$ 
    are already in the constraint set \\

(${\allrule}_{<}$) & $\fuzzy{\cass{w}{\all R.C}}{n}{<} \rightarrow 
                        \fuzzy{\cass{(w,x)}{R}}{1-n}{>}, \fuzzy{\cass{x}{C}}{n}{<}$ \\
   & \hspace*{.5cm} if $x$  new variable and there is no $w'$ such that both \\
   & \hspace*{.5cm} $\fuzzy{\cass{(w,w')}{R}}{1-n}{>}$ and $\fuzzy{\cass{w'}{C}}{n}{<}$ 
    are already in the constraint set \\
\end{tabular}
\]

\renewcommand{\arraystretch}{1}

\nd
Examples of rule instances are the following:

\begin{center}
\begin{tabular}{ll}
(${\allrule}_{\geq}$) & 
$\fuzzy{\cass{a}{\all R.C}}{0.7}{\geq},
                          \fuzzy{\cass{(a,b)}{R}}{0.6}{\geq} \Rightarrow
                          \fuzzy{\cass{b}{C}}{0.7}{\geq}$  \\
& \hspace*{1cm} 
 $\consf$ is $\fuzzy{\cass{(a,b)}{R}}{0.3}{\leq}$ \\
& \hspace*{1cm} 
 $\consf^c = \fuzzy{\cass{(a,b)}{R}}{0.6}{\geq}$ is a conjugate of $\consf$ \\
\\
(${\existsrule}_{<}$) &
 $\fuzzy{\cass{a}{\csome R.C}}{0.8}{<},
                            \fuzzy{\cass{(a,b)}{R}}{0.9}{\geq} \Rightarrow
                            \fuzzy{\cass{b}{C}}{0.8}{<}$ \\
& \hspace*{1cm} 
 $\consf$ is $\fuzzy{\cass{(a,b)}{R}}{0.8}{<}$ \\
& \hspace*{1cm} 
 $\consf^c = \fuzzy{\cass{(a,b)}{R}}{0.9}{\geq}$ is a conjugate of $\consf$ \\
\\
(${\existsrule}_{\geq}$) & 
$\fuzzy{\cass{a}{\csome R.C}}{0.8}{\geq} \Rightarrow
                          \fuzzy{\cass{(w,x)}{R}}{0.8}{\geq}, 
                          \fuzzy{\cass{x}{C}}{0.8}{\geq}$  \\
& \hspace*{1cm} 
 $x$  new variable \\
\\
(${\allrule}_{<}$) & 
$\fuzzy{\cass{a}{\all R.C}}{0.8}{<} \Rightarrow
                          \fuzzy{\cass{(w,x)}{R}}{0.2}{>}, 
                          \fuzzy{\cass{x}{C}}{0.8}{<}$  \\
& \hspace*{1cm} 
 $x$  new variable. \\
\end{tabular}
\end{center}

\nd A set of fuzzy constraints $S$ is said to be {\em complete} if no 
rule is applicable to it.  Any complete set of fuzzy constraints $S_2$ 
obtained from a set of fuzzy constraints $S_1$ by applying the above 
rules \myref{setrules} is called a {\em completion} of $S_1$.  Due to 
the rules $({\orrule}_{\geq})$, $({\orrule}_{>})$, 
$({\andrule}_{\leq})$ and $({\andrule}_{<})$, more than one completion 
can be obtained.  These rules are called {\em nondeterministic rules}.  
All other rules are called {\em deterministic rules}.

It is easily verified that the above calculus has the \emph{termination 
property}, \ie\ any completion of a finite set of fuzzy constraints $S$ 
can be obtained after a finite number of rule applications.


\begin{exmp} \label{exx3}
{\em
Let us consider the following fuzzy KB:

\[
\FKB = \{\fuzzy{\cass{a}{\csome R.D}}{0.7}{\geq},
           \fuzzy{\cass{a}{\all R.C}}{0.4}{\geq},
           \fuzzy{\rass{a}{b}{R}}{0.5}{\geq},
           \fuzzy{\cass{b}{C}}{0.2}{\geq},
           \fuzzy{\cass{b}{D}}{0.3}{\geq} \}
\]

\nd Let $\ass$ be the assertion $\cass{a}{\csome R.(D \andc C)}$, let 
$\assf$ be the fuzzy assertion $\fuzzy{\ass}{0.4}{\geq}$, whereas let 
$\assf'$ be the fuzzy assertion $\fuzzy{\ass}{0.5}{\geq}$.  It is 
easily verified that $\FKB \entailf \assf$, whereas $\FKB \notentailf 
\assf'$.  We show that $\FKB \notentailf \assf'$, by verifying that 
there is a clash-free completion of $S = \FKB \cup 
\{\fuzzy{\cass{a}{\csome R.(D \andc C)}}{0.5}{<}\}$ (precisely, there 
are two of them).

By applying rules $(\ref{setrules})$, we have the following sequences.

%{\small
\[
\begin{array}{lll}
(1) & \fuzzy{\cass{a}{\csome R.D}}{0.7}{\geq} & \mbox{Hypothesis:} S \\
(2) & \fuzzy{\cass{a}{\all R.C}}{0.4}{\geq} & \\
(3) & \fuzzy{\cass{(a,b)}{R}}{0.5}{\geq} & \\
(4) & \fuzzy{\cass{b}{C}}{0.2}{\geq} & \\
(5) & \fuzzy{\cass{b}{D}}{0.3}{\geq} & \\
(6) & \fuzzy{\cass{a}{\csome R.(D \andc C)}}{0.5}{<} \\ \hline  
(7) & \fuzzy{\cass{(a,x)}{R}}{0.7}{\geq}, \fuzzy{\cass{x}{D}}{0.7}{\geq} &
         ({\existsrule}_{\geq}):(1) \\
% (8) & \fuzzy{\cass{b}{C}}{.6}{\geq} & 
%          ({\allrule}_{\geq}):(2),(3) \\
(8) & \fuzzy{\cass{x}{C}}{0.4}{\geq} & 
         ({\allrule}_{\geq}):(2),(7) \\
(9) & \fuzzy{\cass{b}{D \andc C}}{0.5}{<} & 
         ({\existsrule}_{<}):(3),(6) \\
(10) & \fuzzy{\cass{x}{D \andc C}}{0.5}{<} & 
         ({\existsrule}_{<}):(6),(7) \\ \hline
& \ \ \ \Omega_1 \ \ \ | \ \ \ \Omega_2
\end{array}
\]
%}

\nd
where the two sequences $\Omega_1$ and $\Omega_2$ are defined as follows: for $\Omega_1$ we
have the two sequences

{\small
\[
\begin{array}{c}
   \begin{array}{lll}
        (11) & \fuzzy{\cass{b}{D}}{0.5}{<} & 
                  ({\andrule}_{<}):(9)
   \end{array} \\ 
   \\ \hline 
   \begin{array}{l|l}
       \begin{array}[t]{lll}
         (12) & \fuzzy{\cass{x}{D}}{0.5}{<} & 
                ({\andrule}_{<}):(10)  \\
         (13) & \mbox{clash} & (7),(12)
       \end{array} &
       \begin{array}[t]{lll}
         (14) & \fuzzy{\cass{x}{C}}{0.5}{<} & 
             ({\andrule}_{<}):(10)  \\
         (15) & \mbox{clash-free} &
       \end{array}
   \end{array}
\end{array}
\]
}


\nd 
and for $\Omega_2$ we have the two sequences

{\small
\[
\begin{array}{c}
   \begin{array}{lll}
        (16) & \fuzzy{\cass{b}{C}}{0.5}{<} & 
                  ({\andrule}_{<}):(9)
   \end{array} \\ 
   \\ \hline 
   \begin{array}{l|l}
       \begin{array}[t]{lll}
         (17) & \fuzzy{\cass{x}{D}}{0.5}{<} & 
                ({\andrule}_{<}):(10)  \\
         (18) & \mbox{clash} & (7),(17)
       \end{array} &
       \begin{array}[t]{lll}
         (19) & \fuzzy{\cass{x}{C}}{0.5}{<} & 
             ({\andrule}_{<}):(10)  \\
         (20) &  \mbox{clash-free} & 
       \end{array}
   \end{array}
\end{array}
\]
}

\okex
} 
\end{exmp}


\begin{exmp} \label{extris3}
Consider Example~\ref{zadehspecex} and let us prove that 
$\FKB'' \entailf \fuzzy{(\csome {\sf About}.{\sf Car})({\sf i1})}{0.6}{\geq}$.
We prove the above relation by verifying that all completions of 
$S$ $=$ $\FKB''$ $\cup$ $\{\fuzzy{\cass{{\sf i1}}{\csome {\sf About}.{\sf Car}}}{0.6}{<}\}$ contain a clash. In fact, we have the following sequence.

{\small
\[
\begin{array}{lll}
(1) & \fuzzy{\cass{{\sf i1}}{{\sf \csome About.(Car \andc Ferrari^{*})}}}{0.6}{\geq} & \mbox{Hypothesis:} S \\
(2) & \fuzzy{\cass{{\sf i2}}{{\sf \csome About.(Car \andc Porsche^{*})}}}{0.8}{\geq} & \\

(3) & \fuzzy{\cass{{\sf i1}}{\csome {\sf About}.{\sf Car}}}{0.6}{<} \\ \hline
(4) & \fuzzy{\cass{{\sf (i1,x)}}{{\sf About}}}{0.6}{\geq}, 
      \fuzzy{\cass{{\sf x}}{{\sf (Car \andc Ferrari^{*})}}}{0.6}{\geq} & 
           (\existsrule_{\geq}):(1) \\	   
(5) & \fuzzy{\cass{{\sf x}}{{\sf Car}}}{0.6}{<} &
         ({\existsrule}_{<}):(3),(4) \\
		 
(6) & \fuzzy{\cass{{\sf x}}{{\sf Car}}}{0.6}{\geq},  \fuzzy{\cass{{\sf x}}{{\sf Ferrari^{*}}}}{0.6}{\geq},  &
         (\andrule):(4) \\
(7) & \mbox{clash} & (5),(6)
\end{array}
\]
}

\okex
\end{exmp}

\begin{prop} \label{p7}
A finite set of fuzzy constraints $S$ is satisfiable iff there exists a clash
free completion of $S$. \ok
\end{prop}


\begin{pf}
	
$\Rightarrow.)$ Given the termination property, it is easily verified, 
by case analysis, that the above rules are sound, \ie~if $S_1$ is 
satisfiable then there is a satisfiable completion $S_2$ of $S_1$ and, 
thus, $S_2$ contains no clash.  For instance, let us show that the 
(${\allrule}_{\geq}$) rule is sound.  Assume $\I$ is an interpretation 
satisfying $\fuzzy{\cass{w_1}{\all R.C}}{n}{\geq}$ and 
$\fuzzy{\cass{(w_1,w_2)}{R}}{m}{\geq}$, where $m > 1-n$.  Let us show 
that $\I$ satisfies $\fuzzy{\cass{w_2}{C}}{n}{\geq}$.  Since $\I$ 
satisfies $\fuzzy{\cass{w_1}{\all R.C}}{n}{\geq}$ it follows that 
$\max\{1- \highi{R}(\highi{w_{1}}, \highi{w_{2}}), 
\highi{C}(\highi{w_{2}}) \} \geq n$.  But, $\highi{R}(\highi{w_{1}}, 
\highi{w_{2}}) \geq m$ and, thus, $1- \highi{R}(\highi{w_{1}}, 
\highi{w_{2}}) \leq 1 - m < n$.  As a consequence, 
$\highi{C}(\highi{w_{2}}) \geq n$ follows, \ie\ $\I$ satisfies 
$\fuzzy{\cass{w_2}{C}}{n}{\geq}$.

	
$\Leftarrow.)$ Suppose that there exists a clash free completion $S'$ 
of $S$.  We build from $S'$ an interpretation $\I$ satisfying $S'$ 
and, as $S \subseteq S'$, $\I$ satisfies $S$.  $\I$ is called 
\emph{canonical model}.
	
For any primitive constraint $\cons \in S'$, we collect its lower and 
upper bound restrictions in $S'$ as follows: let
\begin{eqnarray*}
		N^{\geq}[\cons] & = & \{n: \fuzzy{\cons}{n}{\geq} \in S'\} \label{n1} \\
		N^{>}[\cons] & = & \{n: \fuzzy{\cons}{n}{>} \in S' \} \label{n2} \\
		N^{\leq}[\cons] & = & \{n: \fuzzy{\cons}{n}{\leq} \in S'\}  \label{n3} \\
		N^{<}[\cons] & = & \{n: \fuzzy{\cons}{n}{<} \in S' \}.   \label{n4}
\end{eqnarray*}

\nd We have to define $\I$ such that for each constraint $\cons$, $\I$ 
satisfies the constraints collected in the sets $N^{(\cdot)}[\cons]$: 
given $N^{\geq}[\cons]$, the truth value $n$ of $\cons$ under $\I$ has 
to be such that $n \geq \max N^{\geq}[\cons]$, whereas \wrt\ 
$N^{>}[\cons]$, the truth value $n$ of $\cons$ under $\I$ has to be 
such that $n \geq \max N^{>}[\cons] + \epsilon$, for a $\epsilon > 0$.  
Similarly, for the other cases, for instance, \wrt\ $N^{<}[\cons]$, the 
truth value $n$ of $\cons$ under $\I$ has to be such that $n \leq \max 
N^{>}[\cons] - \epsilon$, for a $\epsilon > 0$.  The two tables below
\[
\begin{array}{|c|c|c|} \hline
	N^{\geq}[\cons] & N^{>}[\cons] & glb[\cons,\epsilon] \\ \hline
	\emptyset & \emptyset & 0  \\ \hline
	\emptyset & \neq\emptyset & n' + \epsilon \\ \hline
	\neq\emptyset & \emptyset &  n   \\ \hline
	 \neq\emptyset & \neq\emptyset & \mbox{ if } n> n' \mbox{ then } n 
	 \mbox{ else } n' + \epsilon \\ \hline
\end{array}
\]

\[
\begin{array}{|c|c|c|} \hline
	N^{\leq}[\cons] & N^{<}[\cons] & lub[\cons,\epsilon] \\ \hline
	\emptyset & \emptyset & 1  \\ \hline
	\emptyset & \neq\emptyset & m' - \epsilon \\ \hline
	\neq\emptyset & \emptyset &  m   \\ \hline
	 \neq\emptyset & \neq\emptyset & \mbox{ if } m< m' \mbox{ then } m 
	 \mbox{ else } m' - \epsilon \\ \hline
\end{array}
\]
define for any $\cons \in S'$ and $\epsilon > 0$, 
$lub[\cons,\epsilon]$ and $glb[\cons,\epsilon]$, the lower and upper 
bound constraints which $\I$ has to satisfy.  In the tables, with 
$n,n', m,m'$ we indicate $ \max N^{\geq}[\cons]$, $\max N^{>}[\cons]$, 
$\min N^{\leq}[\cons]$ and $\min N^{<}[\cons]$, respectively.  In each 
table we distinguish between the four cases where the sets are empty 
(no constraints) or not.  For instance, if for a constraint 
$\cass{w}{A}$, only $\fuzzy{\cass{w}{A}}{0.3}{\geq}$, 
$\fuzzy{\cass{w}{A}}{0.4}{>}$, $\fuzzy{\cass{w}{A}}{0.5}{\leq}$ and 
$\fuzzy{\cass{w}{A}}{0.6}{<}$ are in $S'$, then according to the first 
table bellow (row 4), for a $\epsilon >0$, $glb[\cass{w}{A}, 
\epsilon] = 0.4 + \epsilon$, whereas $lub[\cass{w}{A}, \epsilon] = 
0.5$.

We will define $\I$ such that $\highi{A}(\highi{w}) = 
glb[\cass{w}{A},\epsilon]$.  To make sure that $ glb[\cass{w}{A}, 
\epsilon] \leq \highi{A}(\highi{w}) \leq lub[\cass{w}{A}, \epsilon]$, 
we have to choose an $\epsilon > 0$ small enough such that 
$glb[\cass{w}{A}, \epsilon] \leq lub[\cass{w}{A}, \epsilon]$, \ie\ 
$0.4 + \epsilon \leq 0.5$.  The existence of such an $\epsilon > 0$ is 
guaranteed by the fact that $S'$ is clash-free.  An additional 
condition that the choice of such an $\epsilon$ has to satisfy 
concerns the case of a constraint $\cons$ of type $\rass{w}{w'}{R}$.  
Let us show the problem with an example.  Suppose $S'$ is 
$\{\fuzzy{\cass{(w,w')}{R}}{0.3}{>}, \fuzzy{\cass{w}{\all 
R.B}}{0.6}{\geq}, \fuzzy{\cass{w'}{B}}{0.5}{\leq} \}$.  Therefore, 
according to the above tables, $glb[\cass{(w,w')}{R},\epsilon_{1}] = 
0.3 + \epsilon_{1}$, $lub[\cass{(w,w')}{R},\epsilon_{1}] = 1$, 
$glb[\cass{w'}{B},\epsilon_{2}] = 0$ and 
$lub[\cass{w'}{B},\epsilon_{2}] = 0.5$.  So, it seems that it is 
sufficient to choose an $\epsilon_{1} >0$ such that $0.3 + 
\epsilon_{1} \leq 1$, which is indeed not the case.  In fact, 
$\fuzzy{\cass{w}{\all R.B}}{0.6}{\geq}$ and 
$\fuzzy{\cass{w'}{B}}{0.5}{\leq}$ introduces an upper bound on 
$\cass{(w,w')}{R}$, \ie\ the truth-value of $\cass{(w,w')}{R}$ under 
$\I$ has to be less or equal to $0.4 = 1- 0.6$.  That is, we have to 
choose an $\epsilon_{1} >0$ such that $0.3 + \epsilon_{1} \leq 0.4$.  
Otherwise, the truth-value of $\cass{w'}{B}$ under $\I$ has to be greater 
or equal to $0.6$, contradicting $lub[\cass{w'}{B},\epsilon_{2}] = 
0.5$.  Again, the existence of such an $\epsilon$ is guaranteed as 
$S'$ is clash-free.

Summing up: since $S'$ is clash-free, it follows that for each primitive 
constraint $\cons$, there is $\epsilon[\cons] > 0$ such that 

\[
glb[\cons,\epsilon[\cons]] \leq lub[\cons,\epsilon[\cons]]
\]

\nd
where if $\cons$ is $\rass{w}{w'}{R}$ then
\begin{equation}\label{epsall}
\begin{array}{l}
\mbox{for each $\fuzzy{\cass{w}{\all R.C}}{n}{\geq}$, if 
$\fuzzy{\cass{w'}{C}}{n}{\geq} \not\in S'$ then $glb[\cons,\epsilon[\cons]] \leq 1-n$;} \\
\mbox{for each $\fuzzy{\cass{w}{\all R.C}}{n}{>}$, 
if $\fuzzy{\cass{w'}{C}}{n}{>} \not\in S'$ then $glb[\cons,\epsilon[\cons]] < 1-n$;} \\
\mbox{for each $\fuzzy{\cass{w}{\csome R.C}}{n}{\leq}$, if 
$\fuzzy{\cass{w'}{C}}{n}{\leq} \not\in S'$ then $glb[\cons,\epsilon[\cons]] \leq n$;} \\
\mbox{for each $\fuzzy{\cass{w}{\csome R.C}}{n}{<}$, if 
$\fuzzy{\cass{w'}{C}}{n}{<} \not\in S'$ then $glb[\cons,\epsilon[\cons]] < n$.}
\end{array}
\end{equation}

\nd Now, consider the following interpretation $\I$ such that

\begin{enumerate}
	\item the domain $\highi{\Delta}$ is the set of objects appearing 
	in $S'$;
	
	\item $\highi{w} = w$, for all $w \in \highi{\Delta}$; 
	
	\item $\highi{\topc}(\highi{w}) = 1$ and 
	$\highi{\bottomc}(\highi{w}) = 0$, for all $w \in \highi{\Delta}$;
	
	\item $\highi{A}(\highi{w}) = 
	glb[\cass{w}{A},\epsilon[\cass{w}{A}]]$, for all primitive 
	concepts $A$ and for all $w \in \highi{\Delta}$; and

	\item $\highi{R}(\highi{w},\highi{w'}) = 
	glb[\cass{(w,w')}{R},\epsilon[\cass{(w,w')}{R}]]$, for all roles 
	$R$ and for all $w, w' \in \highi{\Delta}$.
\end{enumerate}

\nd We show, on induction on the structure of fuzzy constraints $\psi 
\in S'$, that $\I$ satisfies $S'$.

\paragraph{Case $\fuzzy{\cass{w}{A}}{n}{>}$:}
By definition, $\highi{A}(\highi{w}) = 
glb[\cass{w}{A},\epsilon[\cass{w}{A}]] > n$ and, thus, $\I$ satisfies 
$\fuzzy{\cass{w}{A}}{n}{>}$.  The cases $\geq, \leq$ and $<$ are 
similar.

\paragraph{Case $\fuzzy{\rass{w}{w'}{R}}{n}{\geq}$:}
By definition, $\highi{R}(\highi{w},\highi{w'}) = 
glb[\cass{(w,w')}{R},\epsilon[\cass{(w,w')}{R}]] \geq n$ and, thus, 
$\I$ satisfies $\fuzzy{\rass{w}{w'}{R}}{n}{\geq}$.  The cases $>, 
\leq$ and $<$ are similar.

\paragraph{Case $\fuzzy{\cass{w}{C \andc D}}{n}{\geq}$:}
From $\fuzzy{\cass{w}{C \andc D}}{n}{\geq} \in S'$ and $S'$ completed, 
$\fuzzy{\cass{w}{C}}{n}{\geq} \in S'$ and 
$\fuzzy{\cass{w}{D}}{n}{\geq} \in S'$ follows.  By induction, $\I$ 
satisfies both $\fuzzy{\cass{w}{C}}{n}{\geq}$ and 
$\fuzzy{\cass{w}{D}}{n}{\geq}$ and, thus, $\I$ satisfies 
$\fuzzy{\cass{w}{C \andc D}}{n}{\geq}$.  The cases $>, \leq$ and $<$ 
are similar.

\nd
The cases involving $\notc C$ and $C \orc D$ can be shown similarly.

\paragraph{Case $\fuzzy{\cass{w}{\all R.C}}{n}{\geq}$:} 
Let $\ass$ be $\rass{w}{w'}{R}$ and consider 
$\fuzzy{\cass{w'}{C}}{n}{\geq}$.  It follows that, either \ii{i} 
$\fuzzy{\cass{w'}{C}}{n}{\geq} \in S'$; or \ii{ii} 
$\fuzzy{\cass{w'}{C}}{n}{\geq} \not\in S'$.  Case \ii{i}: by 
induction, $\I$ satisfies $\fuzzy{\cass{w'}{C}}{n}{\geq}$ and, thus, 
$\max\{1- \highi{R}(w,w'), \highi{C}(w') \} \geq \highi{C}(w') \geq 
n$.  Case \ii{ii}: by construction $\highi{R}(w,w') = 
glb[\cass{(w,w')}{R},\epsilon[\cass{(w,w')}{R}]]$ and $\highi{R}(w,w') 
\leq 1-n$ (see Equation~\ref{epsall}).  It follows that $\max\{1- 
\highi{R}(w,w'), \highi{C}(w') \} \geq 1- \highi{R}(w,w') \geq n$.  
Therefore, $\inf_{w'\in \highi{\Delta}}\max\{1- \highi{R}(w,w'), 
\highi{C}(w') \} \geq n$, \ie\ $\I$ satisfies $\fuzzy{\cass{w}{\all 
R.C}}{n}{\geq}$.

The cases $\fuzzy{\cass{w}{\all R.C}}{n}{>}, 
\fuzzy{\cass{w}{\csome R.C}}{n}{\leq}$ and $\fuzzy{\cass{w}{\csome 
R.C}}{n}{<}$ can be shown similarly.

\paragraph{Case $\fuzzy{\cass{w}{\csome R.C}}{n}{\geq}$:} Since $S'$ 
is complete, both $\fuzzy{\rass{w}{w'}{R}}{n}{\geq}$ and 
$\fuzzy{\cass{w'}{C}}{n}{\geq}$ are in $S'$.  By induction, $\I$ 
satisfies both $\fuzzy{\rass{w}{w'}{R}}{n}{\geq}$ and 
$\fuzzy{\cass{w'}{C}}{n}{\geq}$.  As a consequence, 
$\min\{\highi{R}(w,w'), \highi{C}(w') \} \geq n$ follows and, thus, 
$\sup_{w'\in \highi{\Delta}}\min\{\highi{R}(w,w'), \highi{C}(w') \} 
\geq n$, \ie\ $\I$ satisfies $\fuzzy{\cass{w}{\csome R.C}}{n}{\geq}$.

The cases $\fuzzy{\cass{w}{\csome R.C}}{n}{>}, \fuzzy{\cass{w}{\all 
R.C}}{n}{\leq}$ and $\fuzzy{\cass{w}{\all R.C}}{n}{<}$ can be shown 
similarly. \qed
\end{pf}


\nd
The following example shows how such an interpretation is build.

\begin{exmp} \label{ex4}
{\em
Let us consider Example~\ref{exx3} and the fuzzy assertion $\assf'$. 
We have shown that $\FKB \notentailf \assf'$ by constructing two 
clash-free completions from $S$. Let us consider the clash-free 
completion $S_{1}$ in branch $\Omega_{1}$:

\[
S_1 = \FKB \cup \{\begin{array}[t]{l}         
         \fuzzy{\cass{a}{\csome R.(D \andc C)}}{0.5}{<}, 
         \fuzzy{\cass{(a,x)}{R}}{0.7}{\geq}, 
         \fuzzy{\cass{x}{D}}{0.7}{\geq},
         \fuzzy{\cass{x}{C}}{0.4}{\geq}, \\
		 \fuzzy{\cass{b}{D \andc C}}{0.5}{<},
 		 \fuzzy{\cass{x}{D \andc C}}{0.5}{<},
         \fuzzy{\cass{b}{D}}{0.5}{<},
         \fuzzy{\cass{x}{C}}{0.5}{<} \}
        \end{array}
\]

\nd
We show that $S_1$ is satisfiable by building an interpretation as described 
in the proof of Proposition~\ref{p7}.
Accordingly, for $\epsilon_{i} > 0$,

\[
\begin{array}{cc}
\begin{array}{lcl}
glb[\cass{(a,b)}{R}, \epsilon_{1}] & = & 0.5    \\
glb[\cass{b}{C}, \epsilon_{2}]     & = & 0.2    \\
glb[\cass{b}{D}, \epsilon_{3}]     & = & 0.3   \\
glb[\cass{(a,x)}{R}, \epsilon_{4}] & = & 0.7    \\
glb[\cass{x}{D}, \epsilon_{5}]     & = & 0.7     \\
glb[\cass{x}{C}, \epsilon_{6}]     & = & 0.4  
\end{array} &
\begin{array}{lcl}
lub[\cass{(a,b)}{R}, \epsilon_{1}] & = & 1    \\
lub[\cass{b}{C}, \epsilon_{2}]     & = & 1    \\
lub[\cass{b}{D}, \epsilon_{3}]     & = & 0.5 - \epsilon_{3}   \\
lub[\cass{(a,x)}{R}, \epsilon_{4}] & = & 1    \\
lub[\cass{x}{D}, \epsilon_{5}]     & = & 1     \\
lub[\cass{x}{C}, \epsilon_{6}]     & = & 0.5 - \epsilon_{6} . 
\end{array}
\end{array}
\]


\nd Therefore, we can freely choose $\epsilon_{2}, \epsilon_{4}$ and 
$\epsilon_{5}$, whereas $\epsilon_{3}$ and $\epsilon_{6}$ have to be 
such that $0.3 \leq 0.5 - \epsilon_{3}$ and $0.4 \leq 0.5 - 
\epsilon_{6}$.  As both $\fuzzy{\cass{(a,b)}{R}}{0.5}{\geq}$ and 
$\fuzzy{\cass{a}{\all R.C}}{0.4}{\geq}$ are in $S_{1}$, while 
$\fuzzy{\cass{b}{C}}{0.4}{\geq} \not\in S_{1}$, we have the additional 
restriction on the choice of $\epsilon_{1}$ (see 
Equation~\ref{epsall}) that $glb[\cass{(a,b)}{R}, \epsilon_{1}] \leq 
0.6$.  But, $glb[\cass{(a,b)}{R}, \epsilon_{1}] = 0.5 \leq 0.6$, for 
every $\epsilon_{1}$ and, thus, the choice of $\epsilon_{1}$ is also 
free.  A solution to the $\epsilon_{i}$ is \eg\ $\epsilon_{i} = 0.1$ 
and, thus, let $\I$ be the following interpretation:

\begin{enumerate}
\item
the domain $\highi{\Delta}$ is the set $\{a,b,x\}$;
\item
$\highi{w} = w$, for all $w \in \highi{\Delta}$; 
\item
$\highi{\topc}(\highi{w}) = 1$ and $\highi{\bottomc}(\highi{w}) = 0$, for all 
$w \in \highi{\Delta}$;
\item
$\highi{C}(b) = 0.2$, 
$\highi{D}(b) = 0.3$,
$\highi{D}(x) = 0.7$ and
$\highi{C}(x) = 0.4$
(in all other cases, $\highi{A}(w) = 0$); and
\item
$\highi{R}(a,b) = 0.5$ and
$\highi{R}(a,x) = 0.7$ 
(in all other cases, $\highi{R'}(w,w') = 0$).
\end{enumerate}

\nd
Now, it is easily verified that $\I$ satisfies $S_1$ and $S$.
} \okex
\end{exmp}

\nd From a computational complexity point of view, the fuzzy 
entailment problem can be proven to be a PSPACE-complete problem, as is 
the classical entailment problem.

\begin{prop} \label{p8} 
Let $\FKB$ be a fuzzy KB and let $\assf$ be a fuzzy assertion.
Determining whether $\FKB \entailf \assf$ is a PSPACE-complete problem. \ok  
\end{prop}

\begin{pf}
We have seen that termination of the above algorithm is guaranteed.  
Additionally, for a crisp KB $\KB$, define $\FKB_{\KB}$ $=$ 
$\{\fuzzy{\ass}{1}{\geq}: \ass \in \KB \}$.  By definition, each $\psi 
\in \FKB_{\KB}$ is KB-normalised and $ \fuzzy{\ass}{0.5}{\geq}$ is 
query-normalised.  Then from Proposition~\ref{p3} it follows that $\KB 
\entail \ass$ iff $\FKB_{\KB} \entailf \fuzzy{\ass}{0.5}{\geq}$.  From 
the PSPACE-completeness of the entailment problem in crisp \alc \ 
\cite{Schmidt-Schauss91}, PSPACE-hardness of the fuzzy entailment 
problem follows.  Unfortunately, our algorithm, as it is, requires 
exponential space due a well know problem inherited from the crisp 
case.  Indeed, it easily verified that a completion of $S= 
\{\cass{x}{C}\}$, where $C$ is the concept

\[
(\csome R.A_{11}) \andc (\csome R.A_{12}) \andc
\all R.((\csome R.A_{21}) \andc (\csome R.A_{22}) \andc \ldots
\all R.((\csome R.A_{n1}) \andc (\csome R.A_{n2})) \ldots)  
\]


\nd contains at least $2^{n} + 1$ variables.  In order to require 
polynomial space, Schmidt-Schau\ss \ and Smolka (1991) %\cite{Schmidt-Schauss91} 
introduced the so-called 
{\em trace rule} $(T\existsrule)$ for the $\csome$ operator.  The 
$(T\existsrule)$ rule modifies the $(\existsrule)$ rule as shown 
below.

\[
\begin{tabular}{ll}
(${\existsrule}$) & $\cass{w}{\csome R.C} \rightarrow
                         \cass{(w,x)}{R}, \cass{x}{C}$ \\
   & \hspace*{.5cm} if $x$  new variable and there is no $w'$ such 
   that both $\cass{(w,w')}{R}$ and $\cass{w'}{C}$ \\ 
   & \hspace*{.5cm} are already in the actual constraint set \\
(${T\existsrule}$) & $\cass{w}{\csome R.C} \rightarrow
                         \cass{(w,x)}{R}, \cass{x}{C}$ \\
   & \hspace*{.5cm} if $x$  new variable and no $\rass{w}{w'}{R'}$ is already in the 
   actual set of constraints.
\end{tabular}
\]

\nd The difference between the $(\existsrule)$ rule and the 
$(T\existsrule)$ is that the latter is applied only once for an object 
$w$.  We are thus compelled to make a nondeterministic choice amongst 
the constraints of the form $\cass{w}{\csome R.C}$.  Furthermore, it 
is convenient to apply a trace rule only if none of the other 
$(\andc), (\orc), (\notc)$ and $(\all)$ rules are applicable.

We say that a set of constraints $S'$ is a \emph{trace} of a set $S$ 
if $S'$ obtained from $S$ by application of the rules where the 
$(\existsrule)$ has been replaced by $(T\existsrule)$.  
Schmidt-Schau\ss \ and Smolka (1991) %\cite{Schmidt-Schauss91} 
have shown that a set of constraints 
$S=\{\cass{x}{C}\}$ is satisfiable iff no trace $S'$ of $S$ contains a 
clash.  As the size of a trace $S'$ of $S$ is bounded polynomially by 
the size of $S$, polynomial space is sufficient to prove 
satisfiability.

The above trace rule works if we start from a 
constraint set of the form $\{\cass{x}{C}\}$.  In the general case, we 
have to rely on so-called \emph{pre-completions} 
\cite{Baader91c,Donini94c}.  A set of constraints $S'$ is said to be a 
\emph{pre-completion} of a given set of constraints $S$, if it is 
obtained from $S$ by the application of the $(\andc), (\orc), (\notc)$ 
and $(\all)$ rules, and none of these rules is applicable to $S'$ (the 
size of $S'$ is polynomially bounded by the size of $S$).  As a 
consequence of this ``pre-processing'' step, all role relationships 
$\cass{(w,w')}{R} \in S'$ can be ignored, \ie\ removed from $S'$, 
because they no longer carry any additional information.  Now, in a 
second step we can apply the method above by checking whether no trace 
from $S'$ contains a clash.  In summary, a set of constraints $S$ is 
satisfiable iff there is a pre-completion $S'$ of $S$ such that no 
trace $S''$ of $S'$ contains a clash.

In the fuzzy case, similar trace rules can easily be defined.  For 
instance, the correspondent trace rule of the $({\existsrule}_{\geq})$ 
rule is


\[
\begin{tabular}{ll}
(${T\existsrule}_{\geq}$) & $\fuzzy{\cass{w}{\csome R.C}}{n}{\geq} \rightarrow
                           \fuzzy{\cass{(w,x)}{R}}{n}{\geq}, \fuzzy{\cass{x}{C}}{n}{\geq}$ \\
   & \hspace*{.5cm} if $x$ new variable and no 
   $\fuzzy{\cass{(w,w')}{R'}}{m}{\geq}$ is already in \\
   & \hspace*{.5cm} the actual set of fuzzy constraints.
\end{tabular}
\]

\nd The trace rules correspondent to the rules (${\existsrule}_{>}$), 
(${\allrule}_{\leq}$) and (${\allrule}_{<}$) are defined similarly.  
By proceeding as for the crisp case, it can be shown that \ii{i} a set 
of fuzzy constraints $S$ is satisfiable iff there is a pre-completion 
$S'$ of $S$ such that no trace $S''$ of $S'$ contains a clash; and 
\ii{ii} the size of a trace $S''$ of $S$ is bounded polynomially by the 
size of $S$.  As a consequence, the satisfiability problem is in 
PSPACE, which completes the proof.  \qed
\end{pf}


\nd This result establishes an important property about our fuzzy DL. 
In effect, it says that no additional computational cost has to be 
paid for the major expressive power.

%------------------------------ COMPUTING subs -------
\subsection{A Decision Procedure for the Subsumption Problem}  
\label{subprob}
%--------------------------------------------------------

\nd In this section we address the subsumption problem, \ie\ deciding 
whether $C \subsf_{\FKB_{T}} D$, where $C$ and $D$ are two concepts 
and $\FKB$ is a fuzzy terminology.  As we have seen (see 
Example~\ref{zadehspecex}), $C \subsf_{\FKB_{T}} D$ can be reduced to 
the case of an empty terminology by applying the KB expansion 
process.  So, without loss of generality, we can limit our attention 
to the case $C \subsf_{\emptyset} D$.

At first, an analogue to relation \myref{pbb7} holds.  In 
fact, it can easily be shown that

\begin{prop}\label{p4}
Let $C$ and $D$ be two concepts. It follows that
$C \subsf_{\emptyset} D$ iff for all $n> 0$  
$\fuzzy{\cass{a}{C}}{n}{\geq} \entailf \fuzzy{\cass{a}{D}}{n}{\geq}$, 
where $a$ is a new individual. \ok
\end{prop}

\begin{pf}
	
$\Rightarrow.)$ Assume that $C \subsf_{\emptyset} D$ holds.  Suppose 
to the contrary that $\exists n > 0$ such that 
$\fuzzy{\cass{a}{C}}{n}{\geq} \notentailf 
\fuzzy{\cass{a}{D}}{n}{\geq}$.  Therefore, there is an interpretation 
$\I$ and an $n >0$ such that $\highi{C}(\highi{a}) \geq n$ and 
$\highi{D}(\highi{a}) < n$.  But, from the hypothesis $n \leq 
\highi{C}(\highi{a}) \leq \highi{D}(\highi{a}) < n$ follows.  Absurd.

$\Leftarrow.)$ Assume that for all $n> 0$, 
$\fuzzy{\cass{a}{C}}{n}{\geq} \entailf \fuzzy{\cass{a}{D}}{n}{\geq}$ 
holds.  Suppose to the contrary that $C \not\subsf_{\emptyset} D$ 
holds.  Therefore, there is an interpretation $\I$ and $d \in 
\highi{\Delta}$ such that $\highi{C}(d) > \highi{D}(d) \geq 0$.  Let us 
extent $\I$ to $a$ such that $\highi{a}=d$ and consider $\overline{n} 
= \highi{C}(d) >0$.  Of course, $\I$ satisfies 
$\fuzzy{\cass{a}{C}}{\overline{n}}{\geq}$.  Therefore, from the 
hypothesis it follows that $\I$ satisfies 
$\fuzzy{\cass{a}{D}}{\overline{n}}{\geq}$, \ie\ $\highi{D}(d) \geq 
\overline{n} = \highi{C}(d) > \highi{D}(d)$.  Absurd.  \qed
\end{pf}

\nd How can we check whether for all $n> 0$ 
$\fuzzy{\cass{a}{C}}{n}{\geq} \entailf \fuzzy{\cass{a}{D}}{n}{\geq}$ 
holds?  A solution to this problem, restricted to the propositional 
case, is given by Straccia (2000a). %\cite{Straccia00b}.  
Indeed, it is shown that

\begin{prop}[Straccia, 2000a]\label{p9a} %[\cite{Straccia00b}]\
Let $p$ and $q$ be two propositions, $0 < n_{1} \leq 0.5$ and $1 \geq n_{2} 
>0.5$.  It follows that for all $n>0$, $\fuzzy{p}{n}{\geq} \entailf 
\fuzzy{q}{n}{\geq}$ iff for both $m \in \{n_{1},n_{2}\}$, 
$\fuzzy{p}{m}{\geq} \entailf \fuzzy{q}{m}{\geq}$ holds.  \ok
\end{prop}

\nd The above proposition establishes that, at the propositional 
level, in order to check whether $\fuzzy{p}{n}{\geq} \entailf 
\fuzzy{q}{n}{\geq}$ holds for all $n$, it is sufficient to check the 
entailment relation with respect to two values $n_{1}, n_{2}$.  The 
first being less or equal than $0.5$, while the second being greater than 
$0.5$, respectively.  This is due to the fact that for given values 
$n,n' \leq 0.5$, any proof of $\fuzzy{p}{n}{\geq} \entailf 
\fuzzy{q}{n}{\geq}$ can be converted into a proof for 
$\fuzzy{p}{n'}{\geq} \entailf \fuzzy{q}{n'}{\geq}$ and vice-versa. 
The case where $n,n' > 0.5$ is similar.

The above proposition can be extended to our fuzzy DL as well.

\begin{lem}\label{l1}
Let $C$ and $D$ be two concepts, $0< n,n' \leq 0.5$ and let $a$ be an 
individual.  It follows that $\fuzzy{\cass{a}{C}}{n}{\geq} \entailf 
\fuzzy{\cass{a}{D}}{n}{\geq}$ iff $\fuzzy{\cass{a}{C}}{n'}{\geq} 
\entailf \fuzzy{\cass{a}{D}}{n'}{\geq}$.  \ok
\end{lem}

\begin{pf}
It is enough to show that 
$S = \{\fuzzy{\cass{a}{C}}{n}{\geq},\fuzzy{\cass{a}{D}}{n}{<}\}$ is 
satisfiable iff 
$S' = \{\fuzzy{\cass{a}{C}}{n'}{\geq},\fuzzy{\cass{a}{D}}{n'}{<}\}$ is 
satisfiable.  

$\Rightarrow.)$ Assume that $S$ is satisfiable.  So, there is a 
clash-free completion $\tilde{S}$ of $S$.  With $\tilde{S}[n/n']$ we 
indicate the set of fuzzy constraints obtained from $\tilde{S}$, by 
replacing any value $n$ in $\tilde{S}$ with $n'$ and any value $1-n$ 
in $\tilde{S}$ with $1-n'$, respectively.  We will show that 
$\tilde{S}[n/n']$ is a clash-free completion of $S'$ and, thus, $S'$ 
is satisfiable.

Let $r_{1}, \ldots ,r_{k}$, $k \geq 0$ be the sequence of inference rule 
applications, which applied to $S$ get $\tilde{S}$.  Let 
$\tilde{S}_{0}=S$, let $\tilde{S}_{k}=\tilde{S}$ and for $1 \leq i 
\leq k$ let $\tilde{S}_{i}$ be the set of fuzzy constraints obtained 
from $\tilde{S}_{i-1}$ by the application of the $r_{i}$ rule to 
$\tilde{S}_{i-1}$.

By induction on $k$, we show that \ii{i} the sequence of inference 
rules $r_{1}, \ldots , r_{k}$ can be applied to $S'$ as well; \ii{ii} 
for $\tilde{S'}_{0}=S'$, $\tilde{S'}_{k}=\tilde{S'}$ and 
$\tilde{S'}_{i}$ the set of fuzzy constraints obtained from 
$\tilde{S'}_{i-1}$ by the application of the $r_{i}$ rule to 
$\tilde{S'}_{i-1}$, we have that $\tilde{S'}_{i}= \tilde{S}_{i}[n/n']$ 
and, thus, $\tilde{S'} = \tilde{S'}_{k} = \tilde{S}_{k}[n/n'] = 
\tilde{S}[n/n']$; and \ii{iii} if $\tilde{S}_{k}$ is a clash-free 
completion of $S$ then $\tilde{S'}_{k}$ is a clash-free completion of 
$S'$ as well.


\begin{description}
\item[case $k =0$:] No rule is applicable to $S$ and $\tilde{S}_{0} = 
S$ is a completion of $S$.  By case analysis, \ii{i} it is easily 
verified that no rule is applicable to $S'$ and \ii{ii} 
$S' = \tilde{S'}_{0} = \tilde{S}_{0}[n/n'] = S[n/n']$.  \ii{iii} So, 
$\tilde{S'}_{0}$ is a completion of $S'$.  We show that 
$\tilde{S'}_{0}$ is clash-free.  Assume to the contrary that 
$\tilde{S'}_{0}$, \ie\ $S'$ contains a clash.  As a consequence, $S' = 
\{\fuzzy{\cass{a}{C}}{n'}{\geq},\fuzzy{\cass{a}{C}}{n'}{<}\}$.  But 
then, $S$ is 
$\{\fuzzy{\cass{a}{C}}{n}{\geq},\fuzzy{\cass{a}{C}}{n}{<}\}$, contrary 
to the assumption that $S$ is clash-free.
	
\item[induction step:] by case analysis on the rule $r_{k}$. We limit 
our presentation to the $(\all_{\geq})$ rule as for the other the 
proof is similar.

If $r_{k}$ is $(\all_{\geq})$ then it can be verified that there are 
$\fuzzy{\cass{w}{\all R.C'}}{n}{\geq}$ and 
$\fuzzy{\rass{w}{w'}{R}}{1-n}{>}$ in $\tilde{S}_{k-1}$ such that 
$\fuzzy{\cass{w'}{C'}}{n}{\geq} \not\in \tilde{S}_{k-1}$ and 
$\fuzzy{\cass{w'}{C'}}{n}{\geq} \in \tilde{S}_{k}$.  By induction, 
$\tilde{S}_{k-1}[n/n']= \tilde{S'}_{k-1}$ and, thus, both 
$\fuzzy{\cass{w}{\all R.C'}}{n'}{\geq}$ and 
$\fuzzy{\rass{w}{w'}{R}}{1-n'}{>}$ are in $\tilde{S'}_{k-1}$, while 
$\fuzzy{\cass{w'}{C'}}{n'}{\geq} \not\in \tilde{S'}_{k-1}$.  
Therefore, \ii{i} rule $r_{k}$ is applicable to $\tilde{S'}_{k-1}$ and 
$\fuzzy{\cass{w'}{C'}}{n'}{\geq} \in \tilde{S'}_{k}$; \ii{ii} so, 
$\tilde{S'}_{k} = \tilde{S}_{k}[n/n']$; \ii{iii} from $\tilde{S'}_{k} 
= \tilde{S}_{k}[n/n']$ and, as $\tilde{S}_{k}$ is a completion of $S$, 
by case analysis, it is easily verified that no rule is further 
applicable to $\tilde{S'}_{k}$.  Therefore, $\tilde{S'}_{k}$ is a 
completion of $S'$.  Let us show that $\tilde{S'}_{k}$ is clash free.  
Assume to the contrary that $\tilde{S'}_{k}$ contains a clash.  If one 
of the cases in Table~\ref{clashcons} holds, then from $\tilde{S'}_{k} 
= \tilde{S}_{k}[n/n']$ it follows easily that there is a clash in 
$\tilde{S}_{k}$ as well, which is contrary to assumption that 
$\tilde{S}_{k}$ is clash-free.  On the other hand, if there is a 
conjugated pair of fuzzy constraints in $\tilde{S'}_{k}$ (see 
Table~\ref{tabconj}), then one of the following three pairs is in 
$\tilde{S'}_{k}$: (a) $\fuzzy{\ass}{n'}{\geq}$ and 
$\fuzzy{\ass}{n'}{<}$; (b) $\fuzzy{\ass}{1-n'}{\leq}$ and 
$\fuzzy{\ass}{1-n'}{>}$; and (c) $\fuzzy{\ass}{n'}{<}$ and 
$\fuzzy{\ass}{1-n'}{>}$ (note that $n,n' \leq 0.5$).  Again, as 
$\tilde{S'}_{k} = \tilde{S}_{k}[n/n']$, it follows that there is a 
conjugated pair in $\tilde{S}_{k}$ as well, which is contrary to 
assumption that $\tilde{S}_{k}$ is clash-free.
\end{description}

$\Leftarrow.)$ Can be proven similarly to $\Rightarrow.)$. \qed
\end{pf}

\nd
By proceeding as for Lemma~\ref{l1} it can be shown that

\begin{lem}\label{l2}
Let $C$ and $D$ be two concepts, $1 \geq n,n' > 0.5$ and let $a$ be an 
individual.  It follows that $\fuzzy{\cass{a}{C}}{n}{\geq} \entailf 
\fuzzy{\cass{a}{D}}{n}{\geq}$ iff $\fuzzy{\cass{a}{C}}{n'}{\geq} 
\entailf \fuzzy{\cass{a}{D}}{n'}{\geq}$.  \ok
\end{lem}

\nd
From Lemma~\ref{l1} and Lemma~\ref{l2} it follows that

\begin{prop}\label{p10}
Let $C$ and $D$ be two concepts, $0 < n_{1} \leq 0.5$, $1 \geq n_{2} >0.5$ and 
let $a$ be an individual.  It follows that for all $n> 0$ 
$\fuzzy{\cass{a}{C}}{n}{\geq} \entailf \fuzzy{\cass{a}{D}}{n}{\geq}$ 
iff for both $m \in \{n_{1},n_{2}\}$, $\fuzzy{\cass{a}{C}}{m}{\geq} 
\entailf \fuzzy{\cass{a}{D}}{m}{\geq}$ holds.  \ok
\end{prop}

\nd As a consequence, the subsumption problem can be reduced to the 
entailment problem for which we have a decision algorithm.

%------------------------------ COMPUTING glbdeg -------
\subsection{A Decision Procedure for the BTVB Problem}  \label{maxdeg}
%--------------------------------------------------------

\nd We address now the problem of determining $glb(\Sigma, \ass)$ and 
$lub(\Sigma, \ass)$.  This is important, as computing, \eg~$glb(\FKB, 
\ass)$, is in fact the way to answer a query of type ``to which degree 
is $\ass$ (at least) true, given the (imprecise) facts in $\FKB$?".

Without loss of generality, we will assume that all concepts are in 
NNF ({\em Negation Normal Form}).  Straccia (2000b) %\cite{Straccia00a} 
has shown that, in case of fuzzy propositional logic, from a set $\FKB$ of 
fuzzy propositions of the form $\fuzzy{p}{n}{\geq}$ and 
$\fuzzy{p}{n}{\leq}$, where $p$ is a proposition, it is possible to 
determine a finite set $N^{\FKB} \subset [0,1]$, where $|N^{\FKB}|$ is 
$O(|\FKB|)$, such that $glb(\FKB,q) \in N^{\FKB}$, \ie\ the greatest 
lower bound of a proposition $q$ \wrt\ $\FKB$ has to be an element of 
$N^{\FKB}$.  Therefore, $glb(\FKB,q)$ can be determined by computing 
the greatest value $n \in N^{\FKB}$ such that $\FKB \entailf 
\fuzzy{q}{n}{\geq}$.  An easy way to search for this $n$ is to order 
the elements of $N^{\FKB}$ and then to perform a binary search among 
these values by successive entailment tests.  Dually, as $lub(\FKB,q) 
= 1 - glb(\FKB,\notf q)$ holds, the $lub$ can either be computed from 
the $glb$ or, as $lub(\FKB,q) \in 1-N^{\FKB}$, where $1-N^{\FKB} = 
\{1-n: n \in N^{\FKB} \}$, we can compute it by determining the 
smallest value in $1-N^{\FKB}$.

\vspace*{0.5cm}

\begin{prop}[Straccia, 2000b] \label{p9} %[\cite{Straccia00a}]
Let $\FKB$ be a set of fuzzy propositions in NNF and let $q$ be a proposition. 
Then $glb(\FKB,q) \in N^{\FKB}$ and $lub(\FKB,q) \in 1-N^{\FKB}$, 
where 

\[
\begin{array}{lcl}
     N^{\FKB} & = & \{0,0.5,1\} \ \cup \\ 
                &   & \{n:  \fuzzy{p}{n}{\geq}\in\FKB \} \ \cup \\
                &   & \{1-n: \fuzzy{p}{n}{\leq} \in \FKB  \}  \\ \\
	 1-N^{\FKB} & =  & \{ 1-n: n \in N^{\FKB} \}	. 						 

\end{array}	 
\] \ok

\end{prop}


\nd The above Proposition~\ref{p9} can easily  be extended our fuzzy 
description logic case.  Essentially, the quantifiers do not change the 
possible values of $glb(\Sigma,F)$ and $lub(\Sigma,F)$.

\begin{prop}\label{p11}
Let $\FKB$ be a set of fuzzy assertions in NNF and let $\ass$ be an 
assertion. Then $glb(\FKB,\ass) \in N^{\FKB}$ and $lub(\FKB,\ass) \in 1-N^{\FKB}$, 
where 

\[
\begin{array}{lcl}
     N^{\FKB} & = & \{0,0.5,1\} \ \cup \\ 
                &   & \{n:  \fuzzy{\ass}{n}{\geq} \in \FKB \} \ \cup \\
                &   & \{1-n: \fuzzy{\ass}{n}{\leq} \in \FKB  \}  \\ \\
	 1-N^{\FKB} & =  & \{ 1-n: n \in N^{\FKB} \}	. 						 

\end{array}	 
\] \ok
\end{prop}

\begin{pf} Let us show that $glb(\FKB,\ass) \in N^{\FKB}$.  Let $m$ be 
$glb(\FKB,\ass)$.  By definition, if $m=0$ then $S = \FKB \cup \{ 
\fuzzy{\ass}{n}{<}\}$ is satisfiable for any $n>0$ and $0 \in 
N^{\FKB}$.  Otherwise, $m >0$ is the largest value such that $S = \FKB 
\cup \{ \fuzzy{\ass}{m}{<}\}$ is not satisfiable.  Let us mark each 
sub-expression in $\ass$ with a $^{*}$, so that we can trace the 
components of the query assertion $\ass$ during a deduction.  Consider 
a completion $S'$ of $S$.  Starting from $\fuzzy{\ass}{m}{<}$, by 
applying the rules of inference, only $^{*}$ marked expressions of 
type $\fuzzy{\ass'}{m}{<}$ or $\fuzzy{\ass'}{1-m}{>}$ can appear in 
$S'$.  Furthermore, as $S$ is not satisfiable, $S'$ contains a clash, 
\ie\ the value $m$ is the largest value such that all completions $S'$ 
of $S$ contain a clash.  Let us analyse $S'$.  As $S'$ contains a 
clash, then either \ii{i} there is a clash according to 
Table~\ref{clashcons}, or \ii{ii} there is a clash according to 
Table~\ref{tabconj}.  If \ii{i} is the case, \ie\ there is $\psi \in 
S'$ which is a clash, then we have to distinguish between two cases: 
(a) $\psi$ is not marked with $^{*}$ and (b) $\psi$ is marked with 
$^{*}$.  In the former case, $S'$ contains a clash independently of 
the value $m$ and, thus, the largest possible value $m$ for which $S'$ 
contains a clash is $1$.  In the latter case, as $m > 0$, either $\psi 
=\fuzzy{\cass{w}{\bottomc}}{1-m}{>}$ or $\psi = 
\fuzzy{\cass{w}{\topc}}{m}{<}$ which are both clashes for any value of 
$m$.  As a consequence, the largest possible value $m$ for which $S'$ 
contains a clash according to Table~\ref{clashcons} is $1$.  Assume 
$\ii{ii}$ is the case, \ie\ a conjugated pair of fuzzy constraints 
$\psi$ and $\psi'$ is in $S'$.  Similarly to the previous case, we 
have to distinguish the cases for which $\psi$ and $\psi'$ are marked 
with $^{*}$.  There are four cases:

(a) $\psi = \fuzzy{\ass}{k}{\geq}$ and $\psi'=\fuzzy{\ass'}{k'}{\leq}$ 
are in $S'$, none is marked with $^{*}$ and $k > k'$.  Therefore, $S'$ 
contains a clash for any value of $m$ and, thus, the largest choice is 
$1$;

(b) $\psi = \fuzzy{\ass}{k}{\geq}$ and $\psi'=\fuzzy{\ass'}{m}{<}$ are 
in $S'$, only $\psi'$ is marked with $^{*}$ and $k \geq m$.  
Therefore, $S'$ contains a clash for any value of $m \leq k$ and, 
thus, the largest choice for $m$ is $k$.  It is easily verified by 
case analysis on the rules that from $\psi \in S'$, $k \in N^{\FKB}$ 
follows; 

(c) $\psi = \fuzzy{\ass}{k}{\leq}$ and $\psi'=\fuzzy{\ass'}{1-m}{>}$ 
are in $S'$, only $\psi'$ is marked with $^{*}$ and $k \leq 1-m$.  
Therefore, $S'$ contains a clash for any value of $m \leq 1-k$ and, 
thus, the largest choice for $m$ is $1-k$.  It is easily verified by 
case analysis on the rules that from $\psi \in S'$, $1-k \in N^{\FKB}$ 
follows;

(d) $\psi = \fuzzy{\ass}{m}{<}$ and $\psi'=\fuzzy{\ass'}{1-m}{>}$ 
are in $S'$, both are marked with $^{*}$ and $m \leq 1-m$.  
Therefore, $S'$ contains a clash for any value of $m \leq 0.5$ and, 
thus, the largest choice for $m$ is $0.5$.

Summing up, we have proved that the largest possible value for $m$ is 
such that $m \in N^{\FKB}$. \qed
\end{pf}

\nd The algorithms computing $glb(\FKB,\ass)$ and $lub(\FKB,\ass)$ are 
described in Table~\ref{tabalgomax}.  For instance, by a binary search 
on $N^{\FKB}$, the value of $glb(\FKB,\ass)$ can be determined in at 
most $\log |N^{\FKB}|$ fuzzy entailment tests.

%{\small
\begin{table}
\begin{center}
\begin{tabular}{|c|} \hline \\
\setlength{\unitlength}{.5cm}
\begin{minipage}{.9\columnwidth}
\renewcommand{\thealgo}{$Max(\FKB,\ass)$}
\begin{algo} \mbox{ \ } \\
{\em 
Set $Min := 0$ and $Max := 2$.
\begin{enumerate}
\item
Pick $n \in N^{\FKB} \setminus \{0\}$ such that $Min < n < Max$. If there is no such $n$, then
set $glb(\FKB,\ass):= Min$ and exit.
\item
If $\FKB \entailf \fuzzy{\ass}{n}{\geq}$ then set $Min = n$, else set 
$Max = n$. Go to Step 1.
%\okex
\end{enumerate}
}
\end{algo}

\renewcommand{\thealgo}{$Min(\FKB,\ass)$}
\begin{algo} \mbox{ \ } \\
{\em 
Set $Min := 0$ and $Max := 2$.
\begin{enumerate}
\item
Pick $n \in (1- N^{\FKB}) \setminus \{0\}$ such that $Min < n < Max$. If there is no such $n$, then
set $lub(\FKB,\ass):= \min\{Max,1\}$ and exit.
\item
If $\FKB \entailf \fuzzy{\ass}{n}{\leq}$ then set $Max = n$, else set 
$Min = n$. Go to Step 1.
%\okex
\end{enumerate}
}
\end{algo}

\end{minipage} \\
\\ \hline
\end{tabular}
\end{center}
\caption{Algorithms $Max(\FKB,\ass)$ and $Min(\FKB,\ass)$} \label{tabalgomax}
\end{table}
%}


%--------------------------

\section{Conclusions and Future Work} \label{concl}

\nd In this work, we have presented a quite general fuzzy extension of 
the DL \alc, a significant and expressive representative of the 
various DLs.  Our fuzzy DL enables us to reason in presence of 
imprecise \alc \ concepts, \ie~fuzzy \alc \ concepts.  From a 
semantics point of view, fuzzy concepts are interpreted as fuzzy sets 
\ie~given a concept $C$ and an individual $a$, $C(a)$ is interpreted 
as the truth-value of the sentence ``$a$ is $C$''.  From a syntax 
point of view, we allow to specify lower and upper bounds of the 
truth-value of $C(a)$.  Complete algorithms for reasoning in it have 
been presented, that is, we have devised algorithms for solving 
the entailment problem, the subsumption problem as well as the best 
truth-value bound problem.

An important point concerns computational complexity.  
The complexity result shows that the additional expressive power has 
no impact from a computational complexity point of view.

The extension of DLs to the management of vagueness is not new 
\cite{Tresp98,Yen91a}.  Yen was the first, to the best of my 
knowledge, introducing vagueness into a simple DL. His language has 
two interesting points not included into our language.  Firstly, it 
allows the definition of vague concepts by means of explicit 
membership functions over a domain, \eg\ ${\sf LowPressure} \defcf 
domain({\sf AirPressure}); membershipfx(\lambda p.  {\sf low}(p))$.  
Here the domain over $p$ ranges is given by {\sf AirPressure}.  
$\lambda p.  {\sf low}(p)$ determines the membership degree of being a 
pressure $p$ low.  Secondly, the language allows \emph{concept 
modifiers}, like {\sf Very} or {\sf Slightly}, by means of which 
concepts like ``very low pressure'' can be defined through ${\sf 
VeryLowPressure} \defcf {\sf Very}({\sf LowPressure})$.  This last 
idea has been generalised to \alc\ by Tresp and Molitor (1998) %\cite{Tresp98} 
where a certain type of concept modifiers are allowed.  Strictly speaking, the 
language defined by Tresp and Molitor % \cite{Tresp98} 
is more expressive, as we do not consider 
concept modifiers.  From a semantics point of view, the extension to 
Tresp and Molitor's language %\cite{Tresp98} 
is quite straightforward.  But, the cost that we have to pay for this 
increasing expressive power is that, from a computational complexity 
and algorithms point of view, things changes radically.  Indeed, 
according to Tresp and Molitor %\cite{Tresp98} 
for each ``completion'' a linear optimisation problem 
is generated (set of inequations of the form $op_{1}(t_{1}) R 
op_{2}(t_{2})$ or $op_{1}(t_{1}) Rf(op_{2}(t_{2}))$, where $t_{i}$ is 
a truth-value variable, $R \in \{ \leq, \geq, =$, $op_{i} \in \{id, 
m_{i}\}$, with $id(t)$ the identity and $m_{i}(t)$ is a modifier 
function over truth-value variables, respectively, and $f \in 
\{min,max\}$-derived from the semantics of the connectors $\andc, 
\orc$) and then solved for the best value.  Then, the minimum among 
all computed solutions is taken.  The solutions can be computed by 
relying on methods from the domain of linear programming, \eg\ the 
\emph{simplex method} \cite{Papadimitriou82}.  While it is 
possible to devise a similar approach for our fuzzy DL as well, we 
have seen that this is not necessary.

Both aspects considered by Tresp and Molitor and by Yen, %\cite{Tresp98,Yen91a}, 
although interesting, are not crucial \wrt\ how we model logic-based 
multimedia information retrieval, where underlaying text, image and 
video analysis tools provide us fuzzy assertions \eg\ of the form 
$\fuzzy{\cass{a}{\csome {\sf About}.C}}{n}{\geq}$ from which we may 
infer $\fuzzy{\cass{a}{\csome {\sf About}.D}}{m}{\geq}$.


This work can be used as a basis both for extending existing DL based 
systems and for further research.  In this latter case, there are 
several open points.  For instance, it is not clear yet how to reason 
both in case of fuzzy specialisation of the general form $C \impcf D$ 
and in the case cycles are allowed in a fuzzy KB. Another interesting 
topic for further research concerns the semantics of fuzzy 
connectives.  Of course several other choices for the semantics of the 
connectives $\andc, \orc, \notc, \csome, \all$ can be considered.  
While for a huge number of proposals given in the literature their 
impact from a semantics point of view is well understood, the question 
how they impact from a computational complexity and algorithms point 
of view remains still open.

% In particular, the case of considering general terminological axioms (including cycles) and
% role-forming rules should be worked out. Another interesting point is to understand the impact of
% fuzziness on the computational complexity: is it always true that the upper bound of the complexity
% is the same as in the crisp case?


%----------------------------------------------------

\section*{Acknowledgements}

\nd
I would like to thank the three anonymous reviewers for their helpful 
comments on an early version of this paper. This is an extension and 
         revision of the paper appeared in AAAI-98.


%------------------------------ References -------

\nocite{ChenJ96}

%\input{fuzzyALCshortbbl}

% \bibliographystyle{theapa}
% \bibliography{mybiblio}


\begin{thebibliography}{}

\bibitem[\protect\BCAY{Baader \BBA\ Hollunder}{Baader \BBA\
  Hollunder}{1991a}]{Baader91d}
Baader, F.\BBACOMMA\  \BBA\ Hollunder, B. \BBOP1991a\BBCP.
\newblock \BBOQ {KRIS}: Knowledge representation and inference system, system
  description\BBCQ\
\newblock {\Bem {ACM} {SIGART} Bulletin}, {\Bem 2}, 8--14.

\bibitem[\protect\BCAY{Baader \BBA\ Hollunder}{Baader \BBA\
  Hollunder}{1991b}]{Baader91c}
Baader, F.\BBACOMMA\  \BBA\ Hollunder, B. \BBOP1991b\BBCP.
\newblock \BBOQ A terminological knowledge representation system with complete
  inference algorithm\BBCQ\
\newblock In {\Bem Proc.\ of the Workshop on Processing Declarative Knowledge,
  PDK-91}, \lowercase{\BNUM}\ 567 in Lecture Notes in Artificial Intelligence,
  \BPGS\ 67--86. Springer-Verlag.

\bibitem[\protect\BCAY{Bacchus}{Bacchus}{1990}]{Bacchus90}
Bacchus, F. \BBOP1990\BBCP.
\newblock {\Bem Representing and Reasoning with Probabilistic Knowledge}.
\newblock The {MIT} Press.

\bibitem[\protect\BCAY{Bellman \BBA\ Giertz}{Bellman \BBA\
  Giertz}{1973}]{Bellman73}
Bellman, R.\BBACOMMA\  \BBA\ Giertz, M. \BBOP1973\BBCP.
\newblock \BBOQ On the analytic formalism of the theory of fuzzy sets\BBCQ\
\newblock {\Bem Information Sciences}, {\Bem 5}, 149--156.

\bibitem[\protect\BCAY{Brachman}{Brachman}{1992}]{Brachman92}
Brachman, R.~J. \BBOP1992\BBCP.
\newblock \BBOQ ``reducing'' {CLASSIC} to practice: Knowledge representation
  meets reality\BBCQ\
\newblock In {\Bem Proc.\ of the 3rd Int.\ Conf.\ on the Principles of
  Knowledge Representation and Reasoning (KR-92)}, \BPGS\ 247--258. Morgan
  Kaufmann, Los Altos.

\bibitem[\protect\BCAY{Buchheit, Donini, \BBA\ Schaerf}{Buchheit
  et~al.}{1993a}]{Buchheit93}
Buchheit, M., Donini, F.~M., \BBA\ Schaerf, A. \BBOP1993a\BBCP.
\newblock \BBOQ Decidable reasoning in terminological knowledge representation
  systems\BBCQ\
\newblock In {\Bem Proc.\ of the 13th Int.\ Joint Conf.\ on Artificial
  Intelligence (IJCAI-93)}, \BPGS\ 704--709\ Chambery, France. Morgan Kaufmann,
  Los Altos.

\bibitem[\protect\BCAY{Buchheit, Donini, \BBA\ Schaerf}{Buchheit
  et~al.}{1993b}]{Buchheit93b}
Buchheit, M., Donini, F.~M., \BBA\ Schaerf, A. \BBOP1993b\BBCP.
\newblock \BBOQ Decidable reasoning in terminological knowledge representation
  systems\BBCQ\
\newblock {\Bem Journal of Artificial Intelligence Research}, {\Bem 1},
  109--138.

\bibitem[\protect\BCAY{Chen \BBA\ Kundu}{Chen \BBA\ Kundu}{1996}]{ChenJ96}
Chen, J.\BBACOMMA\  \BBA\ Kundu, S. \BBOP1996\BBCP.
\newblock \BBOQ A sound and complete fuzzy logic system using {Z}adeh's
  implication operator\BBCQ\
\newblock In Ras, Z.~W.\BBACOMMA\  \BBA\ Maciek, M.\BEDS, {\Bem Proc.\ of the
  9th Int.\ Sym.\ on Methodologies for Intelligent Systems (ISMIS-96)},
  \lowercase{\BNUM}\ 1079 in Lecture Notes in Artificial Intelligence, \BPGS\
  233--242. Springer-Verlag.

\bibitem[\protect\BCAY{da~Silva, Pereira, \BBA\ Netto}{da~Silva
  et~al.}{1994}]{daSilva94}
da~Silva, R.~M., Pereira, A. E.~C., \BBA\ Netto, M.~A. \BBOP1994\BBCP.
\newblock \BBOQ A system of knowledge representation based on formulae of
  predicate calculus whose variables are annotated by expressions of a fuzzy
  terminological logic\BBCQ\
\newblock In {\Bem Proc.\ of the 5th Int.\ Conf.\ on Information Processing and
  Managment of Uncertainty in Knowledge-Based Systems, (IPMU-94)},
  \lowercase{\BNUM}\ 945 in Lecture Notes in Computer Science. Springer-Verlag.

\bibitem[\protect\BCAY{Donini, Lenzerini, Nardi, \BBA\ Schaerf}{Donini
  et~al.}{1994}]{Donini94c}
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{Dubois \BBA\ Prade}{Dubois \BBA\ Prade}{1980}]{Dubois80}
Dubois, D.\BBACOMMA\  \BBA\ Prade, H. \BBOP1980\BBCP.
\newblock {\Bem Fuzzy Sets and Systems}.
\newblock Academic Press, New York, NJ.

\bibitem[\protect\BCAY{Dubois \BBA\ Prade}{Dubois \BBA\
  Prade}{1994}]{Dubois94a}
Dubois, D.\BBACOMMA\  \BBA\ Prade, H. \BBOP1994\BBCP.
\newblock \BBOQ Can we enforce full compositionality in uncertainty
  calculi?\BBCQ\
\newblock In {\Bem Proc.\ of the 11th Nat.\ Conf.\ on Artificial Intelligence
  (AAAI-94)}, \BPGS\ 149--154\ Seattle, Washington.

\bibitem[\protect\BCAY{Dubois \BBA\ Prade}{Dubois \BBA\ Prade}{1996}]{Dubois96}
Dubois, D.\BBACOMMA\  \BBA\ Prade, H. \BBOP1996\BBCP.
\newblock \BBOQ Approximate and commonsense reasoning: From theory to
  practice\BBCQ\
\newblock In Ras, Z.~W.\BBACOMMA\  \BBA\ Maciek, M.\BEDS, {\Bem Proc.\ of the
  9th Int.\ Sym.\ on Methodologies for Intelligent Systems (ISMIS-96)},
  \lowercase{\BNUM}\ 1079 in Lecture Notes in Artificial Intelligence, \BPGS\
  19--33. Springer-Verlag.

\bibitem[\protect\BCAY{Halpern}{Halpern}{1990}]{Halpern90}
Halpern, J.~Y. \BBOP1990\BBCP.
\newblock \BBOQ An analysis of first-order logics of probability\BBCQ\
\newblock {\Bem Artificial Intelligence Journal}, {\Bem 46}, 311--350.

\bibitem[\protect\BCAY{Heinsohn}{Heinsohn}{1994}]{Heinsohn94}
Heinsohn, J. \BBOP1994\BBCP.
\newblock \BBOQ Probabilistic description logics\BBCQ\
\newblock In de~Mantara, R.~L.\BBACOMMA\  \BBA\ Pool, D.\BEDS, {\Bem
  Proceedings of the 10th Conference on Uncertainty in Artificila
  Intelligence}, \BPGS\ 311--318.

\bibitem[\protect\BCAY{Hollunder}{Hollunder}{1994}]{Hollunder94}
Hollunder, B. \BBOP1994\BBCP.
\newblock \BBOQ An alternative proof method for possibilistic logic and its
  application to terminological logics\BBCQ\
\newblock In {\Bem 10th Annual Conference on Uncertainty in Artificial
  Intelligence}\ Seattle, Washington. R. Lopez de Mantaras and D. Pool.

\bibitem[\protect\BCAY{Horrocks}{Horrocks}{1998}]{Horrocks98}
Horrocks, I. \BBOP1998\BBCP.
\newblock \BBOQ Using an expressive description logic: Fact or fiction?\BBCQ\
\newblock In {\Bem Proc.\ of the 8th Int.\ Conf.\ on the Principles of
  Knowledge Representation and Reasoning (KR-98)}.

\bibitem[\protect\BCAY{J{\"{a}}ger}{J{\"{a}}ger}{1994}]{Jager94}
J{\"{a}}ger, M. \BBOP1994\BBCP.
\newblock \BBOQ Probabilistic reasoning in terminological logics\BBCQ\
\newblock In {\Bem Proceedings of KR-94, 5-th International Conference on
  Principles of Knowledge Representation and Reasoning}, \BPGS\ 305--316\ Bonn,
  FRG.

\bibitem[\protect\BCAY{Koller, Levy, \BBA\ Pfeffer}{Koller
  et~al.}{1997}]{Koller97}
Koller, D., Levy, A., \BBA\ Pfeffer, A. \BBOP1997\BBCP.
\newblock \BBOQ {P-CLASSIC}: A tractable probabilistic description logic\BBCQ\
\newblock In {\Bem Proc.\ of the 14th Nat.\ Conf.\ on Artificial Intelligence
  (AAAI-97)}, \BPGS\ 390--397.

\bibitem[\protect\BCAY{Kruse, Schwecke, \BBA\ Heinsohn}{Kruse
  et~al.}{1991}]{Kruse91}
Kruse, R., Schwecke, E., \BBA\ Heinsohn, J. \BBOP1991\BBCP.
\newblock {\Bem Uncertainty and Vagueness in Knowledge Based Systems}.
\newblock Springer-Verlag, Berlin, Germany.

\bibitem[\protect\BCAY{Lee}{Lee}{1972}]{Lee72}
Lee, R. C.~T. \BBOP1972\BBCP.
\newblock \BBOQ Fuzzy logic and the resolution principle\BBCQ\
\newblock {\Bem Journal of the ACM}, {\Bem 19\/}(1), 109--119.

\bibitem[\protect\BCAY{Meghini, Sebastiani, \BBA\ Straccia}{Meghini
  et~al.}{1997}]{Meghini97b}
Meghini, C., Sebastiani, F., \BBA\ Straccia, U. \BBOP1997\BBCP.
\newblock \BBOQ Modelling the retrieval of structured documents containing
  texts and images\BBCQ\
\newblock In {\Bem Proceedings of the First European Conference on Research and
  Advanced Technology for Digital Libraries}, \lowercase{\BNUM}\ 1324 in
  Lecture Notes in Computer Science, \BPGS\ 325--344\ Pisa, Italy.

\bibitem[\protect\BCAY{Meghini, Sebastiani, \BBA\ Straccia}{Meghini
  et~al.}{1998}]{Meghini98a}
Meghini, C., Sebastiani, F., \BBA\ Straccia, U. \BBOP1998\BBCP.
\newblock \BBOQ {\sc Mirlog}: A logic for multimedia information
  retrieval\BBCQ\
\newblock In Crestani, F., Lalmas, M., \BBA\ van Rijsbergen, C.\BEDS, {\Bem
  Logic and Uncertainty in Information Retrieval: Advanced models for the
  representation and retrieval of information}, \lowercase{\BVOL}~4 of {\Bem
  The Kluwer International Series On Information Retrieval}, \BCH~7, \BPGS\
  151--185. Kluwer Academic Publishers, Boston, USA.

\bibitem[\protect\BCAY{Meghini \BBA\ Straccia}{Meghini \BBA\
  Straccia}{1996}]{Meghini96}
Meghini, C.\BBACOMMA\  \BBA\ Straccia, U. \BBOP1996\BBCP.
\newblock \BBOQ A relevance terminological logic for information
  retrieval\BBCQ\
\newblock In {\Bem Proceedings of the 19th Annual International ACM SIGIR
  Conference on Research and Development in Information Retrieval (ACM
  SIGIR-96)}, \BPGS\ 197--205\ Zurich, Switzerland.

\bibitem[\protect\BCAY{Nebel}{Nebel}{1988}]{Nebel88}
Nebel, B. \BBOP1988\BBCP.
\newblock \BBOQ Computational complexity of terminological reasoning in
  {BACK}\BBCQ\
\newblock {\Bem Artificial Intelligence}, {\Bem 34}, 371--383.

\bibitem[\protect\BCAY{Nebel}{Nebel}{1990}]{Nebel90a}
Nebel, B. \BBOP1990\BBCP.
\newblock {\Bem Reasoning and revision in hybrid representation systems}.
\newblock Springer, Heidelberg, FRG.

\bibitem[\protect\BCAY{Papadimitriou \BBA\ Steiglitz}{Papadimitriou \BBA\
  Steiglitz}{1982}]{Papadimitriou82}
Papadimitriou, C.~H.\BBACOMMA\  \BBA\ Steiglitz, K. \BBOP1982\BBCP.
\newblock {\Bem Combinatorial Optimization: Algorithms and Complexity}.
\newblock Prentice-Hall, Englewood Cliffs, New Jersey.

\bibitem[\protect\BCAY{Pearl}{Pearl}{1988}]{Pearl88}
Pearl, J. \BBOP1988\BBCP.
\newblock {\Bem Probabilistic Reasoning in Intelligent Systems: Networks of
  Plausible Inference}.
\newblock Morgan Kaufmann, Los Altos.

\bibitem[\protect\BCAY{Peltason}{Peltason}{1991}]{Peltason91}
Peltason, C. \BBOP1991\BBCP.
\newblock \BBOQ The {BACK} system -- an overview\BBCQ\
\newblock {\Bem {SIGART} Bulletin}, {\Bem 2\/}(3), 114--119.

\bibitem[\protect\BCAY{Roth}{Roth}{1996}]{Roth96}
Roth, D. \BBOP1996\BBCP.
\newblock \BBOQ On the hardness of approximate reasoning\BBCQ\
\newblock {\Bem Artificial Intelligence Journal}, {\Bem 82}, 273--302.

\bibitem[\protect\BCAY{Schmidt-Schau{\ss} \BBA\ Smolka}{Schmidt-Schau{\ss}
  \BBA\ Smolka}{1991}]{Schmidt-Schauss91}
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--26.

\bibitem[\protect\BCAY{Sebastiani}{Sebastiani}{1994}]{Sebastiani94a}
Sebastiani, F. \BBOP1994\BBCP.
\newblock \BBOQ A probabilistic terminological logic for modelling information
  retrieval\BBCQ\
\newblock In {\Bem Proceedings of SIGIR-94, 17th ACM International Conference
  on Research and Development in Information Retrieval}, \BPGS\ 122--130\
  Dublin, IRL.
\newblock Published by Springer Verlag, Heidelberg, FRG.

\bibitem[\protect\BCAY{Straccia}{Straccia}{1998}]{Straccia98}
Straccia, U. \BBOP1998\BBCP.
\newblock \BBOQ A fuzzy description logic\BBCQ\
\newblock In {\Bem Proc.\ of the 15th Nat.\ Conf.\ on Artificial Intelligence
  (AAAI-98)}, \BPGS\ 594--599\ Madison, USA.

\bibitem[\protect\BCAY{Straccia}{Straccia}{2000a}]{Straccia00b}
Straccia, U. \BBOP2000a\BBCP.
\newblock \BBOQ A note on the relationship between fuzzy logic and four-valued
  logic\BBCQ\
\newblock Technical report\ B4-22-10-2000, Istituto di Elaborazione
  dell'Informazione, Consiglio Nazionale delle Ricerche, Pisa, Italy.

\bibitem[\protect\BCAY{Straccia}{Straccia}{2000b}]{Straccia00a}
Straccia, U. \BBOP2000b\BBCP.
\newblock \BBOQ Reasoning and experimenting within {Z}adeh's fuzzy
  propositional logic\BBCQ\
\newblock Technical report\ 2000-b4-011, Istituto di Elaborazione
  dell'Informazione, Consiglio Nazionale delle Ricerche, Pisa, Italy.

\bibitem[\protect\BCAY{Tresp \BBA\ Molitor}{Tresp \BBA\
  Molitor}{1998}]{Tresp98}
Tresp, C.\BBACOMMA\  \BBA\ Molitor, R. \BBOP1998\BBCP.
\newblock \BBOQ A description logic for vague knowledge\BBCQ\
\newblock In {\Bem Proc.\ of the 13th European Conf.\ on Artificial
  Intelligence (ECAI-98)}\ Brighton (England).

\bibitem[\protect\BCAY{Xiachun, Yunfei, \BBA\ Xuhua}{Xiachun
  et~al.}{1995}]{Xiaochun95}
Xiachun, C., Yunfei, J., \BBA\ Xuhua, L. \BBOP1995\BBCP.
\newblock \BBOQ The rationality and decidability of fuzzy implications\BBCQ\
\newblock In {\Bem Proc.\ of the 14th Int.\ Joint Conf.\ on Artificial
  Intelligence (IJCAI-95)}, \BPGS\ 1910--1911\ Montreal, Canada. MK.

\bibitem[\protect\BCAY{Yen}{Yen}{1991}]{Yen91a}
Yen, J. \BBOP1991\BBCP.
\newblock \BBOQ Generalizing term subsumption languages to fuzzy logic\BBCQ\
\newblock In {\Bem Proc.\ of the 12th Int.\ Joint Conf.\ on Artificial
  Intelligence (IJCAI-91)}, \BPGS\ 472--477\ Sydney, Australia.

\bibitem[\protect\BCAY{Zadeh}{Zadeh}{1965}]{Zadeh65}
Zadeh, L.~A. \BBOP1965\BBCP.
\newblock \BBOQ Fuzzy sets\BBCQ\
\newblock {\Bem Information and Control}, {\Bem 8\/}(3), 338--353.

\end{thebibliography}



\end{document}
