\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{\nov}[1]{{\overline #1}}
\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 2018.
Homework 3, given Nov 6, due Nov 13}

\bigskip

\bigskip

\noindent
1.
Transform into DNF:
\begin{enumerate}
\item[(a)] $(P \impl Q) \impl R$
\item[(b)] $\not (P \and Q) \and (P \or R)$
\end{enumerate}

\bigskip

\noindent
2.
Transform into CNF:
\begin{description}
\item[(a)] $(P \impl Q) \impl R$
\item[(b)] $(\not P \and Q) \or (P \and \not Q)$
\end{description}

\bigskip

\noindent
3.
Check the equivalence using a normal form of your choice:
\begin{description}
\item[(a)] $(P \impl Q) \and (P \impl R)\ \elc\ P \impl (Q \and R)$
\item[(b)] $(P \impl Q) \impl (P \and R)\ \elc\ (\not P \impl Q) \and (Q \impl P)$
\end{description}

\bigskip

\noindent
4.
Show that reduction to DNF is a complete method for proving unsatisfiability.

\bigskip

\noindent
5.
Show by resolution that the following set of clauses is unsatisfiable.
\begin{enumerate}
\item $A \or B$
\item $\nov A \or C \or D$
\item $C \or \nov D$
\item $\nov B \or \nov C$
\item $\nov A \or B \or \nov C$
\item $A \or \nov B \or C \or D$
\end{enumerate}

\bigskip

\noindent
6.
Apply DPLL to the set of clauses from exercise 5.

\end{document}
