Vereinfachen von Formeln

Satz: Falls M eine Teilformel T (also x = y oder x $ \neq$ y) enthält, die auf keinem Widerspruchskreis vorkommt,

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


Beweis: eine Richtung ist trivial, für die andere: konstruiere aus erfüllender Belegung von M' eine erfüllende Belegung von M.


Algorithmus: solange wie möglich



2009-06-22