\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\\
Spring Semester \os{2001}\\[16pt]

Assignment \#5 -- Propositional Logic: Resolution Refutation and Matching
\large
Due { \os{11}:\os{00}am}, Wednesday March \os{7}, \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:
\begin{itemize}
\item If the jar is heated, and the bug is in the jar, then the bug is dead.

\item The jar is heated.

\item The bug is in the jar.
\end{itemize}
If we wish to know whether the bug is dead, we can model this with the set of
formulas:
$$
\G = \{hj\imp (bij\imp bd),hj,bij\}
$$
and attempt to prove the consequence:
$$
\Gamma\models\ bd
$$

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}
