%VERSION:	563S05/hw08-2005-03-23.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 \#8:}
\centerline{\bf CLAUSE FORM}\\\\

\begin{center}
\begin{tabular}{|c|}
\hline
\small {\bf Last Update:  23 March 2005}\\\\
\small Note:  NEW or UPDATED\\
\small material is highlighted\\\hline
\end{tabular}
\end{center}

\noindent
Convert each of the following FOL wffs to clause form, as defined by
the algorithm presented in lecture.  
For partial credit, show all your work,
and justify each step using the algorithm's numbering scheme.

\begin{enumerate}
\item
$(P \wedge Q) \vee (R \wedge S)$
\item
$\exists x \forall y \exists z \exists w \forall u \forall v \exists t.P(x,y,z,w,u,v,t)$
\item
$\exists x[S(x) \wedge \forall y[S(y) \supset y=x]]$
\item
$\exists x \forall y [ \neg S(y,y) \supset S(x,y)]$
\item
{\bf Do *NOT* attempt this one unless your mind is entirely clear and
you have nothing else to do.  But, if you find yourself in that
situation, you might find this sort of fun to try~:-)}\\
$(P \equiv Q) \equiv (\neg P \equiv \neg Q)$
\end{enumerate}


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

