Blake canonical form

Last updated

Karnaugh map of
html.skin-theme-clientpref-night .mw-parser-output div:not(.notheme)>.tmp-color,html.skin-theme-clientpref-night .mw-parser-output p>.tmp-color,html.skin-theme-clientpref-night .mw-parser-output table:not(.notheme) .tmp-color{color:inherit!important}@media(prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output div:not(.notheme)>.tmp-color,html.skin-theme-clientpref-os .mw-parser-output p>.tmp-color,html.skin-theme-clientpref-os .mw-parser-output table:not(.notheme) .tmp-color{color:inherit!important}}
AB +
BC +
AC, a sum of all prime implicants (each rendered in a different color). Deleting
AC results in a minimal sum. Karnaugh map KV 4mal4 Gruppe01a.svg
Karnaugh map of AB + BC + AC, a sum of all prime implicants (each rendered in a different color). Deleting AC results in a minimal sum.
Karnaugh map KV 4mal4 18.svg
ABD + ABC + ABD + ABC
Karnaugh map KV 4mal4 19.svg
ACD + BCD + ACD + BCD
Boolean function with two different minimal forms. The Blake canonical form is the sum of the two.

In Boolean logic, a formula for a Boolean function f is in Blake canonical form (BCF), [1] also called the complete sum of prime implicants, [2] the complete sum, [3] or the disjunctive prime form, [4] when it is a disjunction of all the prime implicants of f. [1]

Contents

Relation to other forms

The Blake canonical form is a special case of disjunctive normal form.

The Blake canonical form is not necessarily minimal (upper diagram), however all the terms of a minimal sum are contained in the Blake canonical form. [3] On the other hand, the Blake canonical form is a canonical form, that is, it is unique up to reordering, whereas there can be multiple minimal forms (lower diagram). Selecting a minimal sum from a Blake canonical form amounts in general to solving the set cover problem, [5] so is NP-hard. [6] [7]

History

Archie Blake presented his canonical form at a meeting of the American Mathematical Society in 1932, [8] and in his 1937 dissertation. He called it the "simplified canonical form"; [9] [10] [11] [12] it was named the "Blake canonical form" by Frank Markham Brown  [ d ] and Sergiu Rudeanu  [ d ] in 1986–1990. [13] [1] Together with Platon Poretsky's work [14] it is also referred to as "Blake–Poretsky laws". [15] [ clarification needed ]

Methods for calculation

Blake discussed three methods for calculating the canonical form: exhaustion of implicants, iterated consensus, and multiplication. The iterated consensus method was rediscovered [1] by Edward W. Samson and Burton E. Mills, [16] Willard Quine, [17] and Kurt Bing. [18] [19] In 2022, Milan Mossé, Harry Sha, and Li-Yang Tan discovered a near-optimal algorithm for computing the Blake canonical form of a formula in conjunctive normal form. [20]

See also

Related Research Articles

<span class="mw-page-title-main">Boolean algebra (structure)</span> Algebraic structure modeling logical operations

In abstract algebra, a Boolean algebra or Boolean lattice is a complemented distributive lattice. This type of algebraic structure captures essential properties of both set operations and logic operations. A Boolean algebra can be seen as a generalization of a power set algebra or a field of sets, or its elements can be viewed as generalized truth values. It is also a special case of a De Morgan algebra and a Kleene algebra.

A computer algebra system (CAS) or symbolic algebra system (SAS) is any mathematical software with the ability to manipulate mathematical expressions in a way similar to the traditional manual computations of mathematicians and scientists. The development of the computer algebra systems in the second half of the 20th century is part of the discipline of "computer algebra" or "symbolic computation", which has spurred work in algorithms over mathematical objects such as polynomials.

In boolean logic, a disjunctive normal form (DNF) is a canonical normal form of a logical formula consisting of a disjunction of conjunctions; it can also be described as an OR of ANDs, a sum of products, or — in philosophical logic — a cluster concept. As a normal form, it is useful in automated theorem proving.

<span class="mw-page-title-main">Quine–McCluskey algorithm</span> Algorithm for the minimization of Boolean functions

The Quine–McCluskey algorithm (QMC), also known as the method of prime implicants, is a method used for minimization of Boolean functions that was developed by Willard V. Quine in 1952 and extended by Edward J. McCluskey in 1956. As a general principle this approach had already been demonstrated by the logician Hugh McColl in 1878, was proved by Archie Blake in 1937, and was rediscovered by Edward W. Samson and Burton E. Mills in 1954 and by Raymond J. Nelson in 1955. Also in 1955, Paul W. Abrahams and John G. Nordahl as well as Albert A. Mullin and Wayne G. Kellner proposed a decimal variant of the method.

Laws of Form is a book by G. Spencer-Brown, published in 1969, that straddles the boundary between mathematics and philosophy. LoF describes three distinct logical systems:

<span class="mw-page-title-main">Boolean function</span> Function returning one of only two values

In mathematics, a Boolean function is a function whose arguments and result assume values from a two-element set. Alternative names are switching function, used especially in older computer science literature, and truth function, used in logic. Boolean functions are the subject of Boolean algebra and switching theory.

In Boolean algebra, any Boolean function can be expressed in the canonical disjunctive normal form (CDNF), minterm canonical form, or Sum of Products as a disjunction (OR) of minterms. The De Morgan dual is the canonical conjunctive normal form (CCNF), maxterm canonical form, or Product of Sums which is a conjunction (AND) of maxterms. These forms can be useful for the simplification of Boolean functions, which is of great importance in the optimization of Boolean formulas in general and digital circuits in particular.

In Boolean logic, the term implicant has either a generic or a particular meaning. In the generic use, it refers to the hypothesis of an implication. In the particular use, a product term P is an implicant of a Boolean function F, denoted , if P implies F . For instance, implicants of the function

<span class="mw-page-title-main">Platon Poretsky</span>

Platon Sergeevich Poretsky was a noted Russian Imperial astronomer, mathematician, and logician.

In Boolean algebra, Petrick's method is a technique described by Stanley R. Petrick (1931–2006) in 1956 for determining all minimum sum-of-products solutions from a prime implicant chart. Petrick's method is very tedious for large charts, but it is easy to implement on a computer. The method was improved by Insley B. Pyne and Edward Joseph McCluskey in 1962.

Logic is the formal science of using reason and is considered a branch of both philosophy and mathematics and to a lesser extent computer science. Logic investigates and classifies the structure of statements and arguments, both through the study of formal systems of inference and the study of arguments in natural language. The scope of logic can therefore be very large, ranging from core topics such as the study of fallacies and paradoxes, to specialized analyses of reasoning such as probability, correct reasoning, and arguments involving causality. One of the aims of logic is to identify the correct and incorrect inferences. Logicians study the criteria for the evaluation of arguments.

Logic optimization is a process of finding an equivalent representation of the specified logic circuit under one or more specified constraints. This process is a part of a logic synthesis applied in digital electronics and integrated circuit design.

In mathematical logic, algebraic logic is the reasoning obtained by manipulating equations with free variables.

<span class="mw-page-title-main">Consensus theorem</span> Theorem in Boolean algebra

In Boolean algebra, the consensus theorem or rule of consensus is the identity:

<span class="mw-page-title-main">Karnaugh map</span> Graphical method to simplify Boolean expressions

The Karnaugh map is a method of simplifying Boolean algebra expressions. Maurice Karnaugh introduced it in 1953 as a refinement of Edward W. Veitch's 1952 Veitch chart, which itself was a rediscovery of Allan Marquand's 1881 logical diagram aka Marquand diagram but now with a focus set on its utility for switching circuits. Veitch charts are also known as Marquand–Veitch diagrams, Svoboda charts -(albeit only rarely)- and even Karnaugh maps as Karnaugh–Veitch maps.

<span class="mw-page-title-main">Computer algebra</span> Scientific area at the interface between computer science and mathematics

In mathematics and computer science, computer algebra, also called symbolic computation or algebraic computation, is a scientific area that refers to the study and development of algorithms and software for manipulating mathematical expressions and other mathematical objects. Although computer algebra could be considered a subfield of scientific computing, they are generally considered as distinct fields because scientific computing is usually based on numerical computation with approximate floating point numbers, while symbolic computation emphasizes exact computation with expressions containing variables that have no given value and are manipulated as symbols.

In Boolean algebra, Poretsky's law of forms shows that the single Boolean equation is equivalent to if and only if , where represents exclusive or.

Charles Archibald Blake, name officially changed to Archie Blake was an American mathematician. He is well known for the Blake canonical form, a normal form for expressions in propositional logic. In order to compute the canonical form, he moreover introduced the concept of consensus, which was a precursor of the resolution principle, today a common technique in automated theorem proving.

In theoretical computer science, monotone dualization is a computational problem of constructing the dual of a monotone Boolean function. Equivalent problems can also be formulated as constructing the transversal hypergraph of a given hypergraph, of listing all minimal hitting sets of a family of sets, or of listing all minimal set covers of a family of sets. These problems can be solved in quasi-polynomial time in the combined size of its input and output, but whether they can be solved in polynomial time is an open problem.

References

  1. 1 2 3 4 Brown, Frank Markham [at Wikidata] (2012) [2003, 1990]. "Chapter 3: The Blake Canonical Form". Boolean Reasoning - The Logic of Boolean Equations (reissue of 2nd ed.). Mineola, New York: Dover Publications, Inc. pp. 4, 77ff, 81. ISBN   978-0-486-42785-0.
  2. Sasao, Tsutomu (1996). "Ternary Decision Diagrams and their Applications". In Sasao, Tsutomu; Fujita, Masahira (eds.). Representations of Discrete Functions. p. 278. doi:10.1007/978-1-4613-1385-4_12. ISBN   978-0792397205.
  3. 1 2 Kandel, Abraham (1998). Foundations of Digital Logic Design. World Scientific. p. 177. ISBN   978-9-81023110-1.
  4. Knuth, Donald Ervin (2011). Combinatorial Algorithms, Part 1. The Art of Computer Programming. Vol. 4A. p. 54.
  5. Feldman, Vitaly [at Wikidata] (2009). "Hardness of Approximate Two-Level Logic Minimization and PAC Learning with Membership Queries". Journal of Computer and System Sciences . 75: 13–25 [13–14]. doi: 10.1016/j.jcss.2008.07.007 .
  6. Gimpel, James F. (1965). "A Method for Producing a Boolean Function Having an Arbitrary Prescribed Prime Implicant Table". IEEE Transactions on Computers . 14: 485–488.
  7. Paul, Wolfgang Jakob [in German] (1974). "Boolesche Minimalpolynome und Überdeckungsprobleme". Acta Informatica (in German). 4 (4): 321–336. doi:10.1007/BF00289615. S2CID   35973949.
  8. Blake, Archie (November 1932). "Canonical expressions in Boolean algebra". Bulletin of the American Mathematical Society . Abstracts of Papers: 805.
  9. Blake, Archie (1937). Canonical expressions in Boolean algebra (Dissertation). Department of Mathematics, University of Chicago: University of Chicago Libraries.
  10. Blake, Archie (1938). "Canonical expressions in Boolean algebra". The Journal of Symbolic Logic . 3 (2).
  11. Blake, Archie (September 1938). "Corrections to Canonical Expressions in Boolean Algebra". The Journal of Symbolic Logic . 3 (3): 112–113. doi:10.2307/2267595. JSTOR   2267595. S2CID   5810863.
  12. McKinsey, John Charles Chenoweth, ed. (June 1938). "Blake, Archie. Canonical expressions in Boolean algebra, Department of Mathematics, University of Chicago, 1937". The Journal of Symbolic Logic (Review). 3 (2:93): 93. doi:10.2307/2267634. JSTOR   2267634. S2CID   122640691.
  13. Brown, Frank Markham [at Wikidata]; Rudeanu, Sergiu [at Wikidata] (1986), A Functional Approach to the Theory of Prime Implicants, Publication de l'institut mathématique, Nouvelle série, vol. 40, pp.  23–32
  14. Poretsky, Platon Sergeevich (1884). "O sposobach reschenija lopgischeskich rawenstw i ob obrathom spocobe matematischeskoi logiki" О способах решения логических равенств и об обратном способе[On methods of solving logical equalities and the inverse method of mathematical logic. An essay in construction of a complete and accessible theory of deduction on qualitative forms]. Collected Reports of Meetings of Physical and Mathematical Sciences Section of Naturalists' Society of Kazan University (in Russian) (2). (NB. This publication is also referred to as "On methods of solution of logical equalities and on inverse method of mathematical logic".)
  15. Vasyukevich, Vadim O. (2011). "1.10 Venjunctive Properties (Basic Formulae)". Written at Riga, Latvia. Asynchronous Operators of Sequential Logic: Venjunction & Sequention — Digital Circuits Analysis and Design. Lecture Notes in Electrical Engineering (LNEE). Vol. 101 (1 ed.). Berlin / Heidelberg, Germany: Springer-Verlag. p. 20. doi:10.1007/978-3-642-21611-4. ISBN   978-3-642-21610-7. ISSN   1876-1100. LCCN   2011929655. (xiii+1+123+7 pages) (NB. The back cover of this book erroneously states volume 4, whereas it actually is volume 101.)
  16. Samson, Edward Walter; Mills, Burton E. (April 1954). Circuit Minimization: Algebra and Algorithms for New Boolean Canonical Expressions (Technical Report). Bedford, Massachusetts, USA: Air Force Cambridge Research Center. AFCRC TR 54-21.
  17. Quine, Willard Van Orman (November 1955). "A Way to Simplify Truth Functions". The American Mathematical Monthly . 62 (9): 627–631. doi:10.2307/2307285. hdl:10338.dmlcz/142789. JSTOR   2307285.
  18. Bing, Kurt (1955). "On simplifying propositional formulas". Bulletin of the American Mathematical Society . 61: 560.
  19. Bing, Kurt (1956). "On simplifying truth-functional formulas". The Journal of Symbolic Logic . 21 (3): 253–254. doi:10.2307/2269097. JSTOR   2269097. S2CID   37877557.
  20. Mossé, Milan; Sha, Harry; Tan, Li-Yang (2022). "A Generalization of the Satisfiability Coding Lemma and Its Applications". DROPS-IDN/V2/Document/10.4230/LIPIcs.SAT.2022.9. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi: 10.4230/LIPIcs.SAT.2022.9 .