\begin{slide}{Einführung}

  \begin{itemize}\itemsep 0pt
  \item Signatur: 
    \begin{itemize}
    \item Funktionssymbole beliebig
    \item Relationssymbol nur $=$
    \end{itemize}
  \item Universum: Terme 
    (d.h. Leibniz-Axiom für $=$)
  \item
    Formel: Konjunktion von Gleichungen
    (zwischen Termen mit Variablen)
  \end{itemize}

Anwendungen: Verarbeitung symbolischer Ausdrücke
\begin{itemize}\itemsep 0pt
\item logische Programmierung (Prolog)
\item Typprüfung, Typinferenz 
  (für polymorphe Funktionen)
\end{itemize}


\end{slide}
