
\newcommand{\ig}[1]{}
\documentclass[12pt]{article}
\usepackage[dvips]{graphicx}
\usepackage{shortvrb}
\usepackage{epsfig}

\ig{
\topmargin=0in
\textheight=8.5in
\textwidth=6.5in
\oddsidemargin=-.5in
\pagestyle{plain}
}

\setlength{\textwidth}{6.5in}
\setlength{\textheight}{9.0in}
\setlength{\topmargin}{-.5in}
\setlength{\oddsidemargin}{-.0600in}
\setlength{\evensidemargin}{.0625in}

\MakeShortVerb{\|}

\begin{document}
\noindent
{\bf CSCE476/876 \hfill Fall 2020}

\begin{center}
{\bf\large Homework 8 UPDATED}
\end{center}

\begin{description}
\item[Assigned on:] Wednesday November 4 2020.
\item[Due:]  Wednesday November 18, 2020. 
\end{description}

\noindent This homework is a pen-and-paper homework, to be returned in class or with web handin.\\
\noindent The homework is worth 192 points, plus 40 bonus points.  \\

\hrule

\vspace{\baselineskip}

\tableofcontents
\vspace{\baselineskip}

\hrule

\section {Using the inference rules for logic \hfill{\bf (10 points)}}
prove that ``$\exists\, x Z(x)$
follows from the givens.''  Be sure to justify your steps by stating
the inference rule used, along with the previous line(s) to which it
was applied and the unifications used. 
\begin{enumerate}
\item \hspace{1cm}
$P(1)$ \hfill{given}

\item \hspace{1cm}
$W(1) \wedge W(2) \wedge W(3)$ \hfill{given}

\item \hspace{1cm}
$\forall x [P(x) \Rightarrow \neg R(x)]$ \hfill{given}

\item \hspace{1cm}
$\forall x [Q(x) \vee R(x)]$ \hfill{given}

\item \hspace{1cm}
$\forall x [(Q(x) \wedge W(x)) \Rightarrow Z(x)]$ \hfill{given}

\end{enumerate}
\vspace{0.2cm}


\section {AIMA 8.4, page 315. \hfill{\bf (2 points)}}

\section {AIMA 8.9, page 316. \hfill{\bf (19 points)}}
\section {AIMA 8.24, page 319. \hfill{\bf (12 points)}}


\section {Axioms in FOL (Adapted from AIMA, first edition) \hfill{\bf (15 points)}}

Using the following:

\begin{center} |Child(x,y)|, |Sibling(x,y)|, |Female(x)|, |Male(x)|, and |Spouse(x, y)| \end{center}

\begin{itemize}
\item (10 points) Write axioms describing the predicates: |GrandChild|,
|GreatGrandParent|, |Brother|, |Sister|, |Daughter|, |Son|, |Aunt|,
|Uncle|, |BrotherInLaw|, |SisterInLaw|, and |FirstCousin|.  We want
these axioms to be definitions, so use $\Leftrightarrow$ instead of
$\Rightarrow$.
\item (5 points) Knowing that a second cousin is a child of one's parent 
 first cousin, write the definition of a $N^{th}$|-cousin|, as a
 recursive expression in terms of the predicates defined above.  Hint:
 Let $N^{th}$|-cousin| be a ternary predicate, that takes as input
 $n$, and two persons $p_1$ and $p_2$.
\end{itemize}



\section {AIMA 9.3, page 361. \hfill{\bf {(3 points)}}}

\section {AIMA 9.4, page 361. \hfill{\bf {(4 points)}}}

\section {AIMA 9.6, page 361. \hfill{\bf {(12 points)}}}

\section {AIMA 9.13, page 363. \hfill{\bf {(12 points)}}}

For question (d), it is useful to check the following reference:
Smith, D.E., Genesereth, M.R., and Ginsberg, M.L. (1986).  {\em Controlling
recursive inference.} Artificial Intelligence, Volume 30 (3), pages
343--389.  (Page 1036, AIMA2e)

\section {First-Order Logic \hfill{\bf (20 points)}}

Consider the following axioms:
\begin{enumerate}
\item
Anyone who rides any Harley is a rough character.
\item
Every biker rides [something that is] either a Harley or a BMW.
\item
Anyone who rides any BMW is a yuppie.
\item
Every yuppie is a lawyer.
\item
Any nice girl does not date anyone who is a rough character.
\item
Mary is a nice girl, and John is a biker.
\item
(Conclusion) If John is not a lawyer, then Mary does not date John.
\end{enumerate}
\begin{itemize}
\item
Choose appropriate predicates to write the above axioms in first-order
logic, clearly indicating the arguments and arity of each predicate:
\hfill{(2 points)}

\item 
Write each of the above axioms in first-order logic.  Use scratch
paper if necessary, and {\em neatly\/} report your results below. \hfill{(10
points)}
\begin{enumerate}
\item
\mbox{}
\vfill
\item
\mbox{} 
\vfill
\item
\mbox{}
\vfill
\item
\mbox{}
\vfill
\item
\mbox{}
\vfill
\item
\mbox{}
\vfill
\item
\mbox{}
\vfill
\end{enumerate}

\item 
Transform each of the above sentences into a conjunctive normal form.
Clearly state the Skolem functions and clearly number the statements.
\hfill{(4 points)}

\item
Establish the conclusion using the axioms by applying refutation
resolution.  Clearly show the variable bindings at each step and
clearly number the statements.

\hfill{(4 points)}

Negation of conclusion:


\end{itemize}


\section{Unification \hfill{\bf (4 points)}}
What is the most general unifier of the following pairs of wff's? If
none exists, report ``fail.''  Assume that the capital letters are
constants and the lowercase letters are variables.   
\begin{enumerate}
\item 
$P(x, y, x, z)$ and $P(F(w), A, F(B), w)$

\item 
$Q(x, F(x), G(F(x)))$ and $Q(1, y, G(F(y)))$

\item 
Foo($x,y$) and Foo($y,x$)

\item
Mother($x,y$) and Mother($y$,Father($x$)

\end{enumerate}

\section{Unification and Resolution \hfill{\bf (2 points)}}
You are given the following pairs of clauses where upper case letters
indicate constants and lower case letters indicate variables,
functions, or predicates.  Consider each pair independently of the
others.  In each pair, variables with the same name are meant to be
the same variable.  For each of the pairs, specify if the two clauses
can be \underline{resolved}. If yes, show the results of the
unification process.  If not, explain why.
\begin{enumerate}
\item
$p(B, C, x, z, f(A, z, B))$ and $\neg p(y, z, y, C, w)$.

\item
$r(f(y), y, x)$ and $\neg r(x, f(A), f(v))$.

\end{enumerate}


\section{Resolution and Refutation \hfill{\bf (5 points)}}
Use resolution and refutation to solve the problem below.  Hint: First
transform the givens into clausal form.\\
Given:
\begin{enumerate}
\item
$\forall x (P(x) \Rightarrow Q(x))$

\item
$\forall x (P(x) \Rightarrow (\forall y W(y))$

\item
$\forall x \forall y ((Q(x)\wedge W(y)) \Rightarrow S(x))$

\item $P(Mary)$
\end{enumerate}
Show: $S(Mary)$

\section{Translation into FOL \hfill{\bf (14 points)}}

Consider the set of all creatures. We will use the following predicates:
\begin{itemize}
\item 
$Insect(x)$.

\item 
$Moth(x)$.

\item 
$Dragonfly(x)$.

\item 
$Spider(x)$.

\item 
$Eats(x,y)$.

\item 
$Wings(x,y)$: $x$ has $y$ wings.

\item 
$Order(x)$. (Recall that zoologists classify creatures using kingdom,
phylum, class, order, family, genus, and species.)
\end{itemize}

Translate the following sentences into logic.  You may only use the
identity predicate and the predicates and functions listed above.  Try
not to include more bugs in your logic than are required..
\begin{itemize}
\item
Flik is an insect with 4 wings but is not a moth.

\item
Not all insects have 4 wings.

\item
All insects with 2 wings are in the same order.

\item
There are at least 3 difference orders.

\item
Moths and Dragonflies are insects but are not in the same order.

\item
All spiders eat insects.

\item 
Some spiders eat only insects.
\end{itemize}



\section{Inference in First-Order Logic: CNF and Resolution \hfill{\bf(60 points + 40 Bonus)}}

Choose {\em three} (3) of the exercices below, and for each of them,
answer each of the following questions.  The remaining two exercises
are bonus, each worth 20 points.
\begin{itemize}
\item
Choose appropriate predicates to write the above axioms in first-order logic.
\item 
Write the axioms in First-Order Logic.  Report your results neatly. 
\item 

Transform each of the first-order sentences into Conjunctive Normal Form.
Clearly state the Skolem functions and clearly number the statements.
Neatly report your results and  provide as much detail as possible.

\item
Establish the conclusion using the axioms by applying {\em refutation
resolution}.  That is, negate the conclusion and prove the
unsatisfiability of the set of clauses by resolution.
Clearly show the variable bindings at each step and
clearly number the statements.  

\end{itemize}


\subsection{Do Loons Eat Fish? \hfill{\bf (20 points)}}

Consider the following axioms.
\begin{enumerate}
\item
Every bird sleeps in some tree.

\item
Every loon is a bird, and every loon is aquatic.

\item
Every tree in which any aquatic bird sleeps is beside some lake.

\item
Anything that sleeps in anything that is beside any lake eats fish.

\item
(Conclusion) Every loon eats fish.
\end{enumerate}

\subsection{Is there a conservative Austinite? \hfill{\bf (20 points)}}

Consider the following axioms:

\begin{enumerate}
\item
Every Austinite who is not conservative loves some armadillo.

\item
Anyone who wears maroon-and-white shirts is an Aggie.

\item
Every Aggie loves every dog.

\item
Nobody who loves every dog loves any armadillo.

\item 
Clem is an Austinite, and Clem wears maroon-and-white shirts.

\item
(Conclusion) Is there a conservative Austinite?

\end{enumerate}


\subsection{Will Mary Date John? \hfill{\bf (20 points)}}
Consider the following axioms:
\begin{enumerate}
\item
Anyone who buys carrots by the bushel owns either a rabbit or a
grocery store.

\item
Every dog chases some rabbit.

\item
Mary buys carrots by the bushel.

\item
Anyone who owns a rabbit hates anything that chases any rabbit.

\item
John owns a dog.

\item
Someone who hates something owned by another person will not date that
person.

\item
(Conclusion) If Mary does not own a grocery store, she will not date
John.
\end{enumerate}

\subsection{Drunk AI Students \hfill{\bf (20 points)}}
Consider the following axioms.
\begin{enumerate}
\item
Everyone who feels warm either is drunk, or every costume they have is
warm.

\item
Every costume that is warm is furry.

\item
Every AI student is a CS student.

\item
Every AI student has some robot costume.

\item
No robot costume is furry.

\item
(Conclusion) If every CS student feels warm, then every AI student is
drunk.
\end{enumerate}



\subsection{Brilliant CS Students \hfill{\bf (20 points)}}
Consider the following axioms:
\begin{enumerate}
\item
Every student who makes good grades is brilliant or studies.

\item
Every student who is a CS major has some roommate.
[Make ``roommate'' a two-place predicate.]

\item
Every student who has any roommate who likes to party goes to Sixth
Street.

\item
Anyone who goes to Sixth Street does not study.

\item
(Conclusion) If every roommate of every CS major likes to party, then
every student who is a CS major and makes good grades is brilliant.

\end{enumerate}




\end{document}


