We found a match
Your institution may have rights to this item. Sign in to continue.
- Title
Mathematical Foundation of a Functional Implementation of the CNF Algorithm.
- Authors
García-Olmedo, Francisco Miguel; García-Miranda, Jesús; González-Rodelas, Pedro
- Abstract
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.
- Subjects
ALGORITHMS; BOOLEAN algebra; LOGIC; REVERSE engineering
- Publication
Algorithms, 2023, Vol 16, Issue 10, p459
- ISSN
1999-4893
- Publication type
Article
- DOI
10.3390/a16100459