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

\renewcommand{\not}{\neg}
\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 2013.
Homework 3, given Dec 2, due Dec 11}

\bigskip

\bigskip

\noindent

From the book by Chang and Lee:

page 42, ex. 3, ex. 6 (a, b);

page 43, ex. 9 (1, 2);

page 67, ex. 1: (b);

page 69, ex. 15;

page 98, ex. 6: (1, 3, 5), ex. 8 (1).

Prove unsatisfiability by resolution:

(1) $\{\neg P(x) \oor Q(f(x,x),\ P(g(b)),\ \neg Q(f(g(b)), g(b)) $


(2) $\{P(x),\ Q(x, f(x)) \oor \neg P(x),\ \neg Q(g(y), z) $



\end{document}
