\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 2017.
Homework 3, given Nov. 9, due Nov 16.}

\bigskip

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

\bigskip

\noindent
2. 
Discover the sequent rule for disjunction in the goal by using the rules for negation and conjunction.

\bigskip

\noindent
3.
Discover the rules for equivalence (in the assumptions and in the goals)
by using the rules for the other connectives. 

\end{document}


