\begin{slide}{Kernaussagen}

  \begin{itemize}\itemsep 0pt
  \item Constraint-Programmierung $=$ 
    \begin{itemize}
    \item 
    anwendungsspezifische logische Formel,
  \item    
    generische bereichsspezifische 
    Such/Lösungsverfahren
    \end{itemize}
  \item
    CP ist eine Form der deklarativen Programmierung
  \item
    typische Anwendungsfälle für CP mit 
    Formeln ohne Quantoren, mit freien Variablen,
    Solver sagt:
    \begin{itemize}
    \item JA: beweist Existenz-Aussage,
      rekonstruiere Lösung der Anwendungsaufgabe 
      aus Modell
    \item NEIN: das beweist All-Aussage
      (z. B. Implementierung erfüllt Spezifikation
      für jede Eingabe)
    \end{itemize}
  \end{itemize}


\end{slide}
