Vereinfachen von Formeln

Satz: Falls M mathend000# eine Teilformel T mathend000# (also x = y mathend000# oder x≠y mathend000#) enthält, die auf keinem Widerspruchskreis vorkommt,

dann ist M' : = M[T/True] mathend000# erfüllbarkeitsäquivalent zu M mathend000#.

Beweis: eine Richtung ist trivial,

für die andere: konstruiere aus erfüllender Belegung von M' mathend000# eine erfüllende Belegung von M mathend000#.

Algorithmus: solange wie möglich

• eine solche Ersetzung ausführen
• Formel vereinfachen (durch (True∧x) = x mathend000# usw.)