Plan

(für den Rest der Vorlesung)

• Prädikatenlogik (Syntax, Semantik)
• konjunktive Constraints in verschiedenen Bereichen

  z. B. Terme, Gleichungen und Ungleichungen

  auf Zahlen (ganze, rationale, reelle).

• beliebige Boolesche Verknüpfungen

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

• Bit-blasting (SMT → mathend000# SAT)