\documentclass[12pt]{article}
\usepackage{amsfonts}

\voffset=-3.0cm
\hoffset=-2.6cm
\textwidth=17.5cm
\textheight=24cm

\renewcommand{\not}{\neg}
\newcommand{\nov}[1]{{\overline #1}} % negation by overbar
\renewcommand{\and}{\wedge}
\renewcommand{\or}{\vee}
\newcommand{\impl}{\Rightarrow}
\newcommand{\lequiv}{\Leftrightarrow} %equivalence as logical connective
\newcommand{\all}{\forall}
\newcommand{\exi}{\exists}
\newcommand{\elc}{\models}  % semantic logical consequence
\newcommand{\ylc}{\vdash}  % syntactic logical consequence
%\equiv is already defined for === semantic equivalence
\newcommand{\union}{\cup}
\newcommand{\intersect}{\cap}
\newcommand{\true}{{\mathbb{T}}}
\newcommand{\false}{{\mathbb{F}}}


\pagestyle{empty}

\begin{document}

{\bf Logic 1, WS 2006.
Homework 5, given Nov 30, due Dec 7}

\bigskip

\noindent
1. Construct a proof of the sequent:
$$A \or B,\ \not A \or C\ \ \ylc\ \ B \or C,$$
by using the sequent rules duscussed in the lecture.

\bigskip

\noindent
2.
Show by resolution that the following set of clauses in unsatisfiable:\\
$\{A \or B,\ \nov{A} \or B,\ A \or \nov{B},\ \nov{A} \or \nov{B}  \}.$ 

\bigskip

\noindent
3. Consider the theorem:
$$ A \or B \or C,\ C \impl (A \or B),\ A \impl (B \or C),\ (A \and B) \impl C
\ \ \elc\ \ (\overline A \and B) \or (A \and C).$$
Construct the refutation formula corresponding to this theorem
(The refutation formula of
$\phi_1, \ldots,  \phi_n \elc \psi$ is
$\phi_1 \and \ldots  \phi_n \and (\not \psi)$)
and the set of clauses corresponding to it.


\bigskip

\noindent
4. Show by resolution that this set of clauses is unsatisfiable.

\bigskip

\noindent
5. Use the Davis-Putnam procedure in order to show that the set of clauses
from the previous example is unsatisfiable.


\end{document}
