Beweise für Nichterfüllbarkeit

• bisher: Interesse an erfüllender Belegung m∈Mod(F) mathend000# (= mathend000# Lösung einer Anwendungsaufgabe)

• jetzt: Interesse an Mod(F) = ∅ mathend000#.

  Anwendungen: Schaltkreis C mathend000# erfüllt Spezifikation S mathend000# $\iff$ mathend000# Mod(C(x)≠S(x)) = ∅ mathend000#.

Solver rechnet lange, evtl. Hardwarefehler usw.

• m∈Mod(F) mathend000# kann man leicht prüfen

  (unabhängig von der Herleitung)

• wie prüft man Mod(F) = ∅ mathend000#?

  (wie sieht ein Zertifikat dafür aus?)