\begin{slide}{Übung zur Prädikaten-Logik}

  \begin{itemize}\itemsep 0pt\parskip 2pt
  \item Die folgende Formel $E$ ist erfüllbar. 
\begin{eqnarray*}
( \forall x: P(x,f(x)) ) \wedge ( \forall y:\neg P(y,y) ) \\
\wedge (\forall u:\forall v:\forall w: ((P(u,v)\wedge P(v,w))\rightarrow P(u,w))
\end{eqnarray*}
Bestimmen Sie ein Modell mit
möglichst kleinem Universum.

\item Geben Sie eine (kleine) erfüllbare Formel $F$ an, 
so daß jedes Modell von $F$ wenigstens 5 Elemente enthält.

\item Beweisen Sie:  Erfüllbarkeit ist bereits
für Formeln ohne Funktionssymbole unentscheidbar.

Geben Sie dazu ein Verfahren an, das aus einer beliebigen Formel $F$
eine Formel $G$ \emph{ohne Funktionssymbole} erzeugt,
so daß gilt: $F$ besitzt Modell $\iff$ $G$ besitzt Modell.
Hinweis: zusätzliche Relationssymbole.

Wenden Sie das Verfahren auf die o.g. Formel $E$
 (und das von Ihnen gefundene Modell) an.

\item Beweisen Sie, daß Erfüllbarkeit und Allgemeingültigkeit 
  entscheidbar sind für Formeln,
  \begin{itemize}
  \item die nur nullstellige Rel.-Symbole und keine Fkt.-Symbole enthalten,
  \item die nur einstellige Rel.-Symbole und keine Fkt.-Symbole enthalten.
  \end{itemize}
  Hinweis: es genügt, endliche Modelle bis zu einer gewissen Größe 
  zu betrachten.
  \end{itemize}

(vgl. Uwe Schöning: Logik für Informatiker, Spektrum)

\end{slide}

\begin{slide}{Übung zu Termgleichungen}

  \begin{itemize}\itemsep 0pt
  \item sind die Substitutionen $\sigma_1=\{X\mapsto Y\}$
    und $\sigma_2=\{Y\mapsto X\}$ vergleichbar bzgl. $\leq$?
  \item $\le$ auf Substitutionen ist keine Halbordnung.

    Die durch $\leq$ definierte Äquivalenzrelation ist \dots
  \item vervollständigen Sie den Unifikationsalgorithmus,
    vergleichen Sie mit
\url{http://dfa.imn.htwk-leipzig.de/cgi-bin/gitweb.cgi?p=ws11-cb.git;a=blob;f=kw56/Type/Constraint.hs;hb=master}
  \item wenden Sie den Algorithmus an zur Lösung von
\[
     f(X_1,f(X_2,f(X_3,a))) = f(f(X_2,X_2), f(f(X_3,X_3), f(a,a))) 
    \]
  \end{itemize}

\end{slide}
