\documentclass[12pt,letterpaper]{article}
\usepackage[top=1in, bottom=.75in, left=1in, right=1.2in]{geometry}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{nopageno}
\usepackage[pdftex]{graphicx}
\usepackage{pstricks,pst-node,pst-tree}
\usepackage[bottom]{footmisc}
%\pagenumbering{empty}

% \pagestyle{myheadings}
% \markboth{}{ Name:\underline{ \hspace{2in} }}

\newcommand{\bq}{\item \begin{samepage} }
  \newcommand{\eq}{\end{samepage}\vspace{.2in}}

%-----------------------------------
\begin{document}
%-----------------------------------
\vspace*{-.75in}

\begin{center}
{\Large CS444 Predicate Logic Proofs} 
\end{center}

\begin{enumerate}

\bq
Consider the following knowledge base:\footnote{This is a slightly simplified version of question 12.7 from {\emph{Artificial Intelligence: Foundations of Computational Agents}, David Poole and
Alan Mackworth, Cambridge University Press, 2010.}}


\begin{enumerate}
\item $has\_access(X,library) \leftarrow student(X).$
\item $has\_access(X,library) \leftarrow faculty(X).$
\item $has\_access(X,library) \leftarrow has\_access(Y,library) \land parent(Y,X).$
\item $faculty(diane).$
\item $faculty(ming).$
\item $student(william).$
\item $parent(diane, karen).$
\item $parent(diane, robin).$
\item $parent(karen, todd).$
\end{enumerate}

Provide an SLD derivation of the query \texttt{ask} $has\_access(todd, library)$.  Quoting from our textbook: 
\begin{quote}
The main difference between this and the propositional top-down proof
procedure is that, for clauses with variables, the proof procedure
must take copies of clauses from the knowledge base. The copying
renames the variables in the clause with new names. This is both to
remove name clashes between variables and because a single proof may
use different instances of a clause.
\end{quote}

I've started the derivation for you, by creating the answer clause,
and making the first two substitutions.  For the sake of consistency, your
derivation should always attempt to match the left-most atom in the
body of the current answer clause.  See figure 12.4 in our textbook
for an example of appropriate formatting.

$yes() \leftarrow has\_access(todd, library)$

\hspace{.5in} Resolve with (c) above using  the substitution \{$X$/$todd$\}.

$yes() \leftarrow has\_access(Y_1, library) \land parent(Y_1, todd)$

\hspace{.5in} Resolve with (c) above using  the substitution \{$X$/$Y1$\}.

$yes()  \leftarrow has\_access(Y_2, library) \land parent(Y_2, Y_1) \land parent(Y_1, todd)$

\eq
\pagebreak

\bq
Express the following knowledge base in first order logic using
the predicates\\ 
$T(x, y)$  - x is taller than y.\\
$S(x, y)$ - x can see over the head of y.\\
$C(x)$ - x can ride the coaster.\\
$H(x)$ - x has a ticket.\\

\begin{itemize}
\item Anyone who has a ticket and is taller than Alice can ride the roller coaster. 
\item Anyone who can see over another person's head is taller than that person.
\item Bob can see over Alice's head.
\item Bob has a ticket or no one has a ticket.
\item Alice has a ticket.
\end{itemize}
\vspace{2in}
\eq

\bq Convert your first order knowledge base from the previous question
to clausal form. (Conjunctive normal form with all quantifiers removed).
\vspace{2in}
\eq

\pagebreak
\bq Construct a resolution proof that Bob can ride the roller coaster. 

\eq





\end{enumerate}
%-------------------------
\end{document}
%-------------------------







