%
%
%
%
%
%
%
%
%NAME AND DATE OF THIS FILE:	563S05/Proj1/proj1-2005-03-28.tex
%
%
%
%
%
%
%
%
%
\documentclass[12pt]{article}

\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
{\bf CSE 463/563, Spring 2005}

\begin{center}
{\bf Programming Project 1\\
AUTOMATED THEOREM PROVING}\\[\bigskipamount]
\end{center}


\noindent
In this project, you will write programs that could have passed the CS
department's old graduate-level AI
Qualifying Exam questions on logic~:-)\\

\noindent
As described in the syllabus,
your final report should be a conference-style paper containing
your {\bf annotated} code and {\bf commented} sample runs either as
appendices or incorporated into the body of the report.

\begin{enumerate}
\item\label{clauseform}
{\bf (WARNING:  THIS PART IS RELATIVELY EASY.)}
\begin{enumerate}
\item
In lecture, you will be given an
algorithm for {\bf converting a sentence of first-order
logic into ``clause form''} (this algorithm will be on the Web
at:
\begin{quote}
http://www.cse.buffalo.edu/$\sim$rapaport/563S05/clause-form.pdf\\
and\\
http://www.cse.buffalo.edu/$\sim$rapaport/563S05/clause-form.html).
\end{quote}

\noindent
Using your favorite programming language, write a fully-commented algorithm
(e.g., a Lisp function)
that takes a well-formed formula of first-order logic
as input and that returns an
equivalent sentence in clause form.

\begin{quote}
{\bf Suggestion 1:}
You should choose an input notation for wffs that is convenient for the
programming language that you are using.  E.g., for Lisp,
	\begin{quote}
	\begin{verbatim}
	(^ P Q)
	\end{verbatim}
	\end{quote}
might be more convenient than:
	\begin{quote}
	$(P \wedge Q)$
	\end{quote}
You do not need to write a parser (i.e., a compiler) that converts our
text's FOL notation for wffs into yours.  All you need to do is write a
program that converts your notation into clause form.
\end{quote}

\begin{quote}
{\bf Suggestion 2:}
When you rename variables so that variables bound by different
quantifiers have unique names, you can
use rewrite rules of the following form:
\[
(Q_{1} v_{1} F( v_{1}^{*})~\#~Q_{2} v_{1} G( v_{1}^{*}))
\rightarrow
(Q_{1} v_{1} F( v_{1}^{*})~\#~Q_{2} v_{2} G( v_{2}^{*}))
\]
where the $Q_i$ are quantifiers (either the same or different),
\# is either $\vee$ or $\wedge$, the $v_i$ are variables such that
`$v_1$' $\neq$ `$v_2$', and `$F( v_{1}^{*})$' represents a sentence
containing 0 or more occurrences of `$v_1$'.  An example would be:
\[
(\forall x  P(a,x) \wedge \exists x  R(a))
\rightarrow
(\forall x  P(a,x) \wedge \exists y  R(a))
\]
\end{quote}
\normalsize
\item
Apply your algorithm to the following sentence:
\[
\forall x [ Animal(x) \supset (Predator(x) \equiv
                                  \exists y [ Animal(y) \wedge Eats(x,y)])]
\]
\end{enumerate}

\pagebreak

\item\label{unification}
{\bf (WARNING:  THIS PART IS RELATIVELY HARD.)}
\begin{enumerate}
\item
Preferably using the same programming language as for the previous part
of this project (since the two parts will eventually need to
communicate),
implement a fully-commented
{\bf unification algorithm} (either the one in Brachman \& Levesque, the version of that algorithm
(to be)
given in lecture, or one that you find documented elsewhere; please be
sure to give a full citation to whichever version you choose).

More precisely, your algorithm should take a pair of
sentences as input and either return a most general unifier (MGU) for
them, if they are unifiable, or else
return a message such as ``NOT UNIFIABLE''.
(Again, you may assume that
the notation $f(x, g(x))$ can be understood as: {\tt (f x (g x))},
if you prefer using Lispish notation.)
\item
Use your algorithm to answer the following question: For each of the
following pairs of terms, if they unify, show an
MGU; if they don't, say so, and state why. (Note: You only need to
state {\it in your report\/} why a unification failed.  Although a ``trace''
of your unification algorithm might be useful, your {\it program\/} does not
have to indicate exactly where unification failed).  Assume that $u$,
$v$, $x$, $y$, and $z$ are variables, and that $a$, $b$, and $c$ are
individual constants:
\begin{enumerate}
\item
$P(a,x,c)$ and $P(y,b,z)$
\item
$P(a,x,c)$ and $P(y,b,y)$
\item
$P(x,x,c)$ and $P(u,v,u)$
\item
$P(x, f(x), f(y))$ and $P(f(a), f(z), z)$
\item
$P(x, f(x), f(a))$ and $P(f(z), f(z), z)$
\end{enumerate}
\end{enumerate}


\pagebreak

\item
\begin{enumerate}
\item\label{3a}
{\bf (WARNING:  THE COMPUTATIONAL IMPLEMENTATION OF THIS PART IS RELATIVELY HARD.)}\\
Write a {\bf resolution + unification + refutation
theorem prover} for {\it first-order predicate\/} logic.

To do this, you will need to incorporate the two previous parts of the
project into a fully-commented
theorem prover that uses a resolution algorithm with a
refutation strategy.  You may either write such an algorithm from
scratch (recommended, but difficult) or adapt one that you find
elsewhere.  If you choose the latter option, please keep the following
in mind:

\begin{itemize}
\item
You must give a full citation for the algorithm that you use.
\item
You must fully comment the algorithm so that the reader of your report
can understand it (this is especially important if the reader is not
fluent in the programming language that the algorithm is written in) and
so that {\it we\/} know that {\it you\/}  understand it!
\item
Although this option has (as the philosopher Bertrand Russell once
commented) all the advantages of theft over honest toil, it is not
necessarily going to be easier than writing your own, since you will
have to fully understand the one you will be using and you will probably
have to either adapt it to work with the previous components of this
project or else adapt those previous components to work with {\it it\/}.
\end{itemize}

There are several strategies for selecting two target clauses to
resolve. Instead of implementing one or more of these strategies, your program
can ask the user to input two clauses for resolution (i.e., this
aspect of resolution need not be automated).  This interaction can
take place with each pass through the algorithm.

Since this part of the project relies on a working implementation of
the clause-form converter and unification algorithm (from parts~\ref{clauseform} and~\ref{unification}, you should test
those implementations thoroughly before you implement this part.  If
you find that you are getting stuck on one of the first two parts (and
\emph{only if} you are getting stuck), you should ``hand code'' the
clause form inputs or unified results for this part.  In general, you should 
``hand code'' anything in your automated theorem prover that you are unable to automate.
 
\newpage
\item\label{resolution}
{\bf DO PART~\ref{resolution} (AT LEAST BY HAND) WHETHER OR NOT YOU ARE ABLE TO DO PART~\ref{3a}.}\\
This part is inspired by an example in Moore 1982: 429;
in your report,
explain the relationship between Moore's example and this problem:
Using resolution, show that the following set of clauses is
inconsistent.  Assume that $a$, $b$, and $c$ are individual constants,
and that $x$ and $y$ are variables:
\begin{enumerate}
\item
$[Next$-$to(a,b)]$
\item
$[Next$-$to(b,c)]$
\item
$[Green(a)]$
\item
$[\neg Green(c)]$
\item
$[\neg Green(x), Green(y), \neg Next$-$to(x,y)]$
\end{enumerate}
\end{enumerate}
\end{enumerate}
\ \\[\bigskipamount]
\textbf{NOTE:  Please do \textit{all\/} exercises at least \textit{by hand\/}
(in addition to, or instead of, implementing them in a programming
language) as part of your \textit{report\/}.
I will hand out a tentative grading scheme to make it easier for you to
organize your final report.}
\ \\[\bigskipamount]
\centerline{********** NEW **********}\\
\centerline{\fbox{\bf DUE AT START OF LECTURE, {\itshape FRIDAY, APRIL 15}.}}
\centerline{********** NEW **********}\\
\end{document}


\end{document}

