\documentclass[10pt,letterpaper]{article}
\usepackage[latin1]{inputenc}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\title{
        CS444 HW \#5 
}
\author{}
\date{}


\begin{document}
\newcommand{\bq}{\item \begin{samepage} }
\newcommand{\eq}{\end{samepage}}
\maketitle

Answers to the following exercises should be prepared in a text editor
and submitted through blackboard as .pdf files. 


\begin{enumerate}


\bq 
Convert the following sentences into conjunctive normal form.  Show all steps. 
\begin{itemize}
\item $\lnot(A \Rightarrow B)$
\item $A \Rightarrow \lnot(B \vee C)$
\end{itemize}
\eq

\bq
Consider the following knowledge base:
\begin{itemize}

\item If Bob studied, then he passed the exam and he graduated. 

\item If Bob overslept, then he did not pass the exam.

\item Bob did not graduate.

\item Bob overslept.
\end{itemize}

Construct a resolution proof showing that Bob did not study.  Show all steps.

\eq

\bq Express the following knowledge base in first order logic using
the predicates Taller, SeesOver, CanRide, and HasTicket.
\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 If some first person can see over a second person's head, and that second person is taller than some third person, then the the first person is taller than the third person. 
\item Bob can see over Tim's head.
\item Tim can see over Alice's head.
\item Bob has a ticket. 
\end{itemize}
\eq

\bq Prove that Bob can ride the roller
coaster. Each step in your proof should explicitly invoke one of the
inference rules described in Chapters 7 or 9 and should state which
previous lines of the proof are being used.  
\eq

\bq Rewrite the knowledge base from question 3 as a set of Prolog
rules and facts.  Load your Prolog file into an interpreter and try some queries.  Include your entire database in your submission, along with the results of the following queries:
\begin{verbatim}
?- can_ride(tim).
?- can_ride(bob).
?- can_ride(X).
\end{verbatim}

\eq


\end{enumerate}

\end{document}
