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

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

\renewcommand{\not}{\neg}
\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 2008.
Homework 4, given Nov 20, due Nov 27.}

\bigskip

\noindent
1.
Complete the proof of the correctness of the resolution rule as done in the
lecture.

\bigskip

\noindent
2.
Construct sequent calculus proofs for at least two of the following formulae:
\begin{itemize}
\item $((A \impl C) \and (B \impl C))\ \impl\ ((A \or B) \impl C)$
\item $((A \or B) \impl C)\ \impl\ ((A \impl C) \and (B \impl C))$
\item $((A \impl C) \or (B \impl C))\ \impl\ ((A \and B) \impl C)$
\item $((A \and B) \impl C)\ \impl\ ((A \impl C) \or (B \impl C))$
\end{itemize}

\end{document}