\documentclass[12pt]{article}

\usepackage{proof}
\usepackage{fullpage}

\newcommand\os[1] {$\mit{#1}$}
%\newcommand\os[1]{#1}
 
\newcommand\imp\Rightarrow

%\input{qobitree}
\pagestyle{empty}

\begin{document}

\begin{center}
\large 
%\vspace*{-1.5cm}
Harvey Mudd College\\
Computer Science \os{80}\\
Logic for Computer Science\\
Fall Semester \os{2001}\\[16pt]

Assignment \#5 -- Propositional Logic: Resolution Refutation and Matching
\large
Due { \os{11}:\os{00}am}, Friday November \os{2}, \os{2001}
\end{center}

\vspace{0.25in}


\newcommand{\G}{\Gamma}
\newcommand{\D}{\Delta}
\newcommand{\lra}{\longrightarrow}

\begin{enumerate}

\item Consider the set of numbered clauses:
$$
\stackrel{1}{a\lor\neg b\lor c}    \qquad 
\stackrel{2}{b\lor c \lor \neg d}  \qquad
\stackrel{3}{b\lor \neg c\lor e \lor \neg f} \qquad
\stackrel{4}{c \lor d \lor g} 
$$

For each pair of clauses show all possible resolvents of the pair.


\vfill 

\item Consider the set of assumptions:
\begin{itemize}
\item Every fungus is either a mushroom or a toadstool.

\item Every boletus is a fungus.

\item Toadstools are poisonous, as are peach pits.

\item A boletus is not a mushroom.

\item This thing is a boletus.
\end{itemize}
If we wish to know whether ``this thing'' is poisonous, we can model this with the set
of formulas:
$$
\G = \{f\imp(m\lor t),b\imp f, (pp\lor t)\imp p, b\imp\neg m, b\}
$$
and attempt to prove the consequence:
$$
\Gamma\models\ p
$$

Construct the corresponding implication, convert its negation 
to conjunctive normal form, and produce a resolution refutation tree
showing that the consequence holds.

\vfill\hfill{\bf (over)}

\pagebreak

\pagebreak 

\item Consider the set of assumptions and the conclusion from problem 2.

Construct the corresponding implication, convert it (not it's negation)
to CNF, and use the ``simple'' validity tester to show that the original consequence 
holds.

\end{enumerate}

\end{document}
