
\begin{slide}{Vereinfachen von Formeln}

\emph{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/\text{True}]$
erfüllbarkeitsäquivalent zu $M$.

\bigskip 

\emph{Beweis}: eine Richtung ist trivial, 

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

\bigskip 

\emph{Algorithmus}: solange wie möglich
\begin{itemize}
\item eine solche Ersetzung ausführen
\item Formel vereinfachen (durch $(\text{True}\wedge x)=x$ usw.)
\end{itemize}

\end{slide}
