\documentclass[9pt]{scrartcl}
\usepackage{t1enc}
\usepackage[latin2]{inputenc}
\usepackage[a4paper,noheadfoot,left=15mm,right=15mm,top=15mm,bottom=15mm]{geometry}
\usepackage{enumitem}
\usepackage{url}
\usepackage{graphicx}
%\pagestyle{empty}

\def\XYcompile{\xycompile}
\setlength{\fboxsep}{2mm}
\newcommand{\framing}[1]{%
  \medskip
  \framebox{\parbox{12cm}{#1}}
  \medskip
}

\newcommand{\bs}{\symbol{92}} %best method of producing backslash in T1 mode
\newcommand{\tlde}{\symbol{126}} %best method of producing a tilde in T1 mode
\newcommand{\mydef}[1]{\emph{#1}}
\newcommand{\mainIndex}{}
\newcommand{\engdef}[1]{angolul:\ \emph{#1}}

\newcommand{\fullstop}{.}

\newcommand{\bT}{\mathbf{T}}
\newcommand{\cE}{$\mathcal{E}$\ }
\newcommand{\ciE}{\mathcal{E} }
\newcommand{\cR}{$\mathcal{R}$}
\newcommand{\ciR}{\mathcal{R} }
\newcommand{\ciT}{\mathcal{T} }
\newcommand{\cT}{$\mathcal{T}$}
\newcommand{\ciL}{\mathcal{L} }
\newcommand{\cL}{$\mathcal{L}$\ }
\newcommand{\ciI}{\mathcal{I}}
\newcommand{\cI}{$\mathcal{I}$}
\newcommand{\ciA}{\mathcal{A}}
\newcommand{\cA}{$\mathcal{A}$}
\newcommand{\nexptime}{\textsc{NExpTime}}
\newcommand{\exptime}{\textsc{ExpTime}}
\newcommand{\pspace}{\textsc{PSpace}}
\newcommand{\npspace}{\textsc{NPSpace}}
\newcommand{\sqtrcr}{\sqsubseteq^*}

\def\xbox{\vbox{\hrule width 6pt height 7pt}}
\newenvironment{proof}{\smallskip\textit{Proof. (Sketch) }}{\hfill \xbox \medskip\par}

% environment for exercises, feel free to improve
\def\xline{\vbox{\hrule width \textwidth height 1pt}}
% \newcounter{exercisec}[chapter]
% \newenvironment{myexercise}{\xline\nobreak \refstepcounter{exercisec} \noindent \textit{Exercise \thechapter.\theexercisec:}}{\par \nobreak\xline}

% environment for queries
\newenvironment{myquery}{\nobreak \refstepcounter{equation} \noindent}{\hfill\textit{(\theequation)} \par \nobreak }

% colouring
\def\colouring{0} % set this to 1 to enable colors
%\def\colouring{1} % set this to 0 to disable colors
\ifnum \colouring > 0
  \newcommand{\iv}[1]{\textcolor{mmagenta}{\texttt{#1}}}
  \newcommand{\dm}[1]{\textcolor{mlblue}{\texttt{#1}}}
  \newcommand{\class}[1]{\textcolor{mred}{\texttt{#1}}}
  \newcommand{\prop}[1]{\textcolor{mblue}{\texttt{#1}}}
  \newcommand{\lit}[1]{\textcolor{morange}{\texttt{#1}}}
  \newcommand{\op}[1]{\textcolor{mgreen}{\texttt{#1}}}
  \newcommand{\ivC}[1]{\textcolor{mmagenta}{#1}}
  \newcommand{\dmC}[1]{\textcolor{mlblue}{#1}}
  \newcommand{\classC}[1]{\textcolor{mred}{#1}}
  \newcommand{\propC}[1]{\textcolor{mblue}{#1}}
  \newcommand{\litC}[1]{\textcolor{morange}{#1}}
  \newcommand{\opC}[1]{\textcolor{mgreen}{#1}}
  \newcommand{\dliv}[1]{\textcolor{mmagenta}{\textsf{#1}}}
  \newcommand{\dldm}[1]{\textcolor{mgreen}{\texttt{#1}}}
  \newcommand{\dlclass}[1]{\textcolor{mred}{\textsf{#1}}}
  \newcommand{\dlprop}[1]{\textcolor{mblue}{\textsf{#1}}}
  \newcommand{\dllit}[1]{\textcolor{morange}{\textsf{#1}}}
  \newcommand{\dlop}[1]{\textcolor{mgreen}{\textsf{#1}}}
  \newcommand{\ifcolour}[1]{#1}
\else
  \newcommand{\iv}[1]{\texttt{#1}}
  \newcommand{\dm}[1]{\texttt{#1}}
  \newcommand{\class}[1]{\texttt{#1}}
  \newcommand{\prop}[1]{\texttt{#1}}
  \newcommand{\lit}[1]{\texttt{#1}}
  \newcommand{\op}[1]{\texttt{#1}}
  \newcommand{\ivC}[1]{#1}
  \newcommand{\dmC}[1]{#1}
  \newcommand{\classC}[1]{#1}
  \newcommand{\propC}[1]{#1}
  \newcommand{\litC}[1]{#1}
  \newcommand{\opC}[1]{#1}
  \newcommand{\dliv}[1]{\textsf{#1}}
  \newcommand{\dldm}[1]{\texttt{#1}}
  \newcommand{\dlclass}[1]{\textsf{#1}}
  \newcommand{\dlprop}[1]{\textsf{#1}}
  \newcommand{\dllit}[1]{\textsf{#1}}
  \newcommand{\dlop}[1]{\textsf{#1}}
  \newcommand{\ifcolour}[1]{}
\fi


% The mystic bigbox

\newdimen\boxfigwidth 

\def\magicbox{\begingroup
  \boxfigwidth=\hsize
  \advance\boxfigwidth by -2\fboxrule
  \advance\boxfigwidth by -2\fboxsep
  \setbox4=\vbox\bgroup\hsize\boxfigwidth
  \hrule height0pt width\boxfigwidth\smallskip
  \linewidth=\boxfigwidth
}
\def\endmagicbox{\smallskip\egroup\fbox{\box4}\endgroup}

\newcommand{\mypair}[1]{\langle\,#1\,\rangle}

\renewcommand{\textfraction}{0}
\renewcommand{\floatpagefraction}{1}
\renewcommand{\topfraction}{1}
\renewcommand{\bottomfraction}{1}

\newcommand*{\ilink}[1]{\textsf{#1}}
\newcommand*{\code}[1]{\texttt{#1}}
\newenvironment{myverbatim}{\tt\obeylines\obeyspaces\frenchspacing\medskip\setlength{\parindent}{0em}}{\medskip}

\newcommand{\dlclassTall}{\dlclass{Tall}}
\newcommand{\classTall}{\class{Tall}}
\newcommand{\engtall}{tall}
\newcommand{\dlclassT}{\dlclass{T}}
\newcommand{\txtTall}{Tall}

\newcommand{\dlclassBlonde}{\dlclass{Blonde}}
\newcommand{\classBlonde}{\class{Blonde}}
\newcommand{\engblonde}{blonde}
\newcommand{\dlclassB}{\dlclass{B}}
\newcommand{\txtBlonde}{Blonde}

\newcommand{\dlclassOptimist}{\dlclass{Optimist}}
\newcommand{\classOptimist}{\class{Optimist}}
\newcommand{\engoptimist}{optimist}
\newcommand{\engoptimism}{optimism}
\newcommand{\dlclassO}{\dlclass{O}}
\newcommand{\txtOptimist}{Optimist}

\newcommand{\alphenumi}{
%\renewcommand{\itemindent}{0.3em}
\renewcommand{\labelenumi}{(\alph{enumi})}}

\newcommand{\Aurl}[1]{\accessed{} URL: \url{#1}}
\newcommand{\XXXignoreURL}{}  % to mark exclusions from the automatic verification of URLs

% COMMANDS for indexing
% ---------------------
% Include in the index using tt font
\newcommand{\indextt}[1]{\index{#1@\texttt{#1}}}
% Make a from-to style index entry using tt font
% Second argument may be ( or ), for marking the start or end position
\newcommand{\indexttb}[2]{\index{#1@\texttt{#1}|#2}}
% Include in the index and the text using tt font
\newcommand{\indexttins}[1]{\texttt{#1}\index{#1@\texttt{#1}}}
% Incluee a tt font index entry with a parenthesised remark
\newcommand{\indexalcn}[2]{\index{#1@\texttt{#1}~--~$\mathcal{ALCN}$ tableau #2}}
\newcommand{\indexHaskellraw}[3]{\index{#1@#2~--~Haskell~#3}
\indexHaskellBase{#3!#1@#2}}
\newcommand{\indexHaskellBase}[1]{\index{Haskell~(functional~language)!#1}}
\newcommand{\indexHaskell}[2]{\indexHaskellraw{#1}{\texttt{#1}}{#2}}
\newcommand{\indexDublin}[1]{\index{#1@\texttt{#1}~--~Dublin~Core}}
\newcommand{\indexSpec}[1]{\index{#1!specification}\index{specification!#1}}
\newcommand{\indexRestr}[3]{\index{#1!restriction#2#3}\index{restriction!#1#3}}
\newcommand{\indexRestrX}[3]{\index{#1~restriction#2#3}\index{restriction!#1#3}}

% \newcommand{\indexX}{\index{}\index{}}
\newcommand{\indexIntersectionRule}{\index{concept!intersection}%\index{intersection}%
\index{intersection!rule} \index{$\sqcap$-rule}\index{tableau!rule!$\sqcap$-rule}}
\newcommand{\indexExistsRule}{%\indexRestrX{existential}{!full}{}
\index{existential~restriction!rule}\index{$\exists$-rule}\index{tableau!rule!$\exists$-rule}}
\newcommand{\indexValueRule}{%\indexRestrX{value}{}{}
\index{value~restriction!rule}\index{$\forall$-rule}\index{tableau!rule!$\forall$-rule}}
\newcommand{\indexTrValueRule}{\index{value~restriction!transitivity~rule}%
\index{transitivity~rule~for~value~restriction}%
\index{$\forall_+$-rule}\index{tableau!rule!$\forall_+$-rule}}
\newcommand{\indexUnionRule}{\index{concept!union}\index{union!rule}\index{$\sqcup$-rule}\index{tableau!rule!$\sqcup$-rule}}
\newcommand{\indexAtMostRule}{\index{number~restriction!unqualified!at-most~rule}\index{at-most~rule}\index{$\leqslant$-rule}\index{tableau!rule!$\leqslant$-rule}}
\newcommand{\indexAtLeastRule}{\index{number~restriction!unqualified!at-least~rule}\index{at-least~rule}\index{$\geqslant$-rule}\index{tableau!rule!$\geqslant$-rule}}
\newcommand{\indexAtMostRuleQ}{\index{number~restriction!qualified!at-most~rule}\index{at-most~rule}\index{$\leqslant$-rule}\index{tableau!rule!$\leqslant$-rule}}
\newcommand{\indexAtLeastRuleQ}{\index{number~restriction!qualified!at-least~rule}\index{at-least~rule}\index{$\geqslant$-rule}\index{tableau!rule!$\geqslant$-rule}}
\newcommand{\indexJoinRule}{\index{number~restriction!qualified!choice~rule}\index{$\Join$-rule}\index{tableau!rule!$\Join$-rule}}
\newcommand{\indexDomain}[2]{\index{domain!#1#2}\index{#1~domain#2}}
\newcommand{\indexOWL}[1]{\index{OWL (Web~Ontology~Language)#1}}
\newcommand{\indexRDF}[1]{\index{RDF (Resource~Description~Framework)#1}}
\newcommand{\indexURI}[1]{\index{Uniform~Resource~Identifier~(URI)#1}}
\newcommand{\indexTBox}[1]{\index{TBox (Terminological~Box)#1}}
\newcommand{\indexABox}[1]{\index{ABox (Assertion~Box)#1}}
\newcommand{\indexAxiom}[2]{\index{axiom!#1!#2}\index{#1!#2~axiom}\index{#2!#1}}
\newcommand{\indexAxiomX}[2]{\index{axiom!#1!#2}\index{#1!#2~axiom}}
\newcommand{\indexAxiomXX}[2]{\index{axiom!#1!#2}\index{#1!#2}\index{#2!#1}}

\newcommand{\indexCassertion}{\index{assertion!concept}\index{concept!assertion}}
\newcommand{\indexRassertion}{\index{assertion!role}\index{role!assertion}}
\newcommand{\indexDefAxiom}[1]{\index{#1!axiom}\index{axiom!definitional}\index{definition!#1}\index{#1!definition}}
\newcommand{\indexGCI}{\index{GCI (General Concept Inclusion) axiom}
%\index{General Concept Inclusion (GCI) axiom}
\index{axiom!concept!GCI~axiom}\indexAxiom{concept}{inclusion}}
\newcommand{\indexGRIA}{\index{g-RIA (general Role Inclusion Axiom)}
%\index{general Role Inclusion Axiom (g-RIA)}
\indexAxiom{role}{inclusion}}
\newcommand{\indexTableauGraph}{\index{graph!tableau}\index{tableau!graph}}
\newcommand{\indexTableauAsABox}[1]{\indexABox{!tableau~state~viewed~as~ABox#1}\index{map!tableau~to~ABox#1}}
\newcommand{\indexInstance}[1]{\index{instance~reasoning!ABox!#1}%
\indexABox{!reasoning!#1}%
\index{reasoning!ABox!#1}}
\newcommand{\indexReasonABox}[1]{\indexABox{!reasoning!#1}%
\index{reasoning!ABox!#1}%
\index{#1~(ABox~reasoning)}}
\newcommand{\indexReasonTBox}[1]{\indexTBox{!reasoning!#1}%
\index{reasoning!TBox!#1}%
\index{#1~(TBox~reasoning)}}
\newcommand{\indexReasonABoxX}[1]{\indexABox{!reasoning!#1}%
\index{reasoning!ABox!#1}%
\index{#1!ABox~reasoning}}
\newcommand{\indexReasonTBoxX}[1]{\indexTBox{!reasoning!#1}%
\index{reasoning!TBox!#1}%
\index{#1!TBox~reasoning}}
\newcommand{\indexReasonTBoxConc}[1]{\indexTBox{!reasoning!concept~#1}%
\index{reasoning!TBox!concept~#1}%
\index{concept!#1~(TBox~reasoning)}%
\index{#1~of~concepts~(TBox~reasoning)}}
\newcommand{\indexReasonTBoxConcX}[1]{\indexTBox{!reasoning!concept~#1}%
\index{reasoning!TBox!concept~#1}%
\index{concept!#1~(TBox~reasoning)}%
\index{#1!concept}}
\newcommand{\indexMinPrincipleTableau}{\index{minimality~principle!tableau~algorithm}%
\index{tableau!algorithm!minimality~principle}}
\newcommand{\indexOntLang}[1]{\index{ontology!language!#1}\index{#1~ontology~language}}
\newcommand{\indexXMLqualName}{\index{XML!qualified~name}\index{name!qualified}\index{qualified~name}}
\newcommand{\indexRDFgraphComp}[1]{\indexRDF{!graph!#1}\index{graph!RDF!#1}\index{#1!RDF~graph}}
\newcommand{\indexExpRule}{\index{expansion!rule}\index{tableau!rule!expansion~rule}}
\newcommand{\indexNondetRule}{\index{non-deterministic~rule}\index{tableau!rule!non-deterministic~rule}}
\newcommand{\indexModelConstr}{\index{model construction@model~construction~(tableau~algorithm)}}
\newcommand{\indexIntermediateResource}{%
\index{intermediate~resource}%
\index{blank~resource}%
\index{anonymous~resource}%
\indexRDF{!resource%!intermediate
}}
\newcommand{\indexCrawler}{\index{crawler}\index{spider}\index{web~robot}\index{web~spider}}

\newcommand{\dlclassClever}{\dlclass{Tall}}
\newcommand{\classClever}{\class{Tall}}
\newcommand{\engclever}{tall}
\newcommand{\dlclassC}{\dlclass{T}}
\newcommand{\txtClever}{Tall}

\newcommand{\dlclassNice}{\dlclass{Blonde}}
\newcommand{\classNice}{\class{Blonde}}
\newcommand{\engnice}{blonde}
\newcommand{\dlclassN}{\dlclass{B}}
\newcommand{\txtNice}{Blonde}

\newcommand{\stsolsp}{\solsp{1.5cm}}
\newcommand{\bigsolsp}{\solsp{2cm}}
\newcommand{\solsp}[1]{

\vspace*{#1}

}
\begin{document}

\setlength{\parindent}{0cm} 
\setlength{\abovedisplayskip}{2pt}
\setlength{\abovedisplayshortskip}{0pt}
\setlength{\belowdisplayskip}{2pt}
\setlength{\belowdisplayshortskip}{0pt}

\begin{center}
\textbf{
Semantic Web -- Practice/Homework S1
}
\end{center}

\begin{enumerate}[itemsep=2pt,parsep=0pt,leftmargin=*]

\item Consider the interpretation $\ciI_x =
\mypair{\Delta,{I}}$, where

\bigskip

\begin{minipage}[t]{0.5\textwidth}
\begin{eqnarray}
\Delta &=& \{\dldm{Nick}, \dldm{Mary}, \dldm{Ann},
  \dldm{Steve}, \dldm{John}\}\nonumber\\
%  \dlclass{Human}^{I} &=& \Delta \nonumber\\
 \dlclass{Female}^{I} &=& \{\dldm{Mary}, \dldm{Ann}\}\nonumber\\
 \dlprop{hasChild}^{I} &=& \{\mypair{\dldm{Nick}, \dldm{Ann}},\mypair{\dldm{Mary},
  \dldm{Ann}},\nonumber\\
                    & & \hspace*{0.5em}\mypair{\dldm{Ann}, \dldm{John}},\mypair{\dldm{Steve},
  \dldm{John}}\}    \fullstop\nonumber
\end{eqnarray}
\end{minipage}

\vspace*{1cm}


First, write down the set of people that belong to the left and
right hand side of the following $\mathcal{AL}$ axioms, in the example
interpretation $\ciI_x$.

Next, decide if the
interpretation $\ciI_x$ is a model of the axiom, i.e.\ if the axiom
holds in interpretation $\ciI_x$.
\begin{enumerate}
\alphenumi
\item $\forall \dlprop{hasChild}.\bot \sqsubseteq \neg \dlclass{Female}$.\label{dlex7:first}

\bigsolsp

\item $\forall \dlprop{hasChild}.\dlclass{Female} \sqsubseteq \exists
  \dlprop{hasChild}.\top$.

\bigsolsp

\item $\forall \dlprop{hasChild}.\bot \sqsubseteq \forall
  \dlprop{hasChild}.\dlclass{Female}$.

\bigsolsp

\item $\dlclass{Female} \sqcap \forall
  \dlprop{hasChild}.\dlclass{Female}\sqsubseteq \exists
  \dlprop{hasChild}.\top$.

\bigsolsp

\item $\forall \dlprop{hasChild}.\dlclass{Female} \sqcap \forall
  \dlprop{hasChild}.\neg \dlclass{Female}\equiv \forall \dlprop{hasChild}.\bot$. \label{dlex7:last}

\bigsolsp

\end{enumerate}
Select those of the above axioms which are tautologies, i.e.\ statements
that hold in \textbf{all}  their interpretations.  You may check your results using Prot\'eg\'e.
\label{dlex7}

\solsp{4cm}

%% \item  (Optional) Is there an interpretation which is a model of axiom (b) listed in the
%% above Exercise~\ref{dlex7}? If so, give an example.
%% Using this, try to provide a simpler equivalent formulation of axiom (b).


%% \bigsolsp

\clearpage
\item Decide if the following concepts and statements (the last three, below
  the line)  can be formalised in the
language $\mathcal{AL}$ and its extensions $\mathcal{C}$, $\mathcal{U}$,
$\mathcal{E}$ and $\mathcal{N}$. If so, formulate the appropriate concept
expression or axiom. If not, just write: ``cannot be formulated''.

You can assume that the universe contains people only, so you do not need to
mention the the concept  \dlclass{Person} in the formulas.

Try to use the simplest language possible, e.g.\ use $\mathcal{AL}$ with
the smallest number of extensions. For each formula list the single-letter
abbreviations of the $\mathcal{AL}$ extensions it uses.

\begin{enumerate}
\alphenumi
% \renewcommand{\labelenumi}{\parbox{3em}{(\arabic{enumi})}} !!!!!
\item People  with at least one tall child.
  
  Solution: $\exists \dlprop{hasChild}.\dlclass{Tall}$ -- $\mathcal{E}$ 

\item People who do not have at least one tall child.

  Solution: $\neg \exists \dlprop{hasChild}.\dlclass{Tall}$ --
  $\mathcal{EC}$

  Reformulation: $\forall \dlprop{hasChild}.\neg \dlclass{Tall}$ -- just
  plain $\mathcal{AL}$ (without any extensions)

\item People  with at most one tall child (may have several
children, but at most one of these is tall).

  Solution: cannot be formulated in $\mathcal{ALCUEN}$

\item People with at least one child who is either blonde{} or tall{}.
\stsolsp\item People each of whose children is either blonde{} or tall{}.
\stsolsp\item People none of whose children are either blonde{} or tall{}.
\stsolsp\item People  with at most one  child.
\stsolsp\item People  with exactly one  child.
\stsolsp\item People  with exactly one child who happens to be blonde.
\stsolsp\item People  with exactly one blonde child (may have several
children, but exactly one of these is blonde).
\stsolsp

\noindent\makebox[\linewidth]{\hspace*{-1.5em}\rule{0.7\paperwidth}{0.4pt}\hfill}
\smallskip



\item A mother having at least three children is an optimist.
\stsolsp\item A woman is an optimist if all her children are optimists.\\
(Note that this is the same as: if all children of a woman are optimists
then she herself is an optimist.)
\stsolsp\item Anyone can have at most one spouse.
\stsolsp

\end{enumerate}


\clearpage
\item
Using the semantics of
$\mathcal{ALC}$  decide which
of the following axioms are tautologies, i.e.\ statements that hold in \textbf{all}  their interpretations.

\medskip

% \parbox{15em}{(a) $\left\{C\equiv\top\right\} \models \forall R.C\equiv\top$.}& &
% \parbox{15em}{(b) $\left\{\forall R.C\equiv\top\right\} \models C\equiv\top$.}\\
% \parbox{15em}{(c) $\left\{C\equiv\bot\right\} \models \exists R.C\equiv\bot$.}& &
% \parbox{15em}{(d) $\left\{\exists R.C\equiv\bot\right\} \models C\equiv\bot$.}\\
\parbox{15em}{(a) $ \forall R.C_1 \sqcap \forall R.C_2 \sqsubseteq \forall R.(C_1\sqcap C_2)$.}

\solsp{1cm}\parbox{15em}{(b) $ \forall R.C_1 \sqcap \forall R.C_2 \sqsupseteq \forall R.(C_1\sqcap C_2)$.}

\solsp{1cm}\parbox{15em}{(c) $ \exists R.C_1 \sqcap \exists R.C_2 \sqsubseteq \exists R.(C_1\sqcap C_2)$.}

\solsp{1cm}\parbox{15em}{(d) $ \exists R.C_1 \sqcap \exists R.C_2 \sqsupseteq \exists R.(C_1\sqcap C_2)$.}

\solsp{1cm}\parbox{15em}{(e) $ \forall R.C_1 \sqcup \forall R.C_2 \sqsubseteq \forall R.(C_1\sqcup C_2)$.}

\solsp{1cm}\parbox{15em}{(f) $ \forall R.C_1 \sqcup \forall R.C_2 \sqsupseteq \forall R.(C_1\sqcup C_2)$.}

\solsp{1cm}\parbox{15em}{(g) $ \exists R.C_1 \sqcup \exists R.C_2 \sqsubseteq \exists R.(C_1\sqcup C_2)$.}

\solsp{1cm}\parbox{15em}{(h) $ \exists R.C_1 \sqcup \exists R.C_2 \sqsupseteq \exists R.(C_1\sqcup C_2)$.}

\solsp{1cm}\label{dlex12}

You may check your results using Prot\'eg\'e.


\vspace*{1cm}

\item
Consider the following roles: \dlprop{hasParent}, \dlprop{hasMother}, \dlprop{hasChild}, 
\dlprop{hasFather}, \dlprop{hasGrandparent}, \dlprop{hasAncestor},
\dlprop{hasBloodRelation} (People $x$ and $y$ are blood relations if they
have a common ancestor).

Build the role hierarchy of this set of roles, i.e.\
list all the role inclusion  axioms involving these roles. Also declare the
appropriate roles transitive.
\label{dlex17}


\solsp{6cm}



\item
Consider the  roles listed in Exercise~\ref{dlex17}, together
with the role axioms provided by you as the solution to the exercise.
Decide which of the roles are simple.

\solsp{2cm}

\clearpage
\item
Formalise the following concepts and statements using the
$\mathcal{SI}$ language. Use the \dlprop{hasParent}, \dlprop{hasSibling}, and \dlprop{hasPart}
atomic roles and the \dlclass{Person}, \dlclass{Tall}, \dlclass{Car}, \dlclass{Critical}, \dlclass{Faulty}, 
atomic concepts only.
\begin{enumerate}
\alphenumi
\item People with at least one \engclever{} child.
\stsolsp\item People who only have \engclever{} children.
\stsolsp\item Children with at least one \engclever{} parent.
\stsolsp\item Parts of a car.
\stsolsp

\noindent\makebox[\linewidth]{\hspace*{-1.5em}\rule{0.7\paperwidth}{0.4pt}\hfill}
\smallskip

\item A car which has a critical part that is faulty is itself faulty.
\stsolsp\item Children of a person with at least one tall child are either tall themselves or have a tall sibling.
\stsolsp\end{enumerate}


\item
Formalise the following concepts and statements using the
$\mathcal{SHIQ}$ language. Use the atomic roles \dlprop{hasParent} and
\dlprop{hasComponent}. The concept names to be used are given at each task.
\begin{enumerate}
\alphenumi
\item People with at least two \engclever{} children. (\dlclass{Person}, \dlclass{Tall})
\stsolsp
\item Cars with at most two faulty components. (\dlclass{Car}, \dlclass{Faulty})
\stsolsp

\noindent\makebox[\linewidth]{\hspace*{-1.5em}\rule{0.7\paperwidth}{0.4pt}\hfill}
\smallskip

\item A reliable system is not faulty if it has at most one faulty
  component. (\dlclass{ReliableSystem}, \dlclass{Faulty})


  (Reliable systems use certain techniques, such as
  duplication of components, to achieve correct behaviour even if some of
  their components are faulty.)
\end{enumerate}




\end{enumerate}

\end{document}







