\begin{slide}
\slidetitle{Negation Normal Forms}
\bit
\item Operational semantics of embedded implication is intuitionistic.
\item No negation normal forms available in intuitionistic logic.
\item Strong negation normal form (Nelson [1952]) incompatible with
  semantic of failure:
\beq
\neg (D\Imp G) & = & D\imp \neg G
\eneq
\item Valid for \textbf{complementable} programs.
\enit
\mends