Commit db0dd28e authored by Miriam's avatar Miriam

comment on tautologies

parent f19927c8
......@@ -249,7 +249,7 @@ $A^{glv} := \dneg A$
$\Rightarrow$ sufficient to show adequateness for one translation
Most important:
Prove a lot of double negation tautologies:
\item $\KIbox \oplus Z \vdash \dneg (\dneg A \land \dneg B) \leftrightarrow \dneg (A \land B)$
\item $\KIbox \oplus Z \vdash \dneg (\dneg A \lor \dneg B) \leftrightarrow \dneg (A \lor B)$
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment