\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 2015.
Homework 3, given Oct 29, due Nov 5.}

\bigskip

\noindent
1. Prove by reducing both sides to CNF:
$$ ((A \and B) \impl C)\ \equiv\ ((A \impl C) \or (B \impl C)).$$

\bigskip

\noindent
2. Show validity by reducing to CNF:
$$ ((A \and B) \impl C)\ \impl\ ((A \impl C) \or (B \impl C)).$$

\bigskip

\noindent
3. Prove using the $\not \and$-sequent calculus:
$$ \not P,\ \not((\not P) \and Q)\ \ \ylc\ \ \not Q $$

\bigskip

\noindent
4. Prove by refutation, reduction to CNF, and resolution:
$$ ((A \impl C) \or (B \impl C))\ \impl\ ((A \and B) \impl C)$$ 

\bigskip

\noindent
5. Prove the correctness of the sequent rules for disjunction in the assumptions ($\and \ylc$)
and for negation in the goal ($\ylc \not$).
\end{document}
