section ‹Propositional Formulas and CNFs› text ‹We provide a straight-forward definition of propositional formulas, defined as arbitray formulas using variables, negations, conjunctions and disjunctions. CNFs are represented as lists of lists of literals and then converted into formulas.› theory Propositional_Formula imports Main begin subsection ‹Propositional Formulas›