\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}}}
\newcommand{\nov}[1]{{\overline #1}}

\pagestyle{empty}

\begin{document}

{\bf Computational Logic, WS 2018.
Homework 5, given Nov 12, due Nov 19}

\bigskip

\bigskip

\noindent
1. (Optional)
Apply the resolution algorithm to the following set of clauses
(just try to produce short clauses and delete subsumed ones).

$A \or B \or \nov C,\ \ \nov A \or C \or \nov D,\ \ B \or C,$

$B \or \nov C \or D,\ \ \nov A \or D, \ \ A \or \nov C \or \nov D,$

$\nov B \or \nov C,\ \ \nov A \or B \or \nov C \or \nov D,\ \
   A \or \nov B \or C$

\bigskip

\noindent
2.
Apply the DPLL algorithm to the set of clauses from the previous exercise.

\bigskip

\noindent
3. 
Prove in natural style, using inference rules of your choice:

$(A \and B) \impl C\ \lequiv\ (A \impl C) \or (B \impl C)$

$(A \or B) \impl C\ \lequiv\ (A \impl C) \and (B \impl C)$

\end{document}
