Mathematical Foundation of a Functional Implementation of the CNF Algorithm García Olmedo, Francisco Miguel García Miranda, Jesús González Rodelas, Pedro CNF SAT problem Classical logic Boolean algebra Horn clauses Reverse engineering Automatic theorems proving Algorithm implementation Functional programming Haskell The conjunctive normal form (CNF) algorithm is one of the best known and most widely used algorithms in classical logic and its applications. In its algebraic approach, it makes use in a loop of a certain well-defined operation related to the “distributivity” of logical disjunction versus conjunction. For those types of implementations, the loop iteration runs a comparison between formulas to decide when to stop. In this article, we explain how to pre-calculate the exact number of loop iterations, thus avoiding the work involved in the above-mentioned comparison. After that, it is possible to concatenate another loop focused now on the “associativity” of conjunction and disjunction. Also for that loop, we explain how to calculate the optimal number of rounds, so that the decisional comparison phase for stopping can be also avoided. 2023-11-13T13:40:41Z 2023-11-13T13:40:41Z 2023-09-27 journal article García-Olmedo, F.M.; García-Miranda, J.; González- Rodelas, P. Mathematical Foundation of a Functional Implementation of the CNF Algorithm. Algorithms 2023, 16, 459. [https://doi.org/10.3390/a16100459] https://hdl.handle.net/10481/85637 10.3390/a16100459 eng http://creativecommons.org/licenses/by/4.0/ open access Atribución 4.0 Internacional MDPI