Beweise für Nichterfüllbarkeit

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

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

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

Solver rechnet lange, evtl. Hardwarefehler usw.

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

  (unabhängig von der Herleitung)

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

  (wie sieht ein Zertifikat dafür aus?)