Free proposition.
Clause.
CNF formula.
Abstract trait for expressions in CNF.
Abstract type for literals (atoms or atom negations).
Logical negation.
Translation from NNF to CNF with deMorgan's rules.
Translation from NNF to CNF with Tseitin's rules.
Creates a fresh uniquely identified atom.
Propositional logic in conjunctive normal form.