# Mathematical Foundation of a Functional Implementation of the CNF Algorithm
## 1 Introduction  
The conjunctive normal form (CNF) is famous in the history of thought because it organizes discourse by normalizing potentially chaotic statements through the conjunction of a series of statements in the form of disjunctions of other simple statements, namely atomic statements, or the negation of them. CNF has proven to be essential in the treatment of the SAT problem (from \"satisfiability\", usually abbreviated to SAT), which in turn is at the core of automated theorem proving, thanks to the effectiveness of the resolution rule and what is known about the treatment of Horn clauses (see [1]). The other great utility of CNF lies in the minimization of Boolean expressions under the condition of being expressed as a product of sums (POS) (see [2, 3]). It is clear that the POS criterion is the dual concept of the sum of products (SOP) criterion. In general, transforming a formula into CNF is the essence of [PERSON]'s method, an algorithm widely used in various fields: cybernetics, economics, linguistics, philosophy, psychology, etc. For an explanation of the algorithm and detailed applications, see [2] (p. 157), plus extensive comments and applications of the CNF algorithm. In [4] (pp. 69-71), we find a brilliant application of [PERSON]'s method to finite Boolean algebra. Given a propositional formula or a Boolean expression, it is possible to obtain for it an equivalent formula or expression, as the case may be, in CNF by semantic means or by algebraic manipulations. Both procedures are described in [5, 6, 7]; however, algebraic manipulation may be faster. If we focus on the method of syntactic analysis for obtaining CNF, we will consider propositional logic formulas, without loss of generality, in the appropriate language. In this line of thought, the essence of the algorithm is quite simple: after internalizing negation and eliminating double negation, the main task is to replace subformulas ofthe form \((\alpha\vee(\beta\wedge\gamma))\) by their equivalent \(((\alpha\vee\beta)\wedge(\alpha\vee\gamma))\) (distributivity). For the sake of efficiency, we will use Polish notation here as was introduced by [PERSON] in [8] (pp. 33-34). [PERSON] selected K (resp. A) to represent conjunction (resp. disjunction). Disjunction was originally called \"alternation\" by [PERSON] (in Polish \"alternaja\", hence the symbol \"A\"). The word \"disjunction\" in Polish is \"koniukcja\", hence the symbol \"K\". Our notation in this logical work, which is classical notation, is based on this [PERSON] guideline because it has the great advantage of avoiding parentheses and at the same time being univocal. Furthermore, Polish notation is ideal for transitioning to a functional implementation in the Haskell language given the peculiarities of its syntax (see [9]). Since de functor A stands for disjunction and functor K for conjunction in standard Polish notation, what we are saying is that the application of distributivity translates \(\text{A}\,\alpha\,\text{K}\,\beta\gamma\) to \(\text{K}\,\text{A}\,\alpha\beta\,\text{A}\,\alpha\gamma\). With regard to the CNF algorithm, the current state of the art can be found, for example, at [5; 6]. To fix ideas, we will focus on [5] (p. 26) and look at Algorithm 2.3, called TREE-EQ-CNF. Its pseudocode contains the following snippet:  
... { { { { { { { { { { { { { { \  
distributivity that, in a broad sense of the term, classical propositional logic contains between disjunction and conjunction. In that section, the function \(\mathrm{dak}\) is defined (see Figure 1), which, when applied to formulas, manages to reduce the alternation in them of the connector K over A in a unit; this alternation is measured in each formula by the function \(\mathrm{alt}\). The section concludes by showing that the alternation of each formula is precisely the minimum number of applications of \(\mathrm{dak}\) to it, in order to obtain another equivalent formula in conjunctive normal form.