%VERSION:	563S05/hw09-2005-03-30.tex
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
%
\documentclass[12pt]{article}

%FOR ASCII VERSION, COMMENT-OUT ABOVE LINE AND UNCOMMENT THE NEXT 3:
%ALSO:  CHANGE ANY OCCURRENCES OF "supertabular" TO "tabular"
% then use dvi2tty
%\documentclass{article}
%\textwidth 30em
%\hoffset -0.875in

\usepackage{amssymb,fullpage,times,mathptm}


%to draw a line across the page:
\newcommand{\blank}{\mbox{}\hrulefill\linebreak}

%uncomment this to make it double-spaced (default is single-spaced)
%\renewcommand{\baselinestretch}{2}


\parindent 0.5in

% the next line turns hyphenation OFF
\pretolerance=10000


\begin{document}

\noindent
\footnotesize
{\bf CSE 463/563, Spring 2005}
\hspace*{2in}
http://www.cse.buffalo.edu/$\sim$rapaport/563S05.html\\\\
\normalsize
\centerline{\bf Homework \#9}
\centerline{\bf\large  FOL:  Automated Theorem Proving }\\\\
\begin{center}
\begin{tabular}{|c|}
\hline
\small {\bf Last Update:  1 April 2005}
%\\\\
%\small Note:  NEW or UPDATED\\
%\small material is highlighted\\\hline
\\\hline
\end{tabular}
\end{center}

\begin{enumerate}
\item
%{\footnotesize Adapted from Russell \& Norvig, 3/e, Ch.~9, p.~316, \#9.4:}\\\\
For each of the following sets of pairs of atomic wffs, compute a most
general unifier if one exists.  If none exists, then state why not (e.g., state
which part of the unification algorithm fails).
	\begin{enumerate}
	\item
	$\{Q(c,b,c),~Q(y,z,x)\}$
	\item
	$\{R(h(b,c),~z),~R(z,~h(y,y))\}$
	\item
	$\{\mbox{\it Younger\/}(\mbox{\it son-of\/}(x),x),~\mbox{\it Younger\/}(\mbox{\it son-of\/}(y),\mbox{\it bill\/})\}$  (where `bill' is a constant)
	\item
	$\{\mbox{\it Knows\/}(\mbox{\it son-of\/}(x),x),~\mbox{\it Knows\/}(y,y)\}$
	\end{enumerate}

\item
%{\footnotesize Adapted from Russell \& Norvig, 3/e, Ch.~9, p.~318, \#9.18:}\\\\
From ``Horses are animals'', it follows that ``The head of a horse is the head of an
animal.''  (This was how Aristotle showed that classical logical ``syllogisms'' (inferences)
were not sufficient for doing all of logic; you need FOL to handle this problem.)  Demonstrate
that this inference is valid by carrying out the following steps:
	\begin{enumerate}
	\item
	Translate the premise and the conclusion into the language of FOL.
	Use 3 predicates, whose syntax and semantics are shown below:
		\begin{quote}
		$[[\mbox{\it Animal\/}(x)]] = [[x]]$ is an animal\\
		$[[\mbox{\it Horse\/}(x)]] = [[x]]$ is a horse\\
		$[[\mbox{\it Head\/}(x,y)]] = [[x]]$ is the head of $y$
		\end{quote}

	\item
	Negate the conclusion, and convert the premise and the negated conclusion
	to clause form, using the algorithm presented in lecture.

	\item
	Use resolution and refutation to show that the conclusion follows from the
	premise.  Be sure to show any MGUs that you might need.
	\end{enumerate}

\pagebreak
\item
	\begin{enumerate}
	\item
	Using the following syntax and semantics, translate the following English
	sentences (adapted from:  Carroll, Lewis (1896), {\it Symbolic Logic\/},
	reprinted in:  Lewis Carroll, {\it Symbolic Logic and the Game of Logic
	(both books bound as one)\/} (New York:  Dover, 1958)) into the language of FOL:
		\begin{quote}
		$[[d]]$ = this dish\\
		$[[N(x)]] = [[x]]$ is nice\\
		$[[P(x)]] = [[x]]$ is a pudding\\
		$[[W(x)]] = [[x]]$ is wholesome
		\end{quote}

		\begin{enumerate}
		\item\label{1}
		All puddings are nice.
		\item
		This dish is a pudding.
		\item\label{3}
		No nice things are wholesome.
		\item\label{4}
		(Therefore:) This dish is unwholesome.
		\end{enumerate}

	\item
	Convert each of your FOL translations of \ref{1}--\ref{3} and the
	{\it negation\/} of \ref{4} into clause form, using our algorithm
	from lecture.

	\item
	Use resolution, unification, and refutation to show that the inference
	is valid.  Be sure to show an MGU for each application of resolution.

	\end{enumerate}

\item
%{\footnotesize Adapted from Russell \& Norvig, 3/e, Ch.~9, p.~318--319, \#9.19:}\\\\
Here are 2 wffs in the language of FOL:
	\begin{description}
	\item[(A)]
	$\forall x \exists y [x \geq y]$
	\item[(B)]
	$\exists y \forall x [x \geq y]$
	\end{description}

	\begin{enumerate}
	\item
	Let the domain of interpretation be all natural numbers:  0, 1, 2, 3, {\ldots},
	and let [[$x \geq y$]] = ``$[[x]]$ is greater than or equal to $[[y]]$''.  Under this
	interpretation, translate (A) and (B) into English.

	\item
	Is (A) true under this interpretation?  Why?

	\item
	Is (B) true under this interpretation?  Why?

	\item
	Using resolution, try to prove that (A) follows from (B).
	Do this even if you think that (B) does not logically entail (A);
	continue until the proof breaks down and you cannot proceed
	(if it does break down).  Show the unifying substitution
	for each resolution step.  If the proof fails, explain exactly
	where, how, and why it breaks down.

	\item
	In the same way, try to prove that (B) follows from (A).
	\end{enumerate}
\end{enumerate}


\centerline{\fbox{\bf DUE: AT THE BEGINNING OF LECTURE, FRIDAY, APRIL 8}}
\ \vspace*{1in}
\ \\
\tiny
\copyright 2005, William J. Rapaport\\
rapaport@cse.buffalo.edu\\
http://www.cse.buffalo.edu/$\sim$rapaport/563S05/hw09.pdf
\end{document}

