Plan

(für den Rest der Vorlesung)

• Prädikatenlogik (Syntax, Semantik)
• existentielle konjunktive Constraints

  in verschiedenen Bereichen, z. B.

  Gleichungen und Ungleichungen auf Zahlen ($\mathbb {Z}$,$\mathbb {Q}$,$\mathbb {R}$)

• beliebige Boolesche Verknüpfungen

  SAT modulo T (= SMT), DPLL(T)

• Bit-blasting (SMT → SAT)