\documentstyle[12pt]{article}

\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}
\newcommand{\all}{\forall}
\newcommand{\exi}{\exists}
\newcommand{\elc}{\models}  % semantic logical consequence
\newcommand{\ylc}{\vdash}  % syntactic logical consequence
\newcommand{\union}{\cup}
\newcommand{\intersect}{\cap}


\pagestyle{empty}

\begin{document}

{\bf Logic 1, WS 2004.
Homework 5, given Nov 04, due Nov 11}

\bigskip

\noindent
1. Prove that if the formula $P(a)$ is satisfiable, then the formula
$\exi_x P(x)$ is also satisfiable.

\bigskip

\noindent
2. Prove that if the formula $\all_x \exi_y P(x,y)$ is satisfiable,
then the formula $\all_x P(x, f(x))$ is also satisfiable.


\bigskip

\noindent
3. Explain how to construct the Herbrand universe for the formula
$$ \all_x (P(f(x), a) \impl Q(b, g(x))).$$

\bigskip

\noindent
4. Bring into the Skolem normal form the negation of the formula:
$$((\all_x (P(x) \impl (Q(x) \and R(x))))\ \and\ (\exi_x (P(x) \and S(x))))
\impl (\exi_x (R(x) \and S(x))).$$


\bigskip

\noindent
5. Use the resolution method in order to infer the empty clause from the
clauses of the formula obtained above.

\end{document}