I am looking at Conjunctive Normal Form examples, such as this:
${\displaystyle (A\lor \neg B\lor \neg C)\land (\neg D\lor E\lor F)}$
where it is a conjunction (AND) of disjunctions (ORs). So it's an AND of ORs. That's coming from looking at Demorgan's Laws, such as these:
${\displaystyle \neg (P\land Q)\vdash (\neg P\lor \neg Q).}$
${\displaystyle \neg (P\lor Q)\vdash (\neg P\land \neg Q).}$
That is coming from looking at minimally functionally complete operator sets, such as these:
One element
${↑}, {↓}$
Two elements
${\displaystyle \{\vee ,\neg \}} {\displaystyle \{\vee ,\neg \}}, {\displaystyle \{\wedge ,\neg \}} {\displaystyle \{\wedge ,\neg \}}, {\displaystyle \{\to ,\neg \}} {\displaystyle \{\to ,\neg \}}, {\displaystyle \{\gets ,\neg \}} {\displaystyle \{\gets ,\neg \}}, {\displaystyle \{\to ,\bot \}} {\displaystyle \{\to ,\bot \}}, {\displaystyle \{\gets ,\bot \}} {\displaystyle \{\gets ,\bot \}}, {\displaystyle \{\to ,\nleftrightarrow \}} {\displaystyle \{\to ,\nleftrightarrow \}}, {\displaystyle \{\gets ,\nleftrightarrow \}} {\displaystyle \{\gets ,\nleftrightarrow \}}, {\displaystyle \{\to ,\nrightarrow \}} {\displaystyle \{\to ,\nrightarrow \}}, {\displaystyle \{\to ,\nleftarrow \}} {\displaystyle \{\to ,\nleftarrow \}}, {\displaystyle \{\gets ,\nrightarrow \}} {\displaystyle \{\gets ,\nrightarrow \}}, {\displaystyle \{\gets ,\nleftarrow \}} {\displaystyle \{\gets ,\nleftarrow \}}, {\displaystyle \{\nrightarrow ,\neg \}} {\displaystyle \{\nrightarrow ,\neg \}}, {\displaystyle \{\nleftarrow ,\neg \}} {\displaystyle \{\nleftarrow ,\neg \}}, {\displaystyle \{\nrightarrow ,\top \}} {\displaystyle \{\nrightarrow ,\top \}}, {\displaystyle \{\nleftarrow ,\top \}} {\displaystyle \{\nleftarrow ,\top \}}, {\displaystyle \{\nrightarrow ,\leftrightarrow \}} {\displaystyle \{\nrightarrow ,\leftrightarrow \}}, {\displaystyle \{\nleftarrow ,\leftrightarrow \}} {\displaystyle \{\nleftarrow ,\leftrightarrow \}}$
Three elements
${\displaystyle \{\lor ,\leftrightarrow ,\bot \}} {\displaystyle \{\lor ,\leftrightarrow ,\bot \}}, {\displaystyle \{\lor ,\leftrightarrow ,\nleftrightarrow \}} {\displaystyle \{\lor ,\leftrightarrow ,\nleftrightarrow \}}, {\displaystyle \{\lor ,\nleftrightarrow ,\top \}} {\displaystyle \{\lor ,\nleftrightarrow ,\top \}}, {\displaystyle \{\land ,\leftrightarrow ,\bot \}} {\displaystyle \{\land ,\leftrightarrow ,\bot \}}, {\displaystyle \{\land ,\leftrightarrow ,\nleftrightarrow \}} {\displaystyle \{\land ,\leftrightarrow ,\nleftrightarrow \}}, {\displaystyle \{\land ,\nleftrightarrow ,\top \}} {\displaystyle \{\land ,\nleftrightarrow ,\top \}}$
This got me wondering why you always see the CNF in automated theorem proving, if it can be simplified from it's 3 symbols to 2 symbols such as AND + NOT, or even one symbols such as NAND. So in my attempt at the CNF example above, it would become:
${\displaystyle \neg(\neg A\land (B\land C))\land \dots}$
...something like that...
I'm wondering what the downsides are to simplifying CNF into using only 2 operation types such as AND + NOT or OR + NOT. Along those lines, wondering what advantage CNF gives you over just using the corresponding two operation form. If you simplified a complex programmatic expression down to AND + NOT, I'm wondering if there would be any advantage to then "complexifying" that 2-operation form into the CNF's 3-operation form.