\documentclass[12pt]{article}
\usepackage{amsfonts}
 
\voffset=-3.0cm
\hoffset=-2.6cm
\textwidth=17.5cm
\textheight=24cm

\renewcommand{\not}{\neg}
\newcommand{\ovneg}[1]{{\overline{#1}}}
\newcommand{\aand}{\wedge}
\newcommand{\oor}{\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 Automated Reasoning, WS 2017.
Homework 2, given Nov 29, due Dec 6}

\bigskip

\bigskip

\noindent
Apply the DPLL algorithm to the following set of clauses:

$A \oor B \oor \ovneg C,\ \ \ovneg A \oor C \oor \ovneg D,\ \ B \oor C,$

$B \oor \ovneg C \oor D,\ \ \ovneg A \oor D, \ \ A \oor \ovneg C \oor \ovneg D,$

$\ovneg B \oor \ovneg C,\ \ \ovneg A \oor B \oor \ovneg C \oor \ovneg D,\ \
   A \oor \ovneg B \oor C$


\bigskip

\noindent
2.
Study what happens in the DPLL algorithm if the last clause is missing.

\bigskip

\noindent
3.
Show by refutation, normal form, and resolution that $G$ is a semantical logical consequence of $F_1, F_2$.

$F_1:\ \ \exi_x(P[x] \aand \all_y(D[y] \impl L[x, y]))$

$F_2:\ \ \all_x(P[x] \impl \all_y(Q[y] \impl \neg L[x, y])),$

$G:\ \ \all_x(D[x] \impl \neg Q[x]).$

\end{document}
