\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{alltt}
\usepackage{graphicx}
\pagestyle{empty}
\newcommand{\ntt}[1]{{\ttfamily #1}}

\begin{document}

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

\begin{center}
\textbf{\Large
              AIT Semantic and Declarative Technologies Course\\[1ex]
          Homework L3:  Defining family relationships using FOL clauses \\[1ex]
}
\end{center}


Assume the definition of the following predicates has
been provided:
\begin{itemize}
\item \ntt{hParent(Ch, P)}: \ntt{Ch} has a parent \ntt{P}.

\item \ntt{female(P)}: \ntt{P} is female.

\item \ntt{male(P)}: \ntt{P} is male.
\end{itemize}

For example these predicates can be defined  in ``database style'' by
 the following clauses:
\begin{alltt}
+hParent(a, f).           +male(a).         +female(c).
+hParent(a, g).           +male(b).         +female(d).
+hParent(b, f).           +male(f).         +female(g).
\ldots                       \ldots               \ldots
\end{alltt}


%% +hParent(b, g).           +male(p).         +female(h).
%% +hParent(c, h).           +male(z).         +female(q).
%% +hParent(d, h).                             +female(x).
%% +hParent(f, p).           
%% +hParent(f, q).           
%% +hParent(h, p).           
%% +hParent(h, q).           
%% +hParent(q, x).           
%% +hParent(q, z).           


Your task is to write clauses defining predicates for the following family
relationships:

\begin{enumerate}
\item \texttt{hGrandparent(Ch, G)}: \texttt{Ch} has a grandparent
  \texttt{G}.  (solved below as an example)
\item \texttt{hMother(Ch, M)}: \texttt{Ch}'s mother is \texttt{M}.
\item \texttt{hChild(P, Ch)}: \texttt{P} has a child \texttt{Ch}. 
\item \texttt{hSon(P, S)}: \texttt{P} has a son \texttt{S}.
\item \texttt{hSibling(S1, S2)}: \texttt{S1} has a sibling  \texttt{S2}.\\
(Clarification: let's consider two people siblings, if they share \textit{at
  least} one parent.)
\item \texttt{hCousin(C1, C2)}: \texttt{C1} has a cousin  \texttt{C2}.\\
(Clarification: cousins have parents who are siblings, in the above sense.)
\item \texttt{hAncestor(Ch, A)}: \texttt{Ch} has an ancestor  \texttt{A}.\\
(Clarification: a person's ancestors are: their parent, their parent's
  parent, their parent's parent's parent, etc.)
\end{enumerate}

Note that each of these definitions, except for the last, should be
transformed to a single clause.

Suggested steps, using the first task as an example:

\begin{itemize}
\item Start with writing a semi-formalized English sentence which describes
  how to check the given family relationship in terms of one or more other
  ones. The sentence should start with the specification of the
  predicate (the English sentence after the colon), followed by the word \textbf{if}:

\texttt{Ch} has a grandparent \texttt{G} \textbf{if} (\ldots).

The remaining part, (\ldots), should take the form of one or more sentences
separated by \textbf{and} (possibly also by \textbf{or}).  These sentences
should be selected from the ones appearing after a colon in the above
descriptions of the predicates. What you may change is only the naming of the
individuals concerned.

Also, you may need to add the text: ``there exist(s) \texttt{X} \ldots such
that'' in front of these sentences.

In the example:

\texttt{Ch} has a grandparent \texttt{G} \textbf{if} there exists
\texttt{P} such that \ntt{Ch} has a parent \texttt{P} \textbf{and} \ntt{P}
has a parent \texttt{G}.

\item Rewrite the text into a FOL implication $\leftarrow$ (drawn right to
  left):

$\forall \mathtt{Ch}, \mathtt{G}.(\mathtt{hGrandparent(Ch, G)} \leftarrow
  \exists \mathtt{P} . ( \mathtt{hParent(Ch, P)} \wedge \mathtt{hParent(P,
    G)}))$\ntt{.}
\item Rewrite the above formula to clausal form:
\begin{itemize}
\item Rewrite the implication to a disjunction:

$\forall \mathtt{Ch}, \mathtt{G}.(\mathtt{hGrandparent(Ch, G)} \vee \neg
  \exists \mathtt{P} . ( \mathtt{hParent(Ch, P)} \wedge \mathtt{hParent(P,
    G)}))$\ntt{.}
\item Move negation inside non-atomic formulas:

$\forall \mathtt{Ch}, \mathtt{G}.(\mathtt{hGrandparent(Ch, G)} \vee
  \forall \mathtt{P} . ( \neg \mathtt{hParent(Ch, P)} \vee \neg \mathtt{hParent(P,
    G)}))$\ntt{.}
\item Bring quantifiers outside:

$\forall \mathtt{Ch}, \mathtt{G}, \mathtt{P}.(\mathtt{hGrandparent(Ch, G)} \vee
   \neg \mathtt{hParent(Ch, P)} \vee \neg \mathtt{hParent(P, G)})$\ntt{.}

\item Transform to clause notation:
\ntt{+hGrandparent(Ch, G) -hParent(Ch, P) -hParent(P, G).}

\end{itemize}

Note that you need not go through the details of this transformation, it is
enough to provide the final form in clause notation.


\end{itemize}

For the predicate \ntt{hSibling} you need one more helper predicate:
\begin{quote}
\ntt{neq(X,Y)}: \ntt{X} is not equal to \ntt{Y}.
\end{quote}

You can think of this predicate as if defined by the following FOL formula:
\begin{quote}
$\mathtt{neq}(x, y) \leftarrow \neg ({x} = {y})$
\end{quote}


\end{document}







