{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T02:32:38Z","timestamp":1760149958999,"version":"build-2065373602"},"reference-count":12,"publisher":"MDPI AG","issue":"10","license":[{"start":{"date-parts":[[2023,9,27]],"date-time":"2023-09-27T00:00:00Z","timestamp":1695772800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Algorithms"],"abstract":"<jats:p>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 \u201cdistributivity\u201d 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 \u201cassociativity\u201d 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.<\/jats:p>","DOI":"10.3390\/a16100459","type":"journal-article","created":{"date-parts":[[2023,9,27]],"date-time":"2023-09-27T07:38:46Z","timestamp":1695800326000},"page":"459","update-policy":"https:\/\/doi.org\/10.3390\/mdpi_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Mathematical Foundation of a Functional Implementation of the CNF Algorithm"],"prefix":"10.3390","volume":"16","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0382-0288","authenticated-orcid":false,"given":"Francisco Miguel","family":"Garc\u00eda-Olmedo","sequence":"first","affiliation":[{"name":"Departamento de \u00c1lgebra, Granada University, 18071 Granada, Spain"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2528-0566","authenticated-orcid":false,"given":"Jes\u00fas","family":"Garc\u00eda-Miranda","sequence":"additional","affiliation":[{"name":"Departamento de \u00c1lgebra, Granada University, 18071 Granada, Spain"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0567-3939","authenticated-orcid":false,"given":"Pedro","family":"Gonz\u00e1lez-Rodelas","sequence":"additional","affiliation":[{"name":"Departamento de Matem\u00e1tica Aplicada, Granada University, 18071 Granada, Spain"}]}],"member":"1968","published-online":{"date-parts":[[2023,9,27]]},"reference":[{"key":"ref_1","unstructured":"Bol\u00e7, L., Bundy, A., Siekmann, J., and Sloman, A. (1983). Automation of Reasoning. 2 Classical Papers on Computational Logic 1967\u20131970, Springer."},{"key":"ref_2","unstructured":"Hill, F.J., and Peterson, G.R. (1981). Introduction to Switching Theory and Logical Design, John Wiley & Sons."},{"key":"ref_3","doi-asserted-by":"crossref","unstructured":"Whitesitt, J.E. (1962). Boolean Algebra and Its Applications, Addison-Wesley Publishing Company.","DOI":"10.1063\/1.3058148"},{"key":"ref_4","unstructured":"Gorb\u00e1tov, V.A. (1988). Fundamentos de la Matem\u00e1tica Discreta, Mir."},{"key":"ref_5","unstructured":"B\u00fcning, H.K., and Lettmann, T. (1999). Propositional Logic: Deduction and Algorithms, Cambridge University Press."},{"key":"ref_6","unstructured":"Gill, A. (1976). Applied Algebra for the Computer Sciences, Prentice-Hall."},{"key":"ref_7","unstructured":"Hoos, H.H., and Mitchell, D.G. (2005). SAT 2004, LNCS 3542, Springer."},{"key":"ref_8","unstructured":"\u0141ukasiewicz, J. (1966). Elements of Mathematical Logic, Pergamon Press."},{"key":"ref_9","unstructured":"Lipova\u010da, M. (2011). Learn You a Haskell for Great Good, No Starch Press."},{"key":"ref_10","doi-asserted-by":"crossref","unstructured":"Monk, J.D. (1976). Mathematical Logic, Springer.","DOI":"10.1007\/978-1-4684-9452-5"},{"key":"ref_11","unstructured":"Bourbaki, N. (1977). Th\u00e9orie des Ensembles, El\u00e9ments de Math\u00e9matique; Hermann."},{"key":"ref_12","unstructured":"Kunen, K. (2009). The Foundations of Mathematics, College Publications. Mathematical Logic and Foundations."}],"container-title":["Algorithms"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/1999-4893\/16\/10\/459\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T20:59:39Z","timestamp":1760129979000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/1999-4893\/16\/10\/459"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,9,27]]},"references-count":12,"journal-issue":{"issue":"10","published-online":{"date-parts":[[2023,10]]}},"alternative-id":["a16100459"],"URL":"https:\/\/doi.org\/10.3390\/a16100459","relation":{},"ISSN":["1999-4893"],"issn-type":[{"type":"electronic","value":"1999-4893"}],"subject":[],"published":{"date-parts":[[2023,9,27]]}}}