\begin{slide}{EC/UF}

EC: Equality-Constraints
  \begin{itemize}\itemsep 0pt
  \item Definieren Sie die Syntax von EC
    (durch Angabe einer Signatur)
  \item Geben Sie je ein Beispiel für ein
    erfüllbares und ein nicht erfüllbares EC
    mit zwei Variablen an.
  \item Beweisen Sie: (*) für alle $C\in\text{EC}$ 
    mit $n$ Variablen gilt:

    $C$ besitzt Modell $\iff$ $C$ besitzt Modell
    mit Universum der Größe $\le n$.
  \end{itemize}
UF: EC mit uninterpretierten Funktionen
\begin{itemize}\itemsep 0pt
\item Geben Sie ein UF-Constraint an,
  für das (*) nicht gilt.
\item (Zusatz): gilt UF(*) mit einer anderen Schranke
  (als $\le n$)?
\end{itemize}

\end{slide}
