Theory and implementation of efficient canonical systems for sentential calculus, based on Prime Normal Forms

www.bucephalus.org

first version May 1999, revised version September 2002

Abstract

A literal conjunction γ = [∧λ_{1}...λ_{m}] is a prime factor of a Disjunctive Normal Form (DNF) Δ =[∨[∧λ_{11}...λ_{1m_{1}}]... [∧λ_{n1}...λ_{nm_{n}}]] iff γ ⇒ Δ and none of the λ_{1}, ..., λ_{m} could be deleted without violating γ ⇒ Δ. A DNF Δ = [∨γ_{1}...γ_{n}] is a prime DNF (PDNF) iff {γ_{1}, ..., γ_{n}} is the set of all its prime factors. Every sentential formula has exactly one equivalent PDNF so that this defines a canonic representation which is distinguished from other possible canonizations. PDNF’s can be constructed with the well–known Quine–McCluskey method, but that implementation is of exponential complexity and thus not practical in general. Therefore an efficient algorithm is designed in this paper. A dual system for prime conjunctive normal forms (PCNF’s) is presented as well. It is shown how the whole sentential calculus, all junctions and semantic decisions, is effectively handled by these two systems.

Contents

1 Introduction: Normal Forms 4 2 Basic concepts of sentential logic, DNF’s and CNF’s 6 3 * Implementation: The DNF and the CNF system 9 4 Special DNF’s and CNF’s 11 5 Covering and Subvalence 17 6 * Implementation of a fast subvalence decision with Prime Normal Forms 18 7 Component pairs 19 8 * Implementation: Minimal and Prime Normal Forms of component pairs 21 9 The M–Procedure 23 10 * Implementation of the M–Procedure 24 11 The completeness theorem and the P–Procedure 28 12 * Implementation of the P–Procedure 31 13 * Implementation: The PDNF and the PCNF system 33

1 Introduction: Normal Forms

Formal expressions, and logical expressions in particular, can be very different but still denote the same. For instance

• “5/2” and “2.5”

• “¬∀x(f(x) ≠ g(x))” and “∃x(f(x) = g(x))”

These examples are quite simple, but this ambiguity is a complex and important problem in general. Algebra, sometimes even the whole of mathematics is often said to be the reasoning about the equivalence of expressions. What is always desired in particular is a transformation of “difficult”, “incomprehensible” forms into “simple”, “compact”, and “understandable” or “standard” forms. In logic we talk about “normal forms”.

\underline{Definition} Let F be the set of all formulas (of a particular language) and N ⊆ F. If there is for every φ ∈ F a ν ∈ N such that φ ⇔ ν (i.e. φ and ν are equivalent), then N is called a set of normal forms. Every function nf : F ⟶ N with nf(φ) ⇔ φ for every φ ∈ F is called a (N–)normalizer (on F) and nf(φ) is a (N–)normalform of φ.

Most of the time there are several possibilities to define standard or normal forms. The context then determines which of the definitions is preferred. The decimal notation for numbers has a long tradition in daily life, but in computer science it is more practical to use the dual representation.

There is a series of criteria to describe and compare the qualities of normal forms:

• Intuitivity: How comprehensive and readable are the formulas?

• Canonicity: How much do syntactic and semantic similarities coincide? \underline{Definition}

A set N of normal forms is canonic, if for all ν_{1}, ν_{2} ∈ N: ν_{1} ⇔ ν_{2} iff ν_{1} = ν_{2}. Accordingly a normalizer nf : F ⟶ N is said to be canonic, if nf(φ_{1}) = nf(φ_{2}) for all φ_{1}, φ_{2} ∈ F with φ_{1} ⇔ φ_{2}.

If a definition of canonic normal forms is possible, the whole semantics of a language can be defined immediately as well: the normal form then is the meaning of an expression or a formula.

• Complexity of the representation: How big are the normal forms?

• Computational complexity: How high is the effort required for the normalizer and how do the normal forms behave in additional operations?

• Conservativity of the normalizer: If φ is a normal form already, is then nf(φ) = φ? This would contribute to the readability.

• Realizability as technical devices: Are the occuring junctors implementable? What is the behaviour of the divice in time? etc.

There is quite a number of possibilities to define normal forms in sentential logic. Most often the so–called “disjunctive” and the “conjunctive normal forms” (DNF’s and CNF’s) are used. Arguments for their superiority are:

• Their intuitivity:

• CNF’s are like a collection of elementary laws: Axiom systems, deductive systems are essentially CNF’s.

• DNF’s are like a collection of elementary possibil-

ities, similar to catalogues or inductive systems.

• As such they can often be modified by just adding or deleting components.

• Their similarity with arithmetics (Boole).

But DNF’s and CNF’s are not canonic already. Interestingly they are established as standards in sentential logic, but there are hardly any definitions of canonic DNF’s and CNF’s, not to mention any established standard.^{1} I suggest, the reason lies partly in the inner algebraic structure of sentential logic itself, which, at first sight, seems to refuse a canonization that would be superior in all quality criterias: The smallest DNF’s (or CNF’s) mostly look a little bit different to the, in some respect, most comprehensible^{2} DNF’s etc. Another reason might be, that potential standards are easily defined, but can be constructed only with considerable efforts.

The goal of this paper is first to show, that there is in fact only just one (reasonable) canonization of the DNF’s and CNF’s, a “natural canonic” so to say, that we will call “(ordered) prime disjunctive/conjunctive normal forms”. It doesn’t need new theorems and proofs to demonstrate that, one must only consequently ask the question for a canonic. The answer then is a proposal for a standardization of sentential logic. Really new, I think, is the method that constructs all the prime factors of any given formula. Different to the common method of Quine–McCluskey our algorithm is not of exponential, but of polynomial complexity^{3}, so that non–trivial applications can be mastered as well. In this way the proposed standardization of the propositional calculus is not only theoretically, but also practically well founded. The intention is to equally satisfy two kinds of readers: the specialist in Boolean algebras, who is investigating the possibility of “factorizing” the elements of these structures similar to the factorization in integer domains. Secondly the computer scientist who needs to build fast systems based on the sentential calculus and is looking for the quickest algorithms that can be implemented into sequential machines without further modification or refinement and altogether enable the full range of logical operations (i.e. junctions and semantic decisions). Because these two interests are quite conflicting, we separated the implementations from the algebraic core: the chapters that have “ * Implementation: ...” in their title can be seen as appendices and should be skipped.

1In fact there are the often so–called “canonic” DNF’s, that consist of all their maximal literal conjunctions. For instance, the “canonic DNF” of [A → B] would be [∨[∧\overline{A}\overline{B}][∧\overline{A}B][∧AB]]. The advantage of this form is that sentential logic turns into set theory in this way: conjunction, disjunction and negation of formulas become the intersection, union, and complementation of sets of maximal literal conjunctions. But these forms, except for simple cases, cannot be handled in practice because of the exponential demands of their representation. (Besides, strictly spoken these forms are not even canonic. For instance, [∨[∧]] and [∨[∧A][∧\overline{A}]] are both “canonic”, but they are equivalent and yet not equal.)

2see the chapter on subvalence and covering

3[Comment September 2002: At the time of the first publication I didn’t bother with complexity issues and I only mentioned them in footnotes. But obviously, it was a very naive thing to claim polynomial complexity without proving it. A paper about this neglected aspect is currently in progress.]

2 Basic concepts of sentential logic, DNF’s and CNF’s

\underline{Definition} From now on A shall be a fixed set of atoms. (For example the set of all non–empty strings made of letters and digits.) We assume that there is a linear order ≤_{A} defined on A. (For example, the lexical order). We also write for α_{1}, α_{2} ∈ A

α_{1} <_{A} α_{2} iff (α_{1} ≤_{A} α_{2} and α_{1} ≠ α_{2}) (Most of the time we will omit the subscript A and simply write ≤ and <.)

\underline{Definition} The set of all formulas (on A) is recursively defined as follows:^{4}

• Every α ∈ A is an (atomic) formula.

• 0 and 1 are formulas.

• ¬φ the negation of φ is a formula for every formula φ.

• If n ≥ 0 and φ_{1}, ..., φ_{n} are formulas, so are^{5} [∧φ_{1}...φ_{n}] the conjunction of φ_{1}, ..., φ_{n} [∨φ_{1}...φ_{n}] the disjunction of φ_{1}, ..., φ_{n} [\overline{∧}φ_{1}...φ_{n}] the nand-junction of φ_{1}, ..., φ_{n} [\overline{∨}φ_{1}...φ_{n}] the nor-junction of φ_{1}, ..., φ_{n}.

• For formulas φ_{1} and φ_{2} the following expressions are formulas: [φ_{1} → φ_{2}] the subjunction of φ_{1} and φ_{2} [φ_{1} ↔ φ_{2}] the equijunction of φ_{1} and φ_{2}

\underline{Definition} In formulas of the form [∗φ_{1}...φ_{n}] we call n the arity of length and the φ_{1}, ..., φ_{n} the components of the junction. At(φ) denotes the set of all atoms occuring in a formula φ. = denotes the syntactic identity of two formulas.

\underline{Examples} If φ = [[∧A¬B] → [A ↔ C]] then At(φ) = {A, B, C}. [∧AB] = [∧AB] but [∧AB] ≠ [∧BA]

\underline{Definition} Let ∗ ∈ \{∧, ∨, \overline{∧}, \overline{∨}\}, φ′ be a formula and φ = [∗φ_{1}...φ_{n}] and ψ = [∗ψ_{1}...ψ_{m}] be formulas. We write • φ′ ∈ φ, φ is an element or component of φ, iff

φ′ ∈ {φ_{1}, ..., φ_{n}}.

• φ′ ∉ φ, iff φ′ is not an element of φ.

• φ ⊆ ψ, φ is contained in ψ, iff {φ_{1}, ..., φ_{n}} ⊆ {ψ_{1}, ..., ψ_{m}}.

• φ ⊈ ψ iff φ is not contained in ψ.

• φ ⊂ ψ, φ is properly contained in ψ, iff φ ⊆ ψ and ψ ⊈ φ.

• φ ⊄ ψ iff φ is not properly contained in ψ.

\underline{Definition} The order ⇒ and the equivalence relation ⇔ on the set of formulas are defined as usual. We will only submit the notations and terminology. For any two formulas φ_{1} and φ_{2}

• φ_{1} ⇒ φ_{2} means φ_{1} is subvalent to φ_{2} or φ_{2} follows from φ_{1}. In that case we say that φ_{1} is an implicand of φ_{2} and that φ_{2} is a consequence of φ_{2}.

• φ_{1} ⇏ φ_{2} denotes that φ_{1} is not subvalent to φ_{2}.

• φ_{1} ⇔ φ_{2} means that φ_{1} and φ_{2} are equivalent.

• φ_{1} ⇎ φ_{2} denotes that φ_{1} and φ_{2} are not equivalent.

Furthermore we write

• φ_{1} ˙⇒φ_{2}, φ_{1} is properly subvalent to φ_{2}, iff φ_{1} ⇒ φ_{2} and φ_{1} ⇎ φ_{2}. As usual, we call a formula φ

• valid or a tautology, iff φ ⇔ 1

• satisfiable iff φ ⇎ 0

• a contradiction iff φ ⇔ 0

\underline{Definition}

• A literal is either an atom (positive literal) or a negated atom (negative literal).

• For a literal λ, its complement is defined as

\overline{λ} := \{ \begin{matrix}α & if λ = ¬α is a negative literal \\ ¬α & if λ = α is a positive literal \end{matrix}

• Two literals λ_{1} and λ_{2} are called complementary, iff λ_{1} = \overline{λ_{2}}.

• |λ| denotes the atom that occurs in a literal λ.

\underline{Definition}

• If λ_{1}, ..., λ_{n} are literals, n ≥ 0, we call [∧λ_{1}...λ_{n}] a literal conjunction, and [∨λ_{1}...λ_{n}] a literal disjunction.

• A literal conjunction [∧λ_{1}...λ_{n}] is called a normal literal conjunction or NLC iff |λ_{1}| < ... < |λ_{n}|.

• A literal disjunction [∨λ_{1}...λ_{n}] is called a normal

4We shall see later in our implementations that our system is very flexible in changing the set of junctors. For every new junctor we only need to add two lines in the algorithm dnf (and cnf).

5If there is a danger of confusion, blanks will be inserted between the components of these junctions, and we would for example write [∧ φ_{1} φ_{2} φ_{3}] instead of [∧φ_{1}φ_{2}φ_{3}]

literal disjunction or NLD iff |λ_{1}| < ... < |λ_{n}|.^{6}

\underline{Theorem}

• A literal conjunction is a contradiction if and only if it contains a pair of complementary literals.

• A literal disjunction is a tautology if and only if it contains a pair of complementary literals.

And since neither NLC’s nor NLC’s contain any pair of literals with the same element, we immediately get the following

\underline{Theorem} • 0 ˙⇒γ for each NLC γ.

• δ ˙⇒1 for each NLD δ.

\underline{Theorem}

• For any two NLC’s γ_{1} and γ_{2} • γ_{1} ⇒ γ_{2} iff γ_{2} ⊆ γ_{1}

• γ_{1} ˙⇒γ_{2} iff γ_{2} ⊂ γ_{1}

• γ_{1} ⇔ γ_{2} iff γ_{1} = γ_{2}

• For any two NLC’s δ_{1} and δ_{2} • δ_{1} ⇒ δ_{2} iff δ_{1} ⊆ δ_{2}

• δ_{1} ˙⇒δ_{2} iff δ_{1} ⊂ δ_{2}

• δ_{1} ⇔ δ_{2} iff δ_{1} = δ_{2}

There are infinitely many literal conjunctions equivalent to a given literal conjunction γ. But only one of them is normal. (The same holds for literal disjunctions.)

There are different possibilities to define a reasonable linear order on the set of NLC’s and NLD’s. We will need this order(s) only for the reason of completion (see the notes on “canonicity” further on), we don’t employ it in the main part of our work. We shall choose the usual lexical order (with the convention, that a positive is lexically smaller than the complementary negative literal). The reader may modify the choice as pleased.

\underline{Definition} With ∗ ∈ {∧, ∨} let [∗λ_{1}...λ_{n}] and [∗λ′_{1}...λ′_{m}] be either two NLC’s or NLD’s. We define

[∗λ_{1}...λ_{n}] ≤ [∗λ′_{1}...λ′_{m}]

iff n = 0
or |λ_{1}| < |λ′_{1}|
or ¬λ_{1} = λ′_{1}
or (λ_{1} = λ′_{1} and [∗λ_{2}...λ_{n}] ≤ [∗λ′_{2}...λ′_{m}]).

Otherwise, we also write [∗λ_{1}...λ_{n}] ≰ [∗λ′_{1}...λ′_{m}].

\underline{Definition}

• If γ_{1}, ..., γ_{n} are NLC’s with n ≥ 0, then [∨γ_{1}...γ_{n}] is called a disjunctive normal form or DNF.

• If δ_{1}, ..., δ_{n} are NLD’s with n ≥ 0, then [∧δ_{1}...δ_{n}] is called a conjunctive normal form or CNF.

\underline{Definition}

• A DNF [∨γ_{1}...γ_{n}] is said to be ordered iff γ_{1} ≤ ... ≤ γ_{n}.

• A CNF [∧δ_{1}...δ_{n}] is said to be ordered iff δ_{1} ≤ ... ≤ δ_{n}.

(If n = 0 or n = 1, the forms are ordered by definition.)

At first sight our definition of DNF’s (and CNF’s) might seem inconsequent, because

• either we follow the common convention and don’t demand any syntactic order at all: A “DNF” would then be a disjunction of literal conjunctions

• or we consequently approach canonicity and demand a full order inside the forms: A “DNF” would then be our ordered DNF.

The main reason for our definition is the fact that it allows us to implement the fastest algorithms. To demand that every literal conjunction must be normal is certainly no loss for the readability of the form and it immediately speeds up the processes. To demand that the NLC’s must be ordered in a sequence would on the other hand just slow down everything. For this reason we will soon even weaken the concept of canonicity for CNF’s and DNF’s a little bit.

\underline{Theorem}

• For every DNF Δ = [∨γ_{1}...γ_{n}] holds

Δ ⇔ 0 iff n = 0.

• For every CNF Γ = [∧δ_{1}...δ_{n}] holds

Γ ⇔ 1 iff n = 0.

\underline{Proof} Because 0 ˙⇒γ for every NLC γ and [∨φ_{1}...φ_{n}] ⇒ [∨φ_{1}...φ_{n}γ] for every n ≥ 0 and all formulas φ_{1}, ..., φ_{n}, there is 0 ˙⇒Δ for every DNF Δ = [∨γ_{1}...γ_{n}] with n > 0. The dual proof holds for CNF’s.

\underline{Theorem} Every formula φ has an (ordered) DNF as well as an (ordered) CNF.

6Instead of being one list of literals, NLC’s (and NLD’s) can be implemented as two lists of atoms, according to the transformation [∧\overline{A}BC\overline{D}\overline{E}F] ⇔ [∧[∧BCF][\overline{∨}ADE]]. Since the atom is the basic unit of sentential logic, one could dispense all junctors with this implementation. The whole system could be managed only by using the data structures atom and list. DNF’s (and CNF’s)

would then be lists of pairs of ordered atom lists. But in practice it is actually more common to take the literal and not the atom as the basis unit. We won’t discuss the arguments for doing so.

This is well known and doesn’t need a proof here. Instead we present two sets of algorithms (the “DNF system” and the “CNF system”) that include a normalizer each (namely “dnf” and “cnf”).

3 * Implementation: The DNF and the CNF system

The following DNF and CNF system are some kind of prototype for the final PDNF and PCNF system (see last chapter). Their central functions are the normalizers dnf and cnf. These are recursively implemented by making exhaustive use of de Morgans law and the junctor transformations into the ∧-∨-¬ system, so that only the disjunctions and conjunctions of DNF’s and CNF’s need to be specified furthermore. These could be done exclusively by using the distributive laws and the concatenation of conjunctions and disjunctions. But as we insist on the “normality” of literal conjunctions and disjunctions, the two functions nlc-and-nlc for the conjunction of two NLC’s and nld-or-nlc for the disjunction of two NLD’s must not be implemented as concatenations, but need a more complex treatment. This is done by the auxiliary algorithm jrec. jrec (the recursive implementation of these junctions) merges its first two parameters stepwise into its third argument, which is returned in the end. We make use of the duality principle and therefore we can use it both for nlc-and-nlc and nld-or-nld.

The DNF system: Declarations The CNF system: Declarations The Normalizer The Normalizer

dnf (φ) dnf (φ)

is a DNF of φ, for every formula φ. is a CNF of φ, for every formula φ. Conjunctions and Disjunctions Conjunctions and Disjunctions nlc-and-nlc (γ1, γ2) nld-or-nld (δ1, δ2) is a DNF of [∧γ1γ2], for every two NLC’s γ1 and γ2. is a CNF of [∨δ1δ2], for every two NLD’s δ1 and δ2. nlc-or-nlc (γ1, γ2) nld-and-nld (δ1, δ2) is a DNF for [∨γ1γ2], for every two NLC’s γ1 and γ2. is a CNF for [∧δ1δ2], for every two NLD’s δ1 and δ2. nlc-and-dnf (γ, Δ) nld-or-cnf (δ, Γ) is a DNF for [∧γΔ], for every NLC γ and DNF Δ. is a CNF for [∨δΓ], for every NLD δ and CNF Γ. nlc-or-dnf (γ, Δ) nld-and-cnf (δ, Γ) is a DNF for [∨γΔ], for every NLC γ and DNF Δ. is a CNF for [∧δΓ], for every NLD δ and CNF Γ. dnf-and-dnf (Δ1, Δ2) cnf-or-cnf (Γ1, Γ2) is a DNF for [∧Δ1Δ2], for every two DNF’s Δ1 and Δ2. is a CNF for [∨Γ1Γ2], for every two CNF’s Γ1 and Γ2. dnf-or-dnf (Δ1, Δ2) cnf-and-cnf (Γ1, Γ2) is a DNF for [∨Δ1Δ2], for every two DNF’s Δ1 and Δ2. is a CNF for [∧Γ1Γ2], for every two CNF’s Γ1 and Γ2. dnf-conj ((Δ1, ..., Δn)) cnf-disj ((Γ1, ..., Γn)) is a DNF for [∧Δ1...Δn], for every list (Δ1, ..., Δn) of DNF’s with n ≥ 0. is a CNF for [∨Γ1...Γn], for every list (Γ1, ..., Γn) of CNF’s with n ≥ 0. dnf-disj ((Δ1, ..., Δn)) cnf-conj ((Γ1, ..., Γn)) is a DNF for [∨Δ1...Δn], for every list (Δ1, ..., Δn) of DNF’s with n ≥ 0. is a CNF for [∧Γ1...Γn], for every list (Γ1, ..., Γn) of CNF’s with n ≥ 0. The DNF system: Implementation The CNF system: Implementation

dnf (φ)  cnf (φ)

:= \{ \begin{matrix}[∨[∧φ]] & if φ is an atom \\ [∨] & if φ = 0 \\ [∨[∧]] & if φ = 1 \\ [∨[∧¬α]] & if φ = ¬α and α is atom \\ [∨[∧]] & if φ = ¬0 \\ [∨] & if φ = ¬1 \\ dnf (φ′) & if φ = ¬¬φ′ \\ dnf-disj ((dnf (¬φ1), ..., dnf (¬φn))) & if φ = ¬[∧φ1...φn] \\ dnf-conj ((dnf (¬φ1), ..., dnf (¬φn))) & if φ = ¬[∨φ1...φn] \\ dnf-conj ((dnf (φ1), ..., dnf (φn))) & if φ = ¬[\overline{∧}φ1...φn] \\ dnf-disj ((dnf (φ1), ..., dnf (φn))) & if φ = ¬[\overline{∨}φ1...φn] \\ dnf-and-dnf (dnf (φ1), dnf (¬φ2)) & if φ = ¬[φ1 → φ2] \\ dnf-or-dnf ( \\ dnf-and-dnf (dnf (φ1), dnf (¬φ2)), \\ dnf-and-dnf (dnf (¬φ1), dnf (φ2))) & if φ = ¬[φ1 ↔ φ2] \\ dnf-conj (dnf (φ1), ..., dnf (φn)) & if φ = [∧φ1...φn] \\ dnf-disj (dnf (φ1), ..., dnf (φn)) & if φ = [∨φ1...φn] \\ dnf-disj (dnf (¬φ1), ..., dnf (¬φn)) & if φ = [\overline{∧}φ1...φn] \\ dnf-conj (dnf (¬φ1), ..., dnf (¬φn)) & if φ = [\overline{∨}φ1...φn] \\ dnf-or-dnf (dnf (¬φ1), dnf (φ2)) & if φ = [φ1 → φ2] \\ dnf-or-dnf ( \\ dnf-and-dnf (dnf (φ1), dnf (φ2)) \\ dnf-and-dnf (dnf (¬φ1), dnf (¬φ2))) & if φ = [φ1 ↔ φ2] \end{matrix} := \{ \begin{matrix}[∧[∨φ]] & if φ is an atom \\ [∧[∨]] & if φ = 0 \\ [∧] & if φ = 1 \\ [∧[∨¬α]] & if φ = ¬α and α is atom \\ [∧] & if φ = ¬0 \\ [∧[∨]] & if φ = ¬1 \\ cnf (φ′) & if φ = ¬¬φ′ \\ cnf-disj ((cnf (¬φ1), ..., cnf (¬φn))) & if φ = ¬[∧φ1...φn] \\ cnf-conj ((cnf (¬φ1), ..., cnf (¬φn))) & if φ = ¬[∨φ1...φn] \\ cnf-conj ((cnf (φ1), ..., cnf (φn))) & if φ = ¬[\overline{∧}φ1...φn] \\ cnf-disj ((cnf (φ1), ..., cnf (φn))) & if φ = ¬[\overline{∨}φ1...φn] \\ cnf-and-cnf (cnf (φ1), cnf (¬φ2)) & if φ = ¬[φ1 → φ2] \\ cnf-or-cnf ( \\ cnf-and-cnf (cnf (φ1), cnf (¬φ2)), \\ cnf-and-cnf (cnf (¬φ1), cnf (φ2))) & if φ = ¬[φ1 ↔ φ2] \\ cnf-conj (cnf (φ1), ..., cnf (φn)) & if φ = [∧φ1...φn] \\ cnf-disj (cnf (φ1), ..., cnf (φn)) & if φ = [∨φ1...φn] \\ cnf-disj (cnf (¬φ1), ..., cnf (¬φn)) & if φ = [\overline{∧}φ1...φn] \\ cnf-conj (cnf (¬φ1), ..., cnf (¬φn)) & if φ = [\overline{∨}φ1...φn] \\ cnf-or-cnf (cnf (¬φ1)cnf (φ2)) & if φ = [φ1 → φ2] \\ cnf-or-cnf ( \\ cnf-and-cnf (cnf (φ1), cnf (φ2)) \\ cnf-and-cnf (cnf (¬φ1), cnf (¬φ2))) & if φ = [φ1 ↔ φ2] \end{matrix}

nlc-and-nlc (γ1, γ2) nld-or-nld (δ1, δ2)

:= jrec (γ1, γ2, [∧])  := jrec (δ1, δ2, [∨])

nlc-or-nlc (γ1, γ2) nld-and-nld (δ1, δ2)

:= [∨γ1γ2]  := [∧δ1δ2]

nlc-and-dnf (γ, [∨γ1...γn]) nld-or-cnf (δ, [∧δ1...δn]) := dnf-disj ((nlc-and-nlc (γ, γ1), ..., nlc-and-nlc (γ, γn))) := cnf-conj ((nld-or-nld (δ, δ1), ..., nld-or-nld (δ, δn)))

nlc-or-dnf (γ, [∨γ1...γn]) nld-and-cnf (δ, [∧δ1...δn])

:= [∨γγ1...γn]  := [∧δδ1...δn]

dnf-and-dnf ([∨γ1...γn], Δ) cnf-or-cnf ([∧δ1...δn], Γ) := dnf-disj ((nlc-and-dnf (γ1, Δ), ..., nlc-and-dnf (γn, Δ))) := cnf-conj ((nld-or-cnf (δ1, Γ), ..., nld-or-cnf (δn, Γ)))

dnf-or-dnf ([∨γ1...γn], [∨γ′ 1...γ′ m]) cnf-and-cnf ([∧δ1...δn], [∧δ′1...δ′m])

:= [∨γ1...γnγ′ 1...γ′ m]  := [∧δ1...δnδ′1...δ′m]

dnf-conj ((Δ1, ..., Δn)) cnf-disj ((Γ1, ..., Γn))

:= \{ \begin{matrix}[∨[∧]] & if n = 0 \\ Δ1 & if n = 1 \\ dnf-and-dnf (Δ1, dnf-conj ((Δ2, ..., Δn))) & if n > 1 \end{matrix} := \{ \begin{matrix}[∧[∨]] & if n = 0 \\ Γ1 & if n = 1 \\ cnf-or-cnf (Γ1, cnf-disj ((Γ2, ..., Γn))) & if n > 1 \end{matrix}

dnf-disj ((Δ1, ..., Δn)) cnf-conj ((Γ1, ..., Γn))

:= \{ \begin{matrix}[∨] & if n = 0 \\ Δ1 & if n = 1 \\ dnf-or-dnf (Δ1, dnf-disj ((Δ2, ..., Δn))) & if n > 1 \end{matrix} := \{ \begin{matrix}[∧] & if n = 0 \\ Γ1 & if n = 1 \\ cnf-and-cnf (Γ1, cnf-conj ((Γ2, ...Γn))) & if n > 1 \end{matrix}

Auxiliary algorithms

\overline{∗} := \{ \begin{matrix}∨ & if ∗ = ∧ \\ ∧ & if ∗ = ∨ \end{matrix} \} for ∗ ∈ \{∧, ∨\}

jrec ([∗λ1...λn], [∗λ′1...λ′m], [∗μ1...μk])

:= \{ \begin{matrix}[\overline{∗}[∗μ1...μkλ′1...λ′m]] & if n = 0 \\ [\overline{∗}[∗μ1...μkλ1...λn]] & if m = 0 \\ jrec ([∗λ2...λn], [∗λ′1...λ′m], [∗μ1...μkλ1]) & if n > 0 and m > 0 and |λ1| < |λ′1| \\ jrec ([∗λ1...λn], [∗λ′2...λ′m], [∗μ1...μkλ′1]) & if n > 0 and m > 0 and |λ′1| < |λ1| \\ jrec ([∗λ2...λn], [∗λ′2...λ′m], [∗μ1...μkλ1]) & if n > 0 and m > 0 and λ1 = λ′1 \\ [\overline{∗}] & if n > 0 and m > 0 and \overline{λ1} = λ′1 \end{matrix}

4 Special DNF’s and CNF’s

Introduction

A major disadvantage of the DNF system^{7} is the often unnecessary length of the normal forms which impairs the readability and increases the costs for its representations and further operations. The following two examples are equivalent DNF’s:

• [∨[∧\overline{A}\overline{B}\overline{C}][∧A\overline{B}][∧B][∧C][∧C]]

• [∨[∧]]

But the second form will certainly be prefered in all practical means. In our search for a good canonic we will therefore start off with an attempt to find as “small” and “handy” forms as possible. But a remarkable and, on a first view may be even astonishing phenomenon of sentential logic is the fact, that here “small” and “handy” are quite close together, but nevertheless might mean significantly different forms in many cases. In this chapter we will formally conceptualize the desired criteria and we will find three differend special kinds of DNF’s:

• MDNF’s or minimal DNF’s,which are in fact the absolutely shortest DNF’s.

• M2DNF’s or pairwise minimal DNF’s, where each two components are a 2–ary MDNF [∨γ_{i}γ_{j}].

• PDNF’s or prime DNF’s, where the components are exactly the set of all “prime factors”.

As we said, these forms are quite often identical. But in fact they are different concepts and for the construction and comparison of DNF systems it is important to work out these differences and to analyse the properties of these forms.

\underline{\underline{Canonicity}}

First of all we are going to weaken the concept of canonicity, because we want to neglect the order of the components in the normal forms. It only obstructs the flow of our argumentation and unnecessarily increases the costs of the algorithms. Besides, normalizations that are not canonic in general, but still canonic in certain semantically distinguished cases, deserve an extra attention. For example a normalizer nf that is at least “1–canonic”, provides us with a subvalence and equivalence decision, because

φ_{1} ⇒ φ_{2} iff nf([φ_{1} → φ_{2}]) = nf(1).

These kind of normalizers might not define a whole semantic, but at least they enable the definitions of “tautology / contradiction” and “validity / satisfiability”.

\underline{Definition}

• Two DNF’s Δ_{1} = [∨γ_{1}...γ_{n}] and Δ_{2} = [∨γ′_{1}...γ′_{m}] are said to be identical up to the order of their components, or similar in short, written Δ_{1} ≈ Δ_{2}, iff there is a bijection i : {1, ..., n} ⟶ {1, ..., m} such that [∨γ_{i(1)}...γ_{i(n)}] = [∨γ′_{1}...γ′_{m}].

• Two CNF’s Γ_{1} = [∧δ_{1}...δ_{n}] and Γ_{2} = [∧δ′_{1}...δ′_{m}] are said to be identical up to the order of their components, or similar in short, written Γ_{1} ≈ Γ_{2}, iff there is a bijection i : {1, ..., n} ⟶ {1, ..., m} such that [∨δ_{i(1)}...δ_{i(n)}] = [∨δ′_{1}...δ′_{m}].

\underline{Definition} Let N be a set of DNF’s (CNF’s) that is itself a set of normal forms (i.e. for every formula there is an equivalent formula in N). We say that N is

• canonic, when for all ν_{1}, ν_{2} ∈ N ν_{1} ⇔ ν_{2} iff ν_{1} = ν_{2}

• pre-canonic, when for all ν_{1}, ν_{2} ∈ N ν_{1} ⇔ ν_{2} iff ν_{1} ≈ ν_{2}

• 0–canonic, when there is only one contradiction in N

• 1–canonic, when there is only one tautology in N.

Accordingly a N–normalizer nf is called

• canonic, if nf(φ_{1}) = nf(φ_{2}) for all formulas φ_{1} and φ_{2} with φ_{1} ⇔ φ_{2}

• pre-canonic, if nf(φ_{1}) ≈ nf(φ_{2}) for all formulas φ_{1} and φ_{2} with φ_{1} ⇔ φ_{2}

• 0–canonic, if nf(φ) = nf(0) for all contradictory formulas φ.

• 1–canonic, if nf(φ) = nf(1) for all contradictory formulas φ.

The following theorem immediately follows from this definition and it guarantees that a pre–canonic normalizer is actually as good as a canonic one.

\underline{Theorem} If nf is a pre–canonic normalizer and ord the function, that transforms an arbitrary formula into its ordered normal form, then ord ∘ nf is a canonic normalizer.^{8}

\underline{Theorem} DNF’s are

7The “principle of duality” guarantees that all true statements about DNF’s turn into true statements about CNF’s by inverting all occuring junctors. Therefore we will restrict ourselves mainly to DNF’s in the following explanations and proofs.

8ord ∘ nf(φ) := ord(nf(φ))

• neither canonic nor pre–canonic

• not 1–canonic

• 0–canonic CNF’s are

• neither canonic nor pre–canonic

• not 0–canonic

• 1–canonic

\underline{Proof}

• [∨[∧A]] and [∨[∧A\overline{B}][∧AB]] are equivalent DNF’s, but they are neither equal, nor similar.

• [∨[∧\overline{A}][∧A]] ⇔ [∨[∧]] ⇔ 1. Thus DNF’s are not 1–canonic.

• According to a theorem in chapter 2 it holds for each DNF Δ that Δ ⇔ 0 iff Δ = [∨]. Thus DNF’s are 0–canonic.

\underline{\underline{Factors}}

\underline{Definition}

• Let γ be a NLC and Δ = [∨γ_{1}...γ_{n}] a DNF. γ is called a (disjunctive) factor or implicand of Δ, iff γ ⇒ Δ. In other words, iff Δ ⇔ [∨γγ_{1}...γ_{n}]. In particular each component γ_{i} ∈ Δ is a factor of Δ.

• Let δ be a NLD and Γ = [∧δ_{1}...δ_{n}] a CNF. δ is called a (conjunctive) factor or consequence of Γ, iff Γ ⇒ δ. In other words, iff Γ ⇔ [∧δδ_{1}...δ_{n}]. In particular each component δ_{i} ∈ Γ is a factor of Γ.

\underline{Definition}

• A factor γ of a DNF Δ is prime, iff there is no factor γ′ of Δ with γ ˙⇒γ′. Thus “prime” means here not further reducible. No literal can be deleted in γ such that γ is still a factor of Δ.

• A factor δ of a CNF Γ is prime, iff there is no factor δ′ of Γ with δ′ ˙⇒δ. Again “prime” means here not further reducible. For each NLD δ′ the case δ′ ⊂ δ would imply that δ′ is not a factor of Γ.

\underline{Remark} • [∨] is the only DNF that has no factors.

• [∧] is the only CNF that has no factors.

• Every NLC γ is a factor of [∨[∧]].

• Every NLC δ is a factor of [∧[∨]].

Each DNF different to [∨] has infinitely many factors. (The same holds for CNF’s.) This is because the DNF would then at least have one component γ = [∧λ_{1}...λ_{n}]. Every NLC of the form γ′ = [∧λ_{1}...λ_{n}λ_{n+1}...λ_{n+m}] is a factor of Δ too, since γ′ ⇒ γ ⇒ Δ. But although the number of factors is (almost) always infinite, the number of prime factors is always finite, as follows directly from the following

\underline{Theorem}

• For each prime factor γ of a DNF Δ holds: At(γ) ⊆ At(Δ).

• For each prime factor δ of a CNF Γ holds: At(δ) ⊆ At(Γ).

\underline{Proof} Again we only proof the first half of the theorem. Let Γ = [∧[∨λ_{11}...λ_{1m_{1}}]...[∨λ_{n1}...λ_{nm_{n}}]] be a CNF equivalent to Δ and let γ = [∧λ_{1}...λ_{l}]. It holds that γ is a factor of Δ iff γ ⇒ Δ iff [∧γ¬Γ] ⇔ 0 iff [∧γ[∨[∧\overline{λ_{11}}...\overline{λ_{1m_{1}}}]...[∧\overline{λ_{n1}}...\overline{λ_{nm_{n}}}]]] ⇔ 0 iff [∨[∧λ_{1}...λ_{l}\overline{λ_{11}}...\overline{λ_{1m_{1}}}]...[∧λ_{1}...λ_{l}\overline{λ_{n1}}...\overline{λ_{nm_{n}}}]] ⇔ 0 iff [∧λ_{1}...λ_{l}\overline{λ_{i1}}...\overline{λ_{im_{i}}}] ⇔ 0 for each i = 1, ..., n iff {λ_{1}, ..., λ_{l}} ∩ {λ_{i1}, ..., λ_{im_{i}}} ≠ {} for each i = 1, ..., n. Suppose now At(γ) ⊈ At(Δ). So there must be a literal in γ — let it be λ_{1} — such that |λ_{1}| ∉ At(Δ). But in that case {λ_{1}, ..., λ_{l}} ∩ {λ_{i1}, ..., λ_{im_{i}}} = {λ_{2}, ..., λ_{l}} ∩ {λ_{i1}, ..., λ_{im_{i}}} for each i = 1, ..., n. And so [∧λ_{2}...λ_{l}] would be a factor of Δ, too. But then γ wouldn’t be a prime, and that would contradict the initial assumption.

\underline{Corollary} The number of prime factors of a given DNF or CNF is finite.

Prime Normal Forms

\underline{Definition} Suppose φ is a formula

• Let Δ be any arbitrary DNF of φ and {γ_{1}, ..., γ_{n}} the set of all prime factors of Δ. We call Δ′ := [∨γ_{1}...γ_{n}] a prime disjunctive normal form or PDNF (of φ or of Δ).

• Let Γ be any arbitrary CNF of φ and {δ_{1}, ..., δ_{n}} the set of all prime factors of Γ. We call Γ′ := [∧δ_{1}...δ_{n}] a prime conjunctive normal form or PCNF (of φ or of Γ).

Each formula φ has a DNF Δ. The set of all prime factor of Δ is always finite and so the PDNF Δ′ is always well defined (up to the order of its components). Δ′ is uniquely defined, no matter which DNF Δ of φ was chosen. Furthermore Δ′ ⇔ Δ, because:

• Each prime factor γ_{i} is a factor of Δ, thus γ_{i} ⇒ Δ and Δ′ ⇒ Δ.

• Every component γ ∈ Δ has a prime component

γ_{i} ∈ Δ′ such that γ ⇒ γ_{i}, and so Δ ⇒ Δ′.

This proofs the following

\underline{Theorem} For each formula φ there is

• one (up to the order of its components) uniquely defined PDNF Δ′ with Δ′ ⇔ φ, called the PDNF of φ.

• one (up te the order of its components) uniquely defined PCNF Γ′ with Γ′ ⇔ φ, called the PCNF of φ.

In other words: PDNF’s and PCNF’s are pre– canonic and the two according normalizers are well defined.

\underline{Corollary} For each PDNF Δ

• Δ ⇔ 0 iff Δ = [∨]

• Δ ⇔ 1 iff Δ = [∨[∧]] For each PCNF Γ

• Γ ⇔ 0 iff Γ = [∧[∨]]

• Γ ⇔ 1 iff Γ = [∧]

The next theorem about 0– and 1–ary DNF’s and CNF’s, together with one about 2–ary forms stated later on, will be the starting point for our algorithms that can handle all n–ary formulas.

\underline{Theorem} • [∨] is a PDNF.

• [∧] is a PCNF.

• Every DNF [∨γ] with one component is a PDNF.

• Every CNF [∧δ] with one component is a PCNF.

This won’t need an explicit proof.

Syntactic measures

We will new seek for a precise concept of syntactic “size” and propose two syntactic measures: length and volume.

\underline{Definition} For a DNF Δ = [∨[∧λ_{11}...λ_{1n_{1}}]...[∧λ_{m1}...λ_{mn_{m}}]] we put

• lg(Δ) := m the length of Δ

• vol(Δ) := n_{1} + n_{2} + ... + n_{m} the volume of Δ. For a CNF Γ = [∧[∨λ_{11}...λ_{1n_{1}}]...[∨λ_{m1}...λ_{mn_{m}}]] we put • lg(Γ) := m the length of Γ

• vol(Γ) := n_{1} + n_{2} + ... + n_{m} the volume of Γ.

For example, for Δ = [∨[∧ABC][∧\overline{A}\overline{B}\overline{C}]] there is lg(Δ) = 2 and vol(Δ) = 6.

Minimal Normal Forms

\underline{Definition} A DNF Δ is said to be

• of minimal length, if there is no DNF Δ′ such that Δ′ ⇔ Δ and lg(Δ′) < lg(Δ)

• of minimal volume, if there is no DNF Δ′ such that Δ′ ⇔ Δ and vol(Δ′) < vol(Δ)

• a minimal disjunctive normal form or MDNF, if Δ is of minimal length and minimal volume.

A CNF Γ is said to be

• of minimal length, if there is no CNF Γ′ such that Γ′ ⇔ Γ and lg(Γ′) < lg(Γ)

• of minimal volume, if there is no CNF Γ′ such that Γ′ ⇔ Γ and vol(Γ′) < vol(Γ)

• a minimal conjunctive normal form or MCNF, if Γ is of minimal length and minimal volume.

\underline{Remark}

• In general, minimal length does not imply minimal volume. If we take the following two DNF’s as an example

• Δ_{1} = [∨[∧A][∧\overline{A}B]]

• Δ_{2} = [∨[∧A][∧B]]

we can easily verify that they are equivalent and both of minimal length, but obviously 2 = vol(Δ_{2}) < vol(Δ_{1}) = 3.

• It remains an open question here if a minimal volume implies a minimal length.^{9}

If γ is a component of a DNF Δ, but not prime, then there must be a shorter factor γ′ of Δ. If Δ′ is obtained from Δ by replacing γ with γ′, then Δ′ ⇔ Δ and vol(Δ′) < vol(Δ). So, if a DNF is minimal, all its components must be prime factors.

\underline{Theorem}

• All components of a MDNF are prime factors: Let Δ_{m} be a MDNF and Δ_{p} a PDNF with Δ_{m} ⇔ Δ_{p}, then Δ_{m} ⊆ Δ_{p}.

• All components of a MCNF are prime factors:

9I conjecture that this is actually the case: Normal forms of minimal volume are always of minimal length. If this wouldn’t be correct, then there wouldn’t be a MDNF for every formula and thus MDNF’s wouldn’t make a proper set of normal forms. To avoid this, we could have identified minimality with minimality of the volume. But eventually, only the MDNF’s of 0–,1–, and 2–ary DNF’s are of interest in our paper. And restricted to these cases the normalizer is well defined and even pre-canonic, as we will see later on.

Let Γ_{m} be a MCNF and Γ_{p} a PCNF with Γ_{m} ⇔

Γ_{p}, then Γ_{m} ⊆ Γ_{p}.

For many formulas, the MDNF and PDNF are identic. [∨[∧A][∧B]] for instance is both a MDNF and a PDNF. But very often, they are differnt, as in the following example of two equivalent forms:

• [∨[∧AB][∧\overline{B}C]] is a MDNF

• [∨[∧AB][∧\overline{B}C][∧AC]] is the PDNF

The last theorem indicates a method how MDNF’s can be constructed: First, find all prime factors (later on we introduce an algorithm that solves this problem). Then find out which of the subsets of the PDNF still makes an equivalent formula and select the best of them. But, different to PDNF’s MDNF’s are not always unique:

\underline{Theorem}

• MDNF’s are not pre–canonic (thus not canonic), but 0– and 1–canonic.

• MCNF’s are not pre–canonic (thus not canonic), but 0– and 1–canonic.

\underline{Proof}

• Both of the following DNF’s are minimal • Δ_{1} = [∨[∧\overline{B}C][∧B\overline{C}][∧AB]]

• Δ_{2} = [∨[∧\overline{B}C][∧B\overline{C}][∧AC]]

and Δ_{1} ⇔ Δ_{2}, but obviously not Δ_{1} ≈ Δ_{2}. So, MDNF’s are not (pre–)canonic.

• DNF’s are 0–canonic according to a theorem in chapter 4 and as such MDNF’s are 0–canonic.

• All components of a MDNF Δ are prime factors. The only prime factor of a tautologic DNF is [∧]. So Δ ⇔ 1 iff Δ = [∨[∧]]. In other words, MDNF’s are 1–canonic.

\underline{Theorem} • [∨] is a MDNF.

• [∧] is a MCNF.

• Every DNF [∨γ] with one component is a MDNF.

• Every CNF [∧δ] with one component is a MCNF.

So, altogether we have “DNF = PDNF = MDNF”, if the length of the form doesn’t exceed 1.

Pairwise Minimal Normal Forms

In a later chapter we are going to proof that every 2–ary DNF Δ = [∨γ_{L}γ_{R}] has a (up to the order of the components) unique MDNF Δ′, that has at least one and at most two components. We will implement an algorithm to construct Δ′ and we write it as min(γ_{L}, γ_{R}) = Δ′.

By definition the length (thus either 1 or 2) and the volume of Γ′ are at most as big as the length (=2) and volume of Δ.

This algorithm min can be used for the following method to minimize pairwise, called the Minimizing Procedure or the M–Procedure:

(i) Choose any two components γ_{L} and γ_{R} of a given DNF Δ and replace them by components of min(γ_{L}, γ_{R}). (ii) Repeat step (i) until every pair of components of Δ is a MDNF. M-Procedure (Δ) shall denote the result.

An example: From a given DNF two components are selected (indexed by the two underbraces), their MDNF is computed and its components are inserted into the DNF again (indexed by the one or two overbraces).

[∨[∧\overline{A}\overline{B}\overline{C}][∧A\overline{B}][∧B] \underbrace{[∧C]} \underbrace{[∧C]}]

min([∧C], [∧C]) = [∨[∧C]]

[∨ \underbrace{[∧\overline{A}\overline{B}\overline{C}]} \underbrace{[∧A\overline{B}]}[∧B] \overbrace{[∧C]}]

min([∧\overline{A}\overline{B}\overline{C}], [∧A\overline{B}]) = [∨[∧\overline{B}\overline{C}][∧A\overline{B}]]

[∨ \overbrace{\underbrace{[∧\overline{B}\overline{C}]}} \overbrace{[∧A\overline{B}]} \underbrace{[∧B]}[∧C]]

min([∧\overline{B}\overline{C}], [∧B]) = [∨[∧\overline{C}][∧B]]

[∨ \overbrace{\underbrace{[∧\overline{C}]}}[∧A\overline{B}] \overbrace{[∧B]} \underbrace{[∧C]}]

min([∧\overline{C}], [∧C]) = [∨[∧]]

[∨ \overbrace{\underbrace{[∧]}} \underbrace{[∧A\overline{B}]}]

min([∧], [∧A\overline{B}]) = [∨[∧]]

[∨ \overbrace{\underbrace{[∧]}} \underbrace{[∧B]}]

min([∧], [∧B]) = [∨[∧]]

[∨ \overbrace{[∧]}]

Later on we implement an effective version of the M– Procedure, in which the vague instruction “choose any two components” in (i) and the test in (ii) are merged into a single step.

Obviously this whole method is monotone shortening, the DNF is constantly getting better in this respect. One might be tempted to suggest that the finite result is always a MDNF. It therefore might surprise that this is very often the case indeed, but not always. And neither is the result a PDNF in general. Therefore we give the forms that satisfy the terminating condition of the method, an own title:

\underline{Definition}

• A DNF Δ = [∨γ_{1}...γ_{n}] is called pairwise minimal or a M2DNF iff [∨γ_{i}γ_{j}] is minimal for all i, j ∈ {1, ..., n} with i ≠ j.

• A CNF Γ = [∧δ_{1}...δ_{n}] is called pairwise minimal or a M2CNF iff [∧δ_{i}δ_{j}] is minimal for all i, j ∈ {1, ..., n} with i ≠ j.

\underline{Theorem} • Every MDNF is a M2DNF.

• Not every M2DNF is a MDNF.

• Every PDNF is a M2DNF.

• Not every M2DNF is a PDNF

• Every MCNF is a M2CNF.

• Not every M2CNF is a MCNF.

• Every PCNF is a M2CNF.

• Not every M2CNF is a PCNF.

[figure: M2DNF; PDNF; MDNF]

\underline{Proof} • Obviously, every MDNF is a M2DNF.

• Δ = [∨[∧A\overline{B}][∧B\overline{C}][∧AC]] is an example for a M2DNF that isn’t a MDNF. The MDNF of Δ is Δ′ = [∨[∧A][∧B\overline{C}]].

• Suppose there is a PDNF Δ = [∨γ_{1}...γ_{n}] that isn’t a M2DNF. So there must be γ_{i}, γ_{j} ∈ Δ such that there is either a 1–ary DNF [∨γ′] ⇔ [∨γ_{i}γ_{j}] or a 2– ary DNF [∨γ′_{i}γ′_{j}] ⇔ [∨γ_{i}γ_{j}] with γ_{i} ˙⇒γ′_{i} or γ_{j} ˙⇒γ′_{j}. (We will show that in detail later on.). But that would contradict the premise that γ_{i} and γ_{j} both have to be prime factors of Δ.

• Again Δ = [∨[∧A\overline{B}][∧B\overline{C}][∧AC]] is an example for a M2DNF that isn’t a PDNF, which is again Δ′.

\underline{Theorem}

• M2DNF’s are 0–canonic, but not 1–canonic and thus not (pre–)canonic.

• M2CNF’s are 1–canonic, but not 0–canonic and thus not (pre–)canonic.

\underline{Proof} DNF’s are 0–canonic in general, so are M2DNF’s. Δ = [∨[∧]] and Δ′ = [∨ [∧\overline{B}\overline{C}\overline{D}] [∧AC\overline{D}] [∧\overline{A}\overline{B}C] [∧AB\overline{C}] [∧\overline{A}B\overline{D}] [∧BCD] [∧\overline{A}\overline{C}D] [∧A\overline{B}D]] are both tautologies and pairwise minimal, and so the M2DNF’s are not 1–canonic.

Quality comparison

Let us now compare the three special types of DNF’s according to the given criteria in the introduction.

• Intuitivity PDNF’s have the big advantage against the other two types that all factors can be read off directly from the form, and thus all subvalent formulas become directly identifiable, if they are given in DNF.^{10} In this respect, the PDNF’s are the most transparent of all DNF’s.

• Canonicity Of all three sets of DNF’s, only the PDNF’s are canonic.

• Complexity of the representation Actually all three types of normal forms are relatively condensed — this goal was our initial starting point. But the MDNF’s are the absolutely shortest by definition. PDNF’s and M2DNF’s both allow examples for which one type is shorter than the other.^{11}

• Computational complexity Later on we are going to introduce an algorithm of polynomial complexity to transform DNF’s into M2DNF’s. We will extend this idea to build a PDNF–normalizer. PDNF’s are very efficient for the test on subvalence (see next chapter). Usually MDNF’s are constructed out of PDNF’s and thus MDNF’s have the highest computational costs.

10see next chapter about “covering”

11We already saw that a MDNF is always a subset of the equivalent PDNF. I conjecture that the MDNF is always at least half as long as the PDNF. [Comment September 2002: Actually, this conjecture is not correct in general.]

• Conservativity The transformation of an arbitrary formula into a DNF usually changes the whole structure of the form. A further reduction into one of the three special DNF’s is, compare to that, very moderate.

• Realizability as technical devices I suppose, this is the real domain for the MDNF’s.

\underline{Conclusion} M2DNF’s are not very interesting for practical applications. Nevertheless they are indispensable for the theory and implementation of our PDNF system.

MDNF’s are only superior when the representational complexity is the only and most important aspect. There are established methods to construct MDNF’s out of given PDNF’s and I wouldn’t know how to improve them. Therefore we will neglect these forms in the sequel. PDNF’s are the only canonic forms. The rest of this paper is devoted to the construction of an effective PDNF system.

The analysis of the relation between two NLC’s stands at the center of our method and therefore this investigation is a chapter on its own. Subsequently we will first build a M2DNF and then a PDNF system. But first of all we demonstate the subvalence test with prime normal forms, that also provides us with a criterion to decide between a PDNF and a PCNF system in concrete applications.

5 Covering and Subvalence

Because the PDNF-normalizer is 1–canonic, it holds for any two formulas φ_{1} and φ_{2} that

φ_{1} ⇒ φ_{2} iff pdnf([φ_{1} → φ_{2}]) = [∨[∧]] In this way it is possible to implement the subvalence problem, i.e. the question, whether or not a formular implies another one. In actual applications it is very often the case that one side is relatively constant (and then it is often called “program”, “data bank”, “axiom system”, etc.), while the other side (called “input”, “request”, etc.) varies. We could name application systems of the sort φ_{constant} ⇒ φ_{variable} “consequence systems” and the others of the sort φ_{variable} ⇒ φ_{constant} “implicand systems”.

For these two kind of systems there is a much more efficient method for the subvalence problem than the one just mentioned:

• For consequence systems we construct the PCNF Γ_{constant} of φ_{constant} and a CNF Γ_{variable} of φ_{variable} and we decide the truth of Γ_{constant} ⇒ Γ_{variable} by using the following covering concept.

• Accordingly the application of DNF’s suits very well for imlicand systems.

The “covering method” reduces the subvalence problem to the pairwise comparison of NLC’s (NLD’s) and that doesn’t only accelerate the computer, it also supports the comprehension and mental arithmetic of formulas. The semantic of prime normal forms is exceptionally intuitive.

We noticed earlier that:

• For any two NLC’s γ_{1} and γ_{2}: γ_{1} ⇒ γ_{2} iff γ_{2} ⊆ γ_{1}.

• For any two NLD’s δ_{1} and δ_{2}: δ_{1} ⇒ δ_{2} iff δ_{1} ⊆ δ_{2}.

\underline{Definition} For each NLC γ and DNF’s Δ = [∨γ_{1}...γ_{n}] and Δ′ we define:

• γ ⊑ Δ, γ is covered by Δ, iff there is a γ_{i} ∈ Δ such that γ ⇒ γ_{i}.

• γ ⋢ Δ iff γ is not covered by Δ.

• Δ ⊑ Δ′, Δ is covered by Δ′, iff γ_{i} ⊑ Δ′ for every γ_{i} ∈ Δ.

• Δ ⋢ Δ′ iff Δ is not covered by Δ′.

For each NLD δ and CNF’s Γ = [∧δ_{1}...δ_{n}] and Γ′ we define:

• δ ⊑ Γ, δ is covered by Γ, iff there is a δ_{i} ∈ Γ such that δ_{i} ⇒ δ.

• δ ⋢ Γ iff δ is not covered by Γ.

• Γ ⊑ Γ′, Γ is covered by Γ′, iff δ_{i} ⊑ Γ′ for every δ_{i} ∈ Γ.

• Γ ⋢ Γ′ iff Γ is not covered by Γ′.

For DNF’s Δ ⊑ Δ′ always implies Δ ⇒ Δ′. But the reverse is generally only the case if Δ′ is prime^{12}.

\underline{Theorem}

• Let Δ be a DNF and Δ_{p} a PDNF. Then Δ ⇒ Δ_{p} iff Δ ⊑ Δ_{p}.

• Let Γ_{p} be a PCNF and Γ a CNF. Then Γ_{p} ⇒ Γ iff Γ ⊑ Γ_{p}.

\underline{Proof} For Δ = [∨γ_{1}...γ_{n}] there is Δ ⇒ Δ′ iff [[∨γ_{1}...γ_{n}] → Δ′] ⇔ 1 iff [∨[∧¬γ_{1}...¬γ_{n}]Δ′] ⇔ 1 iff [∧[∨¬γ_{1}Δ′]...[∨¬γ_{n}Δ′]] ⇔ 1 iff [∧[γ_{1} → Δ′]...[γ_{n} → Δ′]] ⇔ 1 iff γ_{i} ⇒ Δ′ for each i = 1, ..., n. Thus every γ_{i} ∈ Δ has to be a factor of Δ′. Since Δ′ contains all prime factors, there must be a γ′_{j} ∈ Δ′ for each γ_{i} ∈ Δ such that γ_{i} ⇒ γ′_{j}. Thus γ_{i} ⊑ Δ′ for each i = 1, ..., n and thus Δ ⊑ Δ′.

\underline{Theorem} ⊑ is a quasi-order^{13} on the set of all DNF’s (CNF’s).

12More general, if Δ′ is “f–complete” (see below).

13reflexive and transitive

6 * Implementation of a fast subvalence decision with Prime Normal Forms

The following table of algorithms gives an example of how these results can be implemented. It can later be attached to the fully developed PDNF and PCNF system.

The PDNF system: Declarations The PCNF system: Declarations For NLC’s γ1 and γ2 For NLD’s δ1 and δ2 nlc–sub–nlc(γ1, γ2) = \{ \begin{matrix}0 & if γ1 ⇏ γ2 \\ 1 & if γ1 ⇒ γ2 \end{matrix} nld–sub–nld(δ1, δ2) = \{ \begin{matrix}0 & if δ1 ⇏ δ2 \\ 1 & if δ1 ⇒ δ2 \end{matrix} For a NLC γ and a DNF Δ For a NLD δ and a CNF Γ nlc–cov–dnf(γ, Δ) = \{ \begin{matrix}0 & if γ ⋢ Δ \\ 1 & if γ ⊑ Δ \end{matrix} nld–cov–cnf(δ, Γ) = \{ \begin{matrix}0 & if δ ⋢ Γ \\ 1 & if δ ⊑ Γ \end{matrix} For DNF’s Δ1 and Δ2 For CNF’s Γ1 and Γ2 dnf–cov–dnf(Δ1, Δ2) = \{ \begin{matrix}0 & if Δ1 ⋢ Δ2 \\ 1 & if Δ1 ⊑ Δ2 \end{matrix} cnf–cov–cnf(Γ1, Γ2) = \{ \begin{matrix}0 & if Γ1 ⋢ Γ2 \\ 1 & if Γ1 ⊑ Γ2 \end{matrix} For a DNF Δ1 and a PDNF Δ2 For a PCNF Γ1 and a CNF Γ2 dnf–sub–pdnf(Δ1, Δ2) = \{ \begin{matrix}0 & if Δ1 ⇏ Δ2 \\ 1 & if Δ1 ⇒ Δ2 \end{matrix} pcnf–sub–cnf(Γ1, Γ2) = \{ \begin{matrix}0 & if Γ1 ⇏ Γ2 \\ 1 & if Γ1 ⇒ Γ2 \end{matrix} The PDNF system: Implementations The PCNF system: Implementations nlc–sub–nlc([∧λ1...λn], [∧λ′1...λ′m]) nld–sub–nld([∨λ1...λn], [∨λ′1...λ′m])

:= \{ \begin{matrix}1 & if m = 0 \\ 0 & if m > 0 and n = 0 \\ nlc–sub–nlc([∧λ2...λn], [∧λ′1...λ′m]) & if | λ1 |<| λ′1 | \\ 0 & if | λ′1 |<| λ1 | \\ nlc–sub–nlc([∧λ2...λn], [∧λ′2...λm]) & if λ1 = λ′1 \\ 0 & if \overline{λ1} = λ′1 \end{matrix} := \{ \begin{matrix}1 & if n = 0 \\ 0 & if n > 0 and m = 0 \\ 0 & if | λ1 |<| λ′1 | \\ nld–sub–nld([∨λ1...λn], [∨λ′2...λ′m]) & if | λ′1 |<| λ1 | \\ nld–sub–nld([∨λ2...λn], [∨λ′2...λm]) & if λ1 = λ′1 \\ 0 & if \overline{λ1} = λ′1 \end{matrix}

nlc–cov–dnf(γ, [∨γ1...γn]) nld–cov–cnf(δ, [∧δ1...δn])

:= \{ \begin{matrix}0 & if n = 0 \\ 1 & if nlc–sub–nlc(γ, γ1) = 1 \\ nlc–cov–dnf(γ, [∨γ2...γn]) & if nlc–sub–nlc(γ, γ1) = 0 \end{matrix} := \{ \begin{matrix}0 & if n = 0 \\ 1 & if nld–sub–nld(δ1, δ) = 1 \\ nld–cov–cnf(δ, [∧δ2...δn]) & if nld–sub–nld(δ1, δ) = 0 \end{matrix}

dnf–cov–dnf([∨γ1...γn], Δ) cnf–cov–cnf([∧δ1...δn], Γ)

:= \{ \begin{matrix}1 & if n = 0 \\ 0 & if nlc–cov–dnf(γ1, Δ) = 0 \\ dnf–cov–dnf([∨γ2...γn], Δ) & if nlc–cov–dnf(γ1, Δ) = 1 \end{matrix} := \{ \begin{matrix}1 & if n = 0 \\ 0 & if nld–cov–cnf(δ1, Γ) = 0 \\ cnf–cov–cnf([∧δ2...δn], Γ) & if nld–cov–cnf(δ1, Γ) = 1 \end{matrix}

dnf–sub–pdnf(Δ1, Δ2) pcnf–sub–cnf(Γ1, Γ2) := dnf–cov–dnf(Δ1, Δ2) := cnf–cov–cnf(Γ1, Γ2)

7 Component pairs

In this chapter we will construct an algorithm that determines the MDNF and the PDNF of a 2-ary DNF [∨γ_{L}γ_{R}].^{14} Both do exist and they are unique (up to the order of their components.)

First we introduce a special notation for a literal conjunction that might not be normal yet, but doesn’t contain doubles or complementary literals, and thus can easily be normalized by changing the order of the components:

\underline{Notation} Let [∧λ_{1}...λ_{n}] be a literal conjunction and i : {1, ..., n} ⟶ {1, ..., n} a bijection such that [∧λ_{i(1)}...λ_{i(n)}] is a NLC. (Note that this bijection is unique if it exists.) We then write

[ ˙∧λ_{1}...λ_{n}] := [∧λ_{i(1)}...λ_{i(n)}]

\underline{Definition} Let

• γ_{L} = [∧λ_{1}...λ_{x}] be a NLC

• γ_{R} = [∧λ′_{1}...λ′_{y}] be a NLC We define the following sets (the order of the elements is of no interest here):

• {π_{1}, ..., π_{p}} := {λ_{1}, ..., λ_{x}} ∩ {λ′_{1}, ..., λ′_{y}}

• \{ρ_{1}, ..., ρ_{r}\} := \{λ_{1}, ..., λ_{x}\} ∩ \{\overline{λ′_{1}}, ..., \overline{λ′_{y}}\}

• \{σ_{1}, ..., σ_{s}\} := \{λ_{1}, ..., λ_{x}\} − \{λ′_{1}, ..., λ′_{y}, \overline{λ′_{1}}, ..., \overline{λ′_{y}}\}

• \{τ_{1}, ..., τ_{t}\} := \{λ′_{1}, ..., λ′_{y}\} − \{λ_{1}, ..., λ_{x}, \overline{λ_{1}}, ..., \overline{λ_{x}}\} Thus

• γ_{L} = [ ˙∧π_{1}...π_{p}ρ_{1}...ρ_{r}σ_{1}...σ_{s}]

• γ_{R} = [ ˙∧π_{1}...π_{p}\overline{ρ_{1}}...\overline{ρ_{r}}τ_{1}...τ_{t}] We define

• min(γ_{L}, γ_{R})

• prim(γ_{L}, γ_{R}) according to the following table, depending on the values of p, r, s, and t. In this table we use the abbreviations^{15}

• “N” for any Number, i.e. ≥ 0

• “P” for Positive, i.e. ≥ 1

• “M” for Multiple, i.e. > 1

Without its long and non–informative proof we state the following

\underline{Theorem}

• min(γ_{L}, γ_{R}) is the (up to the order of its components) uniquely defined MDNF of [∨γ_{L}γ_{R}].

• prim(γ_{L}, γ_{R}) is the (up to the order of its components) uniquely defined PDNF of [∨γ_{L}γ_{R}].

\underline{Example} γ_{L} := [∧ABD\overline{E}\overline{G}\overline{K}] γ_{R} := [∧A\overline{B}CE\overline{H}IJ\overline{K}L] For these two NLC’s we have \{π_{1}, ..., π_{p}\} = \{A, \overline{K}\} thus p = 2 \{ρ_{1}, ..., ρ_{r}\} = \{B, \overline{E}\} thus r = 2 \{σ_{1}, ..., σ_{s}\} = \{D, \overline{G}\} thus s = 2 \{τ_{1}, ..., τ_{t}\} = \{C, \overline{H}, I, J, L\} thus t = 5 This is the case “NMNN”in the table and so min(γ_{L}, γ_{R}) = prim(γ_{L}, γ_{R}) = [∨γ_{L}γ_{R}].

We can see in the table that the number p of literals that occur both in γ_{L} and in γ_{R}, doesn’t have any influence on the MDNF and PDNF solution, while the number r of literals that occur in γ_{L} and complemented in γ_{R} is very decisive. Therefore we call [∨γ_{L}γ_{R}] or the relation between γ_{L} and γ_{R}

• incomplementary, if r = 0

• complementary, if r = 1

• hyper–complementary if r > 1.

Furthermore we call [∨γ_{L}γ_{R}] (or γ_{L} and γ_{R}) minimal, iff min(γ_{L}, γ_{R}) = [∨γ_{L}γ_{R}]. As the table shows, this is exactly the case when r > 1 or (s > 0 and t > 0). In case γ_{L} and γ_{R} are complementary and minimal — and only in this case — the PDNF and the MDNF of [∨γ_{L}, γ_{R}] are different: the PDNF contains one additional prime factor. We call it the complementary prime factor or shorter the c–prime factor of γ_{L} and γ_{R} (or [∨γ_{L}γ_{R}]).

14The subscripts “L” and “R” stand for “left” and “right”.

15We introduce these symbols, because in later algorithms we will make use the case symbols “N000”, “N00P”, ..., “NMNN”as identification symbols for the nine different cases.

p  r  s  t  γL  γR  min (γL, γR)  prim (γL, γR)

N  0  0  0  [ ˙∧π1...πp]  [ ˙∧π1...πp]  [∨γL] = [∨γR]  [∨γL] = [∨γR]

N  0  0  P  [ ˙∧π1...πp]  [ ˙∧π1...πpτ1...τt]  [∨γL]  [∨γL]

N  0  P  0  [ ˙∧π1...πpσ1...σs]  [ ˙∧π1...πp]  [∨γR]  [∨γR]

N  0  P  P  [ ˙∧π1...πpσ1...σs]  [ ˙∧π1...πpτ1...τt]  [∨γLγR]  [∨γLγR]

N  1  0  0  [ ˙∧π1...πpρ1]  [ ˙∧π1...πp\overline{ρ1}]  [∨γ′] with  [∨γ′] with
γ′ := [ ˙∧π1...πp]  γ′ := [ ˙∧π1...πp]

N  1  0  P  [ ˙∧π1...πpρ1]  [ ˙∧π1...πp\overline{ρ1}τ1...τt]  [∨γLγ′ R] with  [∨γLγ′ R] with
γ′ R := [ ˙∧π1...πpτ1...τt]  γ′ R := [ ˙∧π1...πpτ1...τt]

N  1  P  0  [ ˙∧π1...πpρ1σ1...σs]  [ ˙∧π1...πp\overline{ρ1}]  [∨γ′ LγR] with  [∨γ′ LγR] with
γ′ L := [ ˙∧π1...πpσ1...σs]  γ′ L := [ ˙∧π1...πpσ1...σs]

N  1  P  P  [ ˙∧π1...πpρ1σ1...σs]  [ ˙∧π1...πp\overline{ρ1}τ1...τt]  [∨γLγR]  [∨γLγRγc] with

γc := [ ˙∧π1...πpσ1...σsτ1...τt] the c–prime factor

N  M  N  N  [ ˙∧π1...πpρ1...ρr σ1...σs]  [ ˙∧π1...πp\overline{ρ1}...\overline{ρr} τ1...τt]  [∨γLγR]  [∨γLγR]

8 * Implementation: Minimal and Prime Normal Forms of component pairs

The implementation of the two functions min(γ_{L}, γ_{R}) and prim(γ_{L}, γ_{R}) could be straightforward: first, determine the four sets {π_{1}, ..., π_{p}}, {ρ_{1}, ..., ρ_{r}}, {σ_{1}, ..., σ_{s}}, and {τ_{1}, ..., τ_{t}}. Then, look up the case and the according instruction in the table and finally construct the formula. But we are eager to create a fast system. min is the core of the M2DNF system, prim will be the most often applied function in the PDNF system.

In fact, the algorithms will not use min and prim, but the “extended” versions xmin and xprim, where xmin(γ_{L}, γ_{R}) := (ξ, min(γ_{L}, γ_{R})) and xprim(γ_{L}, γ_{R}) := (ξ, prim(γ_{L}, γ_{R})) and ξ is the case symbol, i.e. the abbreviations for the numbers of p,r,s, and t in the table.

\underline{Example} For γ_{L} = [∧A\overline{B}DF] and γ_{R} = [∧BC] there are

• xmin (γ_{L}, γ_{R}) = (“N1PP”, [∨[∧A\overline{B}DF][∧BC]])

• xprim (γ_{L}, γ_{R}) = (“N1PP”, [∨ [∧A\overline{B}DF] [∧BC]

[∧ACDF]])

For the implementation of xprim we use the auxiliary recursive function xprec. xprec terminates as soon as the case is clear, and that is mainly what makes it faster than the straightforward version. xprec is not the only version that would do the job, we don’t need to discuss it and the reader is free to use an own version. The duality allows us to formulate xprec for DNF’s and CNF’s together and we use ∗ as the junctor symbol and \overline{∗} for the dual junctor.

Disjunctive component pairs: Declarations Conjunctive component pairs: Declarations

prim(γL, γR) prim(δL, δR)

is the PDNF of [∨γLγR], for any two NLC’s γL and γR is the PCNF of [∧δLδR], for any two NLD’s δL and δR

min(γL, γR) min(δL, δR)

is the MDNF of [∨γLγR], for any two NLC’s γL and γR is the MCNF of [∧δLδR], for any two NLD’s δL and δR

xprim(γL, γR) xprim(δL, δR)

:= (ξ, prim(γL, γR)) where ξ is the case symbol according to the table in chapter 7 := (ξ, prim(δL, δR)) where ξ is the case symbol according to the table in chapter 7

xmin(γL, γR) xmin(δL, δR)

:= (ξ, min(γL, γR)) where ξ is the case symbol according to the table in chapter 7 := (ξ, min(δL, δR)) where ξ is the case symbol according to the table in chapter 7

Disjunctive component pairs: Implementations Conjunctive component pairs: Implementations

xprim(γL, γR)  xprim(δL, δR)
:= xprec([∧], γL, [∧], γR, [∧], [∧], [∧], 0, 0, 0)  := xprec([∨], δL, [∨], δL, [∨], [∨], [∨], 0, 0, 0)
prim(γL, γR)  prim(δL, δR)

:= Δ, where Δ is defined by (ξ, Δ) := xprim(γL, γR) := Γ, where Γ is defined by (ξ, Γ) := xprim(δL, δR)

xmin(γL, γR) xmin(δL, δR)

:= (ξ, Δ′) defined by (ξ, Δ) := xprim(γL, γR) and := (ξ, Γ′) defined by (ξ, Γ) := xprim(δL, δR) and

Δ′ := \{ \begin{matrix}Δ & if lg(Δ) ∈ \{1, 2\} \\ [∨γL, γR] & if lg(Δ) = 3 \end{matrix} Γ′ := \{ \begin{matrix}Γ & if lg(Γ) ∈ \{1, 2\} \\ [∧δL, δR] & if lg(Γ) = 3 \end{matrix}

min(γL, γR) min(δL, δR)

:= Δ, where Δ is defined by (ξ, Δ) := xmin(γL, γR) := Γ, where Γ is defined by (ξ, Γ) := xmin(δL, δR)

Auxiliary algorithms

\overline{∗} := \{ \begin{matrix}∨ & if ∗ = ∧ \\ ∧ & if ∗ = ∨ \end{matrix} \} for ∗ ∈ \{∧, ∨\}

algorithm xprec ([∗λ1...λi], [∗λi+1...λx], [∗λ′1...λ′j], [∗λ{′ \atop j+1}...λ′y], [∗π1...πa], [∗π′1...π′b], [∗π{′′ \atop 1}...π{′′ \atop c}], r, s, t)

begin

if r > 1

then (“NMNN”, [\overline{∗}[∗λ1...λiλi+1...λx][∗λ′1...λ′j λ{′ \atop j+1}...λ′y]])

else if x = i

then if r = 0

then if s = 0

then if (j = y and t = 0)

then (“N000”, [\overline{∗}[∗λ1...λi]])

else (“N00P”, [\overline{∗}[∗λ1...λi]])

else if (j = y and t = 0)

then (“N0P0”, [\overline{∗}[∗λ′1...λ′j]])

else (“N0PP”, [\overline{∗}[∗λ1...λi][∗λ′1...λ′j λ{′ \atop j+1}...λ′y]])

else if s = 0

then if (j = y and t = 0)

then (“N100”, [\overline{∗}[∗π1...πa]])

else (“N10P”, [\overline{∗}[∗λ1...λi][∗π′1...π′bλ{′ \atop j+1}...λ′y]])

else if (j = y and t = 0)

then (“N1P0”, [\overline{∗}[∗π1...πa][∗λ′1...λ′j λ{′ \atop j+1}...λ′y]])

else (“N1PP”, [\overline{∗}[∗λ1...λi][∗λ′1...λ′j λ{′ \atop j+1}...λ′y][∗π{′′ \atop 1}...π{′′ \atop c}λ{′ \atop j+1}...λ′y]])

else if j = y

then if r = 0

then if t = 0

then (“N0P0”, [\overline{∗}[∗λ′1...λ′j]])

else (“N0PP”, [\overline{∗}[∗λ1...λiλi+1..λx][∗λ′1...λ′j]])

else if t = 0

then (“N1P0”, [\overline{∗}[∗π1...πaλi+1...λx][∗λ′1...λ′j]])

else (“N1PP”, [\overline{∗}[∗λ1...λiλi+1...λx][∗λ′1...λ′j][∗π{′′ \atop 1}...π{′′ \atop c}λi+1...λx]])

else if |λi+1| < |λ{′ \atop j+1}|

then xprec ([∗λ1...λiλi+1], [∗λi+2...λx], [∗λ′1...λ′j], [∗λ{′ \atop j+1}...λ′y], [∗π1...πaλi+1], [∗π′1...π′b], [∗π{′′ \atop 1}...π{′′ \atop c}λi+1], r, s + 1, t)

else if |λ{′ \atop j+1}| < |λi+1|

then xprec ([∗λ1...λi], [∗λi+1...λx], [∗λ′1...λ′j λ{′ \atop j+1}], [∗λ{′ \atop j+2}...λ′y], [∗π1...πa], [∗π′1...π′bλ{′ \atop j+1}], [∗π{′′ \atop 1}...π{′′ \atop c}λ{′ \atop j+1}], r, s, t + 1)

else if λi+1 = λj+1

then xprec ([∗λ1...λiλi+1], [∗λi+2...λx], [∗λ′1...λ′j λ{′ \atop j+1}], [∗λ{′ \atop j+2}...λ′y], [∗π1...πaλi+1], [∗π′1...π′bλ{′ \atop j+1}], [∗π{′′ \atop 1}...π{′′ \atop c}λ{′ \atop j+1}], r, s, t)

else xprec ([∗λ1...λi], [∗λi+2...λx], [∗λ′1...λ′j], [∗λ{′ \atop j+2}...λ′y], [∗π1...πa], [∗π′1...π′b], [∗π{′′ \atop 1}...π{′′ \atop c}], r + 1, s, t)

end.

9 The M–Procedure

We already mentioned the M-Procedure: Given a DNF Δ, then

(i) Choose any two components γ_{L} and γ_{R} of Δ and replace them by the components of min (γ_{L}, γ_{R}). (ii) Repeat step (i) until every pair of components of Δ is minimal. M–Procedure (Δ) shall denote the final result.

The result M-Procedure (Δ) is not uniquely defined. Depending on how the instruction “Choose any two components ...” is implemented, the result can be different (i.e. not equal and not similar), as the following example demonstrates. This shows again that the set of M2DNF’s is not (pre-)canonic.

\underline{Example} First version:

Δ = [∨ \underbrace{[∧AB\overline{C}]} \underbrace{[∧ABC]}[∧A\overline{B}C][∧\overline{A}\overline{B}C]]

min([∧AB\overline{C}], [∧ABC]) = [∨[∧AB]]

[∨ \overbrace{[∧AB]} \underbrace{[∧A\overline{B}C]} \underbrace{[∧\overline{A}\overline{B}C]}]

min([∧A\overline{B}C], [∧\overline{A}\overline{B}C]) = [∨[∧\overline{B}C]]

[∨[∧AB] \overbrace{[∧\overline{B}C]}] =: Δ_{1}

Second version:

Δ = [∨ \underbrace{[∧AB\overline{C}]} \underbrace{[∧ABC]}[∧A\overline{B}C][∧\overline{A}\overline{B}C]]

min([∧AB\overline{C}], [∧ABC]) = [∨[∧AB]]

[∨ \underbrace{\overbrace{[∧AB]}} \underbrace{[∧A\overline{B}C]}[∧\overline{A}\overline{B}C]]

min([∧AB], [∧A\overline{B}C]) = [∨[∧AB][∧AC]]

[∨ \overbrace{[∧AB]} \overbrace{\underbrace{[∧AC]}} \underbrace{[∧\overline{A}\overline{B}C]}]

min([∧AC], [∧\overline{A}\overline{B}C]) = [∨[∧AC][∧\overline{B}C]]

[∨[∧AB] \overbrace{[∧AC]} \overbrace{[∧\overline{B}C]}] =: Δ_{2}

Depending on the order in which the components are chosen, the result of M–Procedure (Δ) is Δ_{1} in the first version and Δ_{2} in the second version, with Δ_{1} ≉ Δ_{2}. (By the way, Δ_{1} is the MDNF and Δ_{2} is the PDNF of Δ.)

10 * Implementation of the M– Procedure

\underline{Notation} Let Δ = [∨γ_{1}...γ_{n}] and Δ′ = [∨γ′_{1}...γ′_{m}] be two DNF’s. We define

Δ ∨ Δ′ := [∨γ_{1}...γ_{n}γ′_{1}...γ′_{m}]

Accordingly we write Δ_{1} ∨...∨Δ_{d} for more than two DNF’s.

We are going to create the recursive algorithm mrec to implement the M–Procedure. Let Δ be an arbitrary DNF that is going to be tansformed into a M2DNF. First of all we split Δ into two DNF’s

\overbrace{\underbrace{[∨........]}_{Δ_{0}} ∨ \underbrace{[∨........]}_{Ψ_{2}}}^{Δ}

called Δ_{0} and Ψ_{2}, so Δ = Δ_{0} ∨ Ψ_{2}. In particular

• Δ_{0} is the part of Δ that isn’t pairwise minimal yet, while

• Ψ_{2} is the part of Δ, that is already a M2DNF.

At the beginning, of course there is

• Δ_{0} = Δ

• Ψ_{2} = [∨]

As the procedure proceeds we attempt to increase Ψ_{2}, while Δ_{0} is getting smaller, until finally Δ_{0} = [∨] and Ψ_{2} is returned as the result of the procedure. Therefore in each single step we take the first component γ_{1} of Δ_{0} and for every component μ_{i} of Ψ_{2} we minimize by means of min(γ_{1}, μ_{i}). We further split Ψ_{2} into Ψ_{2} = Δ_{1} ∨ Δ_{2} where

• Δ_{1} is the part of Ψ_{2} that already is a M2DNF together with γ_{1} (we call it Ψ_{1}) and

• Δ_{2} is the remaining part of Ψ_{2}.

\overbrace{\underbrace{[∨ \overbrace{γ_{1}}^{Ψ_{1}} γ_{2}...γ_{c}]}_{Δ_{0}} ∨ \underbrace{\underbrace{[∨ \overbrace{μ_{1}...μ_{n}}^{Ψ_{1}}]}_{Δ_{1}} ∨ \underbrace{[∨μ_{n+1}...μ_{n+m}]}_{Δ_{2}}}_{Ψ_{2}}}^{Δ}

At the beginning of this inner loop we initialize

• Δ_{1} := [∨]

• Δ_{2} := Ψ_{2}

When we continue and if we reach Δ_{2} = [∨], we put Ψ_{2} := [∨γ_{1}] ∨ Ψ_{2} and erase γ_{1} from Δ_{0}. In the following full definition of mrec it is important to note that

• at each step the conditions for Ψ_{1} and Ψ_{2} are satisfied

• the whole expression Δ = Δ_{0} ∨Δ_{1} ∨Δ_{2} is constantly getting shorter, or it remains the same while Ψ_{1} or Ψ_{2} is increasing

so that finally Ψ_{2} is returned as the M2DNF of Δ.

Definition and theorem Let

• Δ_{0} = [∨γ_{1}...γ_{c}] be a DNF with c ≥ 0

• Δ_{1} = [∨μ_{1}...μ_{n}] be a M2DNF with n ≥ 0

• Δ_{2} = [∨μ_{n+1}...μ_{n+m}] be a M2DNF with m ≥ 0 such that

• Ψ_{1} := \{ \begin{matrix}[∨μ_{1}...μ_{n}] & if c = 0 \\ [∨γ_{1}μ_{1}...μ_{n}] & if c > 0 \end{matrix} \} is a M2DNF

• Ψ_{2} := Δ_{1} ∨ Δ_{2} = [∨μ_{1}...μ_{n}μ_{n+1}...μ_{n+m}] is a M2DNF. Then we define

mrec (Δ_{0}, Δ_{1}, Δ_{2})

according to the table at the end of this chapter. Then it holds that

• mrec (Δ_{0}, Δ_{1}, Δ_{2}) ⇔ Δ_{0} ∨ Δ_{1} ∨ Δ_{2}

• mrec (Δ_{0}, Δ_{1}, Δ_{2}) is a M2DNF.

The definition of mrec immediately allows to derive:

• An implementation of the M–Procedure:

\underline{Definition} M–Procedure (Δ) := mrec (Δ, [∨], [∨]) for every DNF Δ.

\underline{Theorem} M–Procedure (Δ) is a M2DNF of Δ, for every DNF Δ.

• A M2DNF normalizer:

\underline{Definition} m2dnf (φ) := M–Procedure (dnf (φ)) for every formula φ

\underline{Theorem}

m2dnf (φ) is a M2DNF of φ, for every formula φ.

• A special fast disjunctor:

\underline{Definition} dnf–or–m2dnf (Δ_{1}, Δ_{2}) := mrec (Δ_{1}, [∨], Δ_{2}) for every DNF Δ_{1} and M2DNF Δ_{2}.

\underline{Theorem} dnf–or–m2dnf (Δ_{1}, Δ_{2}) is a M2DNF of Δ_{1} ∨ Δ_{2}, for every DNF Δ_{1} and M2DNF Δ_{2}.

Proof of the correctness of mrec

We want to proof that mrec is well defined and does exactly what is told. This proof actually comprises four parts: (I) mrec is well–defined: in any case the recursion calls itself, the conditions of the definition must hold. (II) mrec terminates: the algorithm has to terminate after a finite number of steps for every permitted input. (III) mrec (Δ_{0}, Δ_{1}, Δ_{2}) is a M2DNF. (IV) mrec (Δ_{0}, Δ_{1}, Δ_{2}) ⇔ Δ_{0} ∨ Δ_{1} ∨ Δ_{2}

When we start with Δ_{0}^{0} := Δ_{0}, Δ_{1}^{0} := Δ_{1}, and Δ_{2}^{0} := Δ_{2}, the application of mrec initiates a sequence mrec (Δ_{0}^{0}, Δ_{1}^{0}, Δ_{2}^{0}) = mrec (Δ_{0}^{1}, Δ_{1}^{1}, Δ_{2}^{1}) = mrec (Δ_{0}^{2}, Δ_{1}^{2}, Δ_{2}^{2}) = ... = mrec (Δ_{0}^{i}, Δ_{1}^{i}, Δ_{2}^{i}) = mrec (Δ_{0}^{i+1}, Δ_{1}^{i+1}, Δ_{2}^{i+1}) = ...

For the proof of (I) we will need two lemmas, where the first one was mentioned earlier, and the second one is quite obvious: Lemma 1 Every DNF of length 0 or 1 is a M2DNF. Lemma 2 If Ψ ⊂ Ψ′ and Ψ′ is a M2DNF, so is Ψ.

(I) Proof that mrec is well–defined

Each step of the recursion has the general form mrec (Δ_{0}^{i}, Δ_{1}^{i}, Δ_{2}^{i})

= \{ \begin{matrix}Δ_{1}^{i} ∨ Δ_{2}^{i} & in case (1) \\ mrec (Δ_{0}^{i+1}, Δ_{1}^{i+1}, Δ_{2}^{i+1}) & in case (2) or (3.x) \end{matrix}

We need to show by induction that the recursion step i + 1 is well defined, in other words that the conditions for Ψ_{1}^{i+1} and Ψ_{2}^{i+1} of the definition are met. In particular we have:

(2) Ψ_{1}^{i+1} = \{ \begin{matrix}[∨] & if c = 1 \\ [∨γ_{2}] & if c > 1 \end{matrix} \} is a M2DNF

(Lemma 1)

Ψ_{2}^{i+1} = [∨γ_{1}μ_{1}...μ_{n}] = Ψ_{2}^{i} is a M2DNF (induction)

(3.1) Ψ_{1}^{i+1} = \{ \begin{matrix}[∨] & if c = 1 \\ [∨γ_{2}] & if c > 1 \end{matrix} \} is a M2DNF

(Lemma 1)

Ψ_{2}^{i+1} = [∨μ_{1}...μ_{n}μ_{n+1}...μ_{n+m}] = Ψ_{2}^{i} is a M2DNF (induction)

(3.2) Ψ_{1}^{i+1} = \{ \begin{matrix}[∨] & if c = 1 and m = 1 \\ [∨μ_{n+2}] & if c = 1 and m > 1 \\ [∨γ_{2}] & if c > 1 \end{matrix} \} is

a M2DNF (Lemma 1)

Ψ_{2}^{i+1} = [∨γ_{1}μ_{1}...μ_{n}] = Ψ_{1}^{i} is a M2DNF (induction)

(3.3) Ψ_{1}^{i+1} = \{ \begin{matrix}[∨] & if c = 1 \\ [∨γ_{2}] & if c > 1 \end{matrix} \} is a M2DNF

(Lemma 1)

Ψ_{2}^{i+1} = [∨μ_{1}...μ_{n}μ_{n+1}...μ_{n+m}] = Ψ_{2}^{i} is a M2DNF (induction)

(3.4) Ψ_{1}^{i+1} = [∨γ_{1}μ_{1}...μ_{n}μ_{n+1}] is a M2DNF because [∨γ_{1}μ_{1}...μ_{n}] = Ψ_{1}^{i} is a M2DNF (induction), [∨μ_{1}...μ_{n}μ_{n+1}] ⊆ Ψ_{2}^{i} is a M2DNF (Lemma 2) and [∨γ_{1}μ_{n+1}] is minimal. Ψ_{2}^{i+1} = Ψ_{2}^{i} is a M2DNF (induction).

(3.5) Ψ_{1}^{i+1} = \{ \begin{matrix}[∨] & if c = 1 \\ [∨γ_{2}] & if c > 1 \end{matrix} \} is a M2DNF

(Lemma2)

Ψ_{2}^{i+1} ⊆ Ψ_{2}^{i} is a M2DNF (Lemma 2)

(3.6) Ψ_{1}^{i+1} = \{ \begin{matrix}[∨γ′_{1}] & if c = 1 \\ [∨γ_{2}] & if c > 1 \end{matrix} \} is a M2DNF

(Lemma 1)

Ψ_{2}^{i+1} = [∨γ_{1}μ_{1}...μ_{n}] = Ψ_{1}^{i} is a M2DNF (induction)

(3.7) Ψ_{1}^{i+1} = \{ \begin{matrix}[∨γ′_{1}] & if c = 1 \\ [∨γ_{2}] & if c > 1 \end{matrix} \} is a M2DNF

(Lemma 1)

Ψ_{2}^{i+1} = Ψ_{1}^{i} is a M2DNF (induction) (3.8) same as (3.4) (3.9) same as (3.4)

Thus, mrec is well–defined.

(II) Proof that mrec terminates

We define the following strict order^{16} ≻ on the set of all DNF triples:

(Δ_{0}, Δ_{1}, Δ_{2}) ≻ (Δ′_{0}, Δ′_{1}, Δ′_{2})

iff( \begin{matrix}& vol (Δ′_{0} ∨ Δ′_{1} ∨ Δ′_{2}) < vol (Δ_{0} ∨ Δ_{1} ∨ Δ_{2}) \\ & or \\ ( & vol (Δ′_{0} ∨ Δ′_{1} ∨ Δ′_{2}) = vol (Δ_{0} ∨ Δ_{1} ∨ Δ_{2}) and lg (Δ′_{0}) < lg (Δ_{0}) & ) \\ & or \\ ( & vol (Δ′_{0} ∨ Δ′_{1} ∨ Δ′_{2}) = vol (Δ_{0} ∨ Δ_{1} ∨ Δ_{2}) and lg (Δ′_{0}) = lg (Δ_{0}) and lg (Δ′_{2}) < lg (Δ_{2}) & ) \end{matrix} )

Obviously, every chain

(Δ_{0}^{0}, Δ_{1}^{0}, Δ_{2}^{0}) ≻ (Δ_{0}^{1}, Δ_{1}^{1}, Δ_{2}^{1}) ≻ ... ≻ (Δ_{0}^{i}, Δ_{1}^{i}, Δ_{2}^{i}) ≻ ... has to terminate. And because the following table shows that

(Δ_{0}^{i}, Δ_{1}^{i}, Δ_{2}^{i}) ≻ (Δ_{0}^{i+1}, Δ_{1}^{i+1}, Δ_{2}^{i+1})

indeed for every i for which the triple i + 1 is defined, we have proven that mrec (Δ_{0}, Δ_{1}, Δ_{2}) terminates for every permitted input.

16asymmetric and transitive

Case  vol (Δ{i+1 \atop 0} ∨ Δ{i+1 \atop 1} ∨ Δ{i+1 \atop 2})  lg (Δ{i+1 \atop 0})  lg (Δ{i+1 \atop 2})
(2)  vol (Δi 0 ∨ Δi 1 ∨ Δi 2)  lg (Δi 0) − 1  —
(3.1)  vol (Δi 0 ∨ Δi 1 ∨ Δi 2) − lg (γ1)  —  —
with lg (γ1) > 0
(3.2) vol (Δi 0 ∨ Δi 1 ∨ Δi 2) − lg (μn+1) — —
with lg (μn+1) > 0
(3.3) vol (Δi 0 ∨ Δi 1 ∨ Δi 2) − lg (γ1) — —
with lg (γ1) > 0
(3.4)  vol (Δi 0 ∨ Δi 1 ∨ Δi 2)  lg (Δi 0)  lg (Δi 2) − 1
(3.5)  vol (Δi 0 ∨ Δi 1 ∨ Δi 2) − lg (γ1) − 1  —  —
(3.6)  vol (Δi 0 ∨ Δi 1 ∨ Δi 2) − 1  —  —
(3.7)  vol (Δi 0 ∨ Δi 1 ∨ Δi 2) − 1  —  —
(3.8)  vol (Δi 0 ∨ Δi 1 ∨ Δi 2)  lg (Δi 0)  lg (Δi 2) − 1
(3.9)  vol (Δi 0 ∨ Δi 1 ∨ Δi 2)  lg (Δi 0)  lg (Δi 2) − 1

(III) Proof that mrec (Δ_{0}, Δ_{1}, Δ_{2}) is a M2DNF

The algorithm terminates if and only if Δ_{0} = [∨]. And then it returnes Δ_{1} ∨ Δ_{2} =: Ψ_{2} which is a M2DNF.

(IV) Proof that mrec (Δ_{0}, Δ_{1}, Δ_{2}) ⇔ Δ_{0} ∨ Δ_{1} ∨ Δ_{2}

In each recursion step the components only change their order or they are replaced by equivalent components. All these operations don’t change the semantic.

end of proof.

mrec ([∨γ_{1}...γ_{c}], [∨μ_{1}...μ_{n}], [∨μ_{n+1}...μ_{n+m}])

:= \{ \begin{matrix}[∨μ_{1}...μ_{n}μ_{n+1}...μ_{n+m}] & if c = 0 & (1) \\ mrec ([∨γ_{2}...γ_{c}], [∨], [∨γ_{1}μ_{1}...μ_{n}]) & if c > 0 and m = 0 & (2) \\ mrec ([∨γ_{2}...γ_{c}], [∨], [∨μ_{1}...μ_{n}μ_{n+1}...μ_{n+m}]) & if c > 0 and m > 0 and & (3.1) \\ & xmin (γ_{1}, μ_{n+1}) = (“N000”, [∨μ_{n+1}]) \\ mrec ([∨γ_{2}...γ_{c}μ_{n+2}...μ_{n+m}], [∨], [∨γ_{1}μ_{1}...μ_{n}]) & if c > 0 and m > 0 and & (3.2) \\ & xmin (γ_{1}, μ_{n+1}) = (“N00P”, [∨γ_{1}]) \\ mrec ([∨γ_{2}...γ_{c}], [∨], [∨μ_{1}...μ_{n}μ_{n+1}...μ_{n+m}]) & if c > 0 and m > 0 and & (3.3) \\ & xmin (γ_{1}, μ_{n+1}) = (“N0P0”, [∨μ_{n+1}]) \\ mrec ([∨γ_{1}...γ_{c}], [∨μ_{1}...μ_{n}μ_{n+1}], [∨μ_{n+2}...μ_{n+m}]) & if c > 0 and m > 0 and & (3.4) \\ & xmin (γ_{1}, μ_{n+1}) = (“N0PP”, [∨γ_{1}μ_{n+1}]) \\ mrec ([∨γ_{2}...γ_{c}γ′], [∨], [∨μ_{1}...μ_{n}μ_{n+2}...μ_{n+m}]) & if c > 0 and m > 0 and & (3.5) \\ & xmin (γ_{1}, μ_{n+1}) = (“N100”, [∨γ′]) \\ mrec ([∨γ_{2}...γ_{c}μ′_{n+1}μ_{n+2}...μ_{n+m}], [∨], [∨γ_{1}μ_{1}...μ_{n}]) & if c > 0 and m > 0 and & (3.6) \\ & xmin (γ_{1}, μ_{n+1}) = (“N10P”, [∨γ_{1}μ′_{n+1}]) \\ mrec ([∨γ_{2}...γ_{c}γ′_{1}], [∨], [∨μ_{1}...μ_{n}μ_{n+1}...μ_{n+m}]) & if c > 0 and m > 0 and & (3.7) \\ & xmin (γ_{1}, μ_{n+1}) = (“N1P0”, [∨γ′_{1}μ_{n+1}]) \\ mrec ([∨γ_{1}...γ_{c}], [∨μ_{1}...μ_{n}μ_{n+1}], [∨μ_{n+2}...μ_{n+m}]) & if c > 0 and m > 0 and & (3.8) \\ & xmin (γ_{1}, μ_{n+1}) = (“N1PP”, [∨γ_{1}μ_{n+1}]) \\ mrec ([∨γ_{1}...γ_{c}], [∨μ_{1}...μ_{n}μ_{n+1}], [∨μ_{n+2}...μ_{n+m}]) & if c > 0 and m > 0 and & (3.9) \\ & xmin (γ_{1}, μ_{n+1}) = (“NMNN”, [∨γ_{1}μ_{n+1}]) \end{matrix}

11 The completeness theorem and the P–Procedure

The completeness theorem

The M–Procedure generates a M2DNF of a given DNF. But actually we are much more interested in a P– Procedure to derive the PDNF. In this chapter we will formulate the completeness theorem that gives us necessary and sufficient criteria for which a M2DNF is a PDNF by means of the covering concept, and that will be the foundation for the P–Procedure.

\underline{Definition} A DNF Δ is called factor complete or f– complete, iff γ ⊑ Δ for every factor γ of Δ. In other words, Δ is f–complete iff every prime factor of Δ is a component of Δ (i.e. Δ_{p} ⊆ Δ where Δ_{p} is the PDNF of Δ).

\underline{Examples}

• [∨] is f–complete in a trivial way, because it has no factor.

• [∨[∧]] is f–complete, because every NLC γ is a factor, γ ⇒ [∧] and so γ ⊑ [∨[∧]].

\underline{Definition} For a DNF Δ we define CP rimes(Δ) to be the DNF which components are the c–prime factors of all the complementary and minimal pairs of components of Δ. Thus:^{17}

Algorithm CP rimes([∨γ_{1}...γ_{n}]) begin

Δ′ := [∨] ; for i := 1 to n − 1 do

for j := i + 1 to n do

if [∨γ_{i}γ_{j}] is complementary minimal with the

c–prime factor γ′ then Δ′ := Δ′ ∨ [∨γ′] ;

return Δ′ ; end.

\underline{Example} Δ = [∨[∧A\overline{B}][∧B\overline{C}][∧\overline{A}C]] contains three pairs of components that are complementary minimal, namely

• [∧A\overline{B}] and [∧B\overline{C}]. Their c–prime factor is [∧A\overline{C}].

• [∧A\overline{B}] and [∧\overline{A}C] with c–prime factor [∧\overline{B}C].

• [∧B\overline{C}] and [∧\overline{A}C] with c–prime factor [∧\overline{A}B]. So CP rimes(Δ) = [∨[∧A\overline{C}][∧\overline{B}C][∧\overline{A}B]] \underline{Definition}

A DNF Δ is said to be complementary prime complete or c–complete iff CP rimes(Δ) ⊑ Δ.

\underline{Example} Again let Δ = [∨[∧A\overline{B}][∧B\overline{C}][∧\overline{A}C]]. Δ is not c–complete because, for example [∧A\overline{C}] ∈ CP rimes(Δ), but [∧A\overline{C}] ⋢ Δ and thus CP rimes(Δ) ⋢ Δ.

\underline{Theorem} Every f–complete DNF is c–complete.

\underline{Proof} Easy, since every c–prime factor of a pair of complementary minimal components is a factor.

\underline{Corollary} • [∨] and [∨[∧]] are c–complete.

• Every PDNF is c–complete.

Now we are able to state the central completeness theorem:

Theorem (Completeness)

For every DNF Δ the following statements are equivalent

(i) Δ is a PDNF (ii) Δ is a f–complete M2DNF (iii) Δ is a c–complete M2DNF

To proof this, we first proof two lemmata:

\underline{Lemma 1} For every DNF Δ and NLC γ with At (Δ) ⊆ At (γ) there is γ ⇒ Δ iff γ ⊑ Δ.

\underline{Proof} Let γ′ ∈ Δ. With At (Δ) ⊆ At (γ) we have At (γ′) ⊆ At (γ). So there are exactly two different possibilities:

• either γ′ ⊆ γ, and then γ ⇒ γ′, and so γ ⊑ Δ • or γ′ ⊈ γ, and then there must be (at least) one

literal λ ∈ γ′ with \overline{λ} ∈ γ, so that [∧γγ′] ⇔ 0 We can now proof that γ ⇒ Δ iff γ ⊑ Δ

• Suppose that γ ⇒ Δ. Because γ ⇎ 0 for every NLC γ, there must be at least one γ′ ∈ Δ such that [∧γγ′] ⇎ 0. But this implies that γ′ ⊆ γ and γ ⊑ Δ.

• Suppose that γ ⊑ Δ. Then there is a γ′ ∈ Δ with γ ⇒ γ′ by definition, and so γ ⇒ γ′ ⇒ Δ.

Thus: γ ⇒ Δ iff γ ⊑ Δ.

17Again Δ_{1} ∨ Δ_{2} denotes the simple concatenation of two DNF’s.

\underline{Lemma 2} If Δ is a c–complete M2DNF and γ a factor of Δ, then γ ⊑ Δ.

\underline{Proof} Suppose γ = [∧λ_{1}...λ_{n}]. We put {α_{1}, ..., α_{a}} := At (Δ) − At (γ). (The α_{1},...,α_{a} are uniquely defined if we demand that α_{1} < ... < α_{a}. But in fact their order is of no importance here.) We are going to proof that γ ⊑ Δ by induction on a.

• Suppose a = 0.

Then At (Δ) ⊆ At (γ). And since γ is a factor and γ ⇒ Δ, there is γ ⊑ Δ according to lemma 1.

• Suppose a > 0.

We put γ_{0} := [ ˙∧λ_{1}...λ_{n}\overline{α_{1}}] and γ_{1} := [ ˙∧λ_{1}...λ_{n}α_{1}] so that γ = [∧λ_{1}...λ_{n}] ⇔ [∨γ_{0}γ_{1}]. By virtue of the induction it holds that γ_{0} ⊑ Δ and γ_{1} ⊑ Δ. So there must be γ′_{0}, γ′_{1} ∈ Δ such that γ_{0} ⇒ γ′_{0} (i.e. γ′_{0} ⊆ γ_{0}) and γ_{1} ⇒ γ′_{1} (i.e. γ′_{1} ⊆ γ_{1}). We distinguish the following three cases:

• First case: \overline{α_{1}} ∉ γ′_{0}.

Then γ′_{0} ⊆ γ_{0} ⊆ γ and so γ ⇒ γ′_{0}, and that means that γ ⊑ Δ because γ′_{0} ∈ Δ

• Second case: α_{1} ∉ γ′_{1}.

Similar to the first case, γ′_{0} ⊆ γ_{0} ⊆ γ and so again γ ⊑ Δ.

• Third case: \overline{α_{1}} ∈ γ′_{0} and α_{1} ∈ γ′_{1}.

In this case γ′_{0} and γ′_{1} have exactly this one complementary literal, and that makes them complementary NLC’s. And since Δ is a M2DNF and γ′_{0} and γ′_{1} are components of Δ, they must be a minimal pair. So, γ′_{0} = [ ˙∧π_{1}...π_{p}\overline{α_{1}}σ_{1}...σ_{s}] and γ′_{1} = [ ˙∧π_{1}...π_{p}α_{1}τ_{1}...τ_{t}] with p ≥ 0, s > 0, t > 0, {σ_{1}, ..., σ_{s}} ∩ {τ_{1}, ..., τ_{t}} = {} and {π_{1}, ..., π_{p}, σ_{1}, ..., σ_{s}, τ_{1}, ..., τ_{t}} ⊆ {λ_{1}, ..., λ_{n}}. γ′_{c} := [ ˙∧π_{1}...π_{p}σ_{1}...σ_{s}τ_{1}...τ_{t}] is the c–prime factor of γ′_{0} and γ′_{1} and so γ′_{c} ⊆ γ, that is γ ⇒ γ′_{c}. Δ is c–complete, so γ′_{c} ⊑ Δ and that means that γ ⊑ Δ.

Thus, γ ⊑ Δ in each case.

Now we are able to give the whole proof of the completeness theorem:

Proof (Completeness Theorem)

(i) implies (ii)

Every PDNF is both f–complete and pairwise minimal, as we already proved.

(ii) implies (i)

Let Δ be a f–complete M2DNF. Suppose that Δ is not a PDNF. So there must be a component γ ∈ Δ that is not a prime factor of Δ. Since Δ is f–complete, there must be a γ′ ∈ Δ with γ ˙⇒γ′. But in that case min (γ, γ′) = [∨γ′] so that Δ wouldn’t be minimal, different to the initial assumption. Thus, every f–complete M2DNF must be a PDNF.

(ii) implies (iii)

Let Δ be a f–complete M2DNF. If there is a complementary and minimal pair γ_{L} and γ_{R} of components in Δ and their c–prime factor is γ, then γ ⇒ [∨γ_{L}γ_{R}] ⇒ Δ, so that γ is a factor of Δ. Because Δ is f–complete it holds that γ ⊑ Δ. So Δ is c–complete.

(iii) implies (ii)

Let Δ be a c–complete M2DNF and γ be any factor of Δ. According to lemma 2 there is γ ⊑ Δ. So Δ is f–complete.

Summary: (i) iff (ii) iff (iii)

The P–Procedure

\underline{Lemma 3} [∨γ_{L}γ_{R}] ⊑ min (γ_{L}, γ_{R}), for any two NLC’s γ_{L} and γ_{R}

\underline{Proof} min (γ_{L}, γ_{R}) is

• either of length 1, thus of the form [∨γ′], and then γ_{L} ⇒ γ′ and γ_{R} ⇒ γ′

• or of length 2, thus of the form [∨γ′_{L}γ′_{R}], and then γ_{L} ⇒ γ′_{L} and γ_{R} ⇒ γ′_{R}.

So there is always [∨γ_{L}γ_{R}] ⊑ min (γ_{L}, γ_{R}).

\underline{Lemma 4} Δ ⊑ M–Procedure (Δ) for every DNF Δ.

\underline{Proof} In every step of the M–Procedure two components γ_{L} and γ_{R} of Δ are replaced by the components of min (γ_{L}, γ_{R}). Let Δ′ be the result of this replacement. Because [∨γ_{L}γ_{R}] ⊑ min (γ_{L}, γ_{R}) (Lemma 3) there is Δ ⊑ Δ′ and thus Δ ⊑ ... ⊑ M–Procedure (Δ). ⊑ is transitive, so Δ ⊑ M–Procedure (Δ).

\underline{Lemma 5} Let Δ_{1} be a DNF and Δ_{2} be a M2DNF. If M–Procedure (Δ_{1} ∨ Δ_{2}) ≈ Δ_{2}, then Δ_{1} ⊑ Δ_{2}.

\underline{Proof} Because M–Procedure (Δ_{1} ∨ Δ_{2}) ≈ Δ_{2} and Lemma 4, there is Δ_{1} ∨ Δ_{2} ⊑ Δ_{2} and thus Δ_{1} ⊑ Δ_{2}.

Now, we have all the ingredients to implement the P– Procedure that transforms any DNF into its PDNF. It is standing on two feet: the M–Procedure and the completeness theorem, that guarantees us that a M2DNF Δ is a PDNF iff CPrimes (Δ) ⊑ Δ. Because of lemma 5 it follows that for a DNF Δ and Π := CPrimes (Δ) holds:

• if M–Procedure (Π ∨ Δ) ≈ Δ, then Δ is a M2DNF with Π ⊑ Δ and thus Δ is a PDNF.

We use this to implement the P–Procedure that generates for a given DNF Δ a sequence Δ^{1}, Π^{1}, Δ^{2}, Π^{2}, ..., Δ^{i−1}, Π^{i−1}, Δ^{i}, Π^{i}, ... where

• Δ^{1} := M–Procedure (Δ)

• Π^{i} := CPrimes (Δ^{i})

• Δ^{i+1} := M–Procedure (Π^{i} ∨ Δ^{i})

We know that Δ ⇔ Δ^{1} ⇔ ... ⇔ Δ^{i} ⇔ .... So, if there is a fixpoint z with Δ^{z} ≈ Δ^{z+1} (and thus Δ^{z} ≈ Δ^{z+n} for all n), Δ^{z} has to be the PDNF of Δ. Thus, the only thing that is left to be proven is that such a z actually exists for every DNF Δ.^{18} But first we formulate this implementation of the P–Procedure properly:

Algorithm P–Procedure (Δ) begin

i := 1 ; Δ^{1} := M–Procedure (Δ) ; repeat

Π^{i} := CPrimes (Δ^{i}) ; i := i + 1 ; Δ^{i} := M–Procedure (Π^{i−1} ∨ Δ^{i−1}) ;

until Δ^{i} ≈ Δ^{i−1} ; return Δ^{i} ;

end.

The following theorem will enable the proof that the P–Procedure terminates for every input DNF Δ.

\underline{Theorem} ⊑ is a (partial) order on the set of all M2DNF’s in the following sense:

• ⊑ is reflexive

• ⊑ is transitive • ⊑ is anti–symmetric: Δ_{1} ⊑ Δ_{2} and Δ_{2} ⊑ Δ_{1} im-

plies Δ_{1} ≈ Δ_{2}

\underline{Proof} We stated earlier that ⊑ is a quasi–order on the set of DNF’s. It remains to show the anti–symmetry: Assume that Δ_{1} ⊑ Δ_{2} and Δ_{2} ⊑ Δ_{1}, but Δ_{1} ≉ Δ_{2}. That would mean the existence of a γ ∈ Δ_{1} with γ ∉ Δ_{2} (or the other way round). Since Δ_{1} ⊑ Δ_{2} there must be a γ′ ∈ Δ_{2} with γ ⇒ γ′. On the other hand Δ_{2} ⊑ Δ_{1} implies the existence of a γ′′ ∈ Δ_{1} with γ′ ⇒ γ′′. But then γ ⇒ γ′′, and min (γ, γ′′) = [∨γ′′], and that contradicts the assumption that Δ_{1} is pairwise minimal.

Proof (Termination of the P–Procedure) The sequence Δ^{1}, Δ^{2}, ..., Δ^{i−1}, Δ^{i}, ... that the P– Procedure generates, is finite because:

(i) The set {Δ^{1}, Δ^{2}, ..., Δ^{i−1}, Δ^{i}, ...} is finite. For every DNF Δ there is At (CPrimes (Δ)) ⊆ At (Δ) and At (M–Procedure (Δ)) ⊆ At (Δ) and so At (Δ^{i}) ⊆ At (Δ) for every i. But since there is only a finite number of NLC’s on a finite atom set and M2DNF’s don’t have any two equal components, there is only a finite number of M2DNF’s on a finite atom set. (ii) Δ^{1} ⊑ Δ^{2} ⊑ Δ^{3} ⊑ ... because for every i = 1, 2, 3, ...

• Δ^{i} ⊑ Π^{i} ∨ Δ^{i} following immediately from Δ^{i} ⊆ Π^{i} ∨ Δ^{i}

• Π^{i} ∨ Δ^{i} ⊑ M–Procedure (Π^{i} ∨ Δ^{i}) according to lemma 4

and so, since ⊑ is transitive:

• Δ^{i} ⊑ M–Procedure (Π^{i} ∨ Δ^{i}) =: Δ^{i+1} Thus, for every sequence Δ^{1} ⊑ Δ^{2} ⊑ Δ^{3} ⊑ ... there must be a z such that Δ^{z} ≈ Δ^{z+1} ≈ Δ^{z+2} ≈ ... and this is the condition for the algorithm to terminate.

We summarize:

\underline{Theorem} P–Procedure (Δ) is the PDNF of Δ, for every DNF Δ.

18There is even an apriori upper bound for z, namely the number of atoms in Δ. But in average applications z is actually very small and quite independent of the number of atoms.

12 * Implementation of the P– Procedure

Our implementation of the P–Procedure comprised three operations: the M–Procedure, the generation of CP rimes and the ≈–decision. But instead of performing these operations subsequently, we can merge them into one single step and increase the speed of the algorithm considerably. Instead of first constructing the M–Procedure by using min and afterwards generating all the c–prime factors, we could immediately combine these by using prim instead of min, since “prim = min + c–prime”. We define a recursive algorithm prec to transform the P–Procedure similar to the algorithm mrec by extending its three arguments to four. Δ_{3} is the collection of all the c– prime factors of [∨γ_{1}μ_{1}],[∨γ_{1}μ_{2}],...,[∨γ_{1}μ_{n}]. If required Δ_{3} will be attached to Δ_{0} such that the property CPrimes (Ψ_{2}) ⊑ Δ_{0} ∨ Δ_{1} ∨ Δ_{2} ∨ Δ_{3} is maintained in every step of the process, so that in the end, when Ψ_{2} is returned, it is guaranteed to be c–complete.

Definition and Theorem Let

• Δ_{0} = [∨γ_{1}...γ_{n}] be a DNF with c ≥ 0

• Δ_{1} = [∨μ_{1}...μ_{n}] be a M2DNF with n ≥ 0

• Δ_{2} = [∨μ_{n+1}...μ_{n+m}] be a M2DNF with m ≥ 0 • Δ_{3} = [∨π_{1}...π_{p}] a DNF with p ≥ 0

• Δ := Δ_{0} ∨ Δ_{1} ∨ Δ_{2} ∨ Δ_{3}

such that

• Ψ_{1} := \{ \begin{matrix}[∨μ_{1}...μ_{n}] & if c = 0 \\ [∨γ_{1}μ_{1}...μ_{n}] & if c > 0 \end{matrix} \} is a M2DNF

• Ψ_{2} := Δ_{1} ∨ Δ_{2} = [∨μ_{1}...μ_{n}μ_{n+1}...μ_{n+m}] is a M2DNF

• CPrimes (Ψ_{2}) ⊑ Δ

Then we define

prec (Δ_{0}, Δ_{1}, Δ_{2}, Δ_{3})

according to the table at the end of this chapter. Then it holds that

• prec (Δ_{0}, Δ_{1}, Δ_{2}, Δ_{3}) ⇔ Δ
• prec (Δ_{0}, Δ_{1}, Δ_{2}, Δ_{3}) is a PDNF

Δ

\underbrace{[∨ \overbrace{γ_{1}}^{Ψ_{1}} γ_{2}...γ_{c}]}_{Δ_{0}} ∨ \underbrace{\underbrace{[∨ \overbrace{μ_{1}...μ_{n}}^{Ψ_{1}}]}_{Δ_{1}} ∨ \underbrace{[∨μ_{n+1}...μ_{n+m}]}_{Δ_{2}}}_{Ψ_{2}} ∨ \underbrace{[∨π_{1}...π_{p}]}_{Δ_{3}}

The definition of prec immediately allows to derive:

• A new and faster implementation of the P– Procedure: \underline{Definition}

P-Procedure (Δ) := prec (Δ, [∨], [∨], [∨]) for every DNF Δ. \underline{Theorem}

P-Procedure (Δ) is the PDNF of Δ, for every DNF Δ.

• A PDNF normalizer:

\underline{Definition} pdnf (φ) := P-Procedure (dnf (φ)) for every formula φ. \underline{Theorem}

pdnf (φ) is the PDNF of φ, for every formula φ.

• A special disjunctor:

\underline{Definition} dnf-or-pdnf (Δ_{1}, Δ_{2}) := prec (Δ_{1}, [∨], Δ_{2}, [∨]) for every DNF Δ_{1} and PDNF Δ_{2}.

\underline{Theorem} dnf-or-pdnf (Δ_{1}, Δ_{2}) is the PDNF of Δ_{1} ∨ Δ_{2}, for every DNF Δ_{1} and PNDF Δ_{2}.

Proof (Correctness of prec)

The correctness of mrec and the P–Procedure (in the first version) have been proved thoroughly. The correctness of prec can be proven analogue to mrec. Only the fact that prec always terminates deserves additional attention, and this is guaranteed by the correctness proof of the P–Procedure.

prec ([∨γ_{1}...γ_{c}], [∨μ_{1}...μ_{n}], [∨μ_{n+1}...μ_{n+m}], [∨π_{1}...π_{p}])

:= \{ \begin{matrix}[∨μ_{1}...μ_{n}μ_{n+1}...μ_{n+m}] & if c = 0 and p = 0 \\ prec ([∨π_{1}...π_{p}], [∨], [∨μ_{1}...μ_{n}μ_{n+1}...μ_{n+m}], [∨]) & if c = 0 and p > 0 \\ prec ([∨γ_{2}...γ_{c}π_{1}...π_{p}], [∨], [∨γ_{1}μ_{1}...μ_{n}], [∨]) & if c > 0 and m = 0 \\ prec ([∨γ_{2}...γ_{c}], [∨], [∨μ_{1}...μ_{n}μ_{n+1}...μ_{n+m}], [∨]) & if c > 0 and m > 0 and \\ & xprim (γ_{1}, μ_{n+1}) = (“N000”, [∨μ_{n+1}]) \\ prec ([∨γ_{2}...γ_{c}μ_{n+2}...μ_{n+m}π_{1}...π_{p}], [∨], [∨γ_{1}μ_{1}...μ_{n}], [∨]) & if c > 0 and m > 0 and \\ & xprim (γ_{1}, μ_{n+1}) = (“N00P”, [∨γ_{1}]) \\ prec ([∨γ_{2}...γ_{c}], [∨], [∨μ_{1}...μ_{n}μ_{n+1}...μ_{n+m}], [∨]) & if c > 0 and m > 0 and \\ & xprim (γ_{1}, μ_{n+1}) = (“N0P0”, [∨μ_{n+1}]) \\ prec ([∨γ_{1}...γ_{c}], [∨μ_{1}...μ_{n}μ_{n+1}], [∨μ_{n+2}...μ_{n+m}], [∨π_{1}...π_{p}]) & if c > 0 and m > 0 and \\ & xprim (γ_{1}, μ_{n+1}) = (“N0PP”, [∨γ_{1}μ_{n+1}]) \\ prec ([∨γ_{2}...γ_{c}γ′], [∨], [∨μ_{1}...μ_{n}μ_{n+2}...μ_{n+m}], [∨]) & if c > 0 and m > 0 and \\ & xprim (γ_{1}, μ_{n+1}) = (“N100”, [∨γ′]) \\ prec ([∨γ_{2}...γ_{c}μ′_{n+1}μ_{n+2}...μ_{n+m}π_{1}...π_{p}], [∨], [∨γ_{1}μ_{1}...μ_{n}], [∨]) & if c > 0 and m > 0 and \\ & xprim (γ_{1}, μ_{n+1}) = (“N10P”, [∨γ_{1}μ′_{n+1}]) \\ prec ([∨γ_{2}...γ_{c}γ′_{1}], [∨], [∨μ_{1}...μ_{n}μ_{n+1}...μ_{n+m}], [∨]) & if c > 0 and m > 0 and \\ & xprim (γ_{1}, μ_{n+1}) = (“N1P0”, [∨γ′_{1}μ_{n+1}]) \\ prec ([∨γ_{1}...γ_{c}], [∨μ_{1}...μ_{n}μ_{n+1}], [∨μ_{n+2}...μ_{n+m}], [∨ππ_{1}...π_{p}]) & if c > 0 and m > 0 and \\ & xprim (γ_{1}, μ_{n+1}) = (“N1PP”, [∨γ_{1}μ_{n+1}π]) \\ prec ([∨γ_{1}...γ_{c}], [∨μ_{1}...μ_{n}μ_{n+1}], [∨μ_{n+2}...μ_{n+m}], [∨π_{1}...π_{p}]) & if c > 0 and m > 0 and \\ & xprim (γ_{1}, μ_{n+1}) = (“NMNN”, [∨γ_{1}μ_{n+1}]) \end{matrix}

13 * Implementation: The PDNF and the PCNF system

Now we are able to gather the pieces to present the final PDNF and PCNF systems:

• Due to the duality principle we can implement the PCNF system dual to the PDNF system. All the auxiliary algorithms (jrec, prec, xprim, prim, and xprec) are exactly the ones already defined in earlier chapters, except that they make use of the junctor variable ∗, to serve for the PCNF system as well as for the PDNF system.

• In the last chapter we implemented the PDNF nor-

malizer as follows:

pdnf (φ) := P–Procedure (dnf (φ))

:= prec (dnf (φ), [∨], [∨], [∨])

But dnf makes repeatedly use of the distributive law and multiple occurings of components are not deleted. The resulting length of the DNF can explode, even for a simple looking φ. And instead of reducing this DNF in a second step by means of prec, it is in general more efficient^{19} to define pdnf as a recursion that operates itself only on PDNF’s. Besides, that is more elegant. So we don’t define the final PDNF system as an extension of the earlier defined DNF system, but design it as an independent one, only similar to the DNF system.

Finally note that:

• The following systems are only precanonic. We mentioned earlier how this can easily be extended to a canonic system. One can implement

• ord (Φ) a standard sorting algorithm that rearranges the components of the DNF or CNF Φ according to the given (or any other) linear order on the set of NLC’s and NLD’s, so that the result is an ordered DNF or CNF.

• opdnf (φ) := ord (pdnf (φ)) for the unique ordered PDNF and opcnf (φ) := ord (pcnf (φ)) for the unique ordered PCNF of each formula φ.

• The part with the algorithms on subvalence and covering can simply be attached.

19at least if we consider the worst case

The PDNF and the PCNF system

The PDNF system: Declaration The PCNF system: Declaration

The Normalizer The Normalizer

pdnf (φ)  pcnf (φ)

is the PDNF of φ, for every formula φ is the PCNF of φ, for every formula φ

Conjunctions and Disjunctions Conjunctions and Disjunctions

nlc-and-nlc (γ1, γ2) nlc-or-nld (δ1, δ2) is the PDNF of [∧γ1γ2], for every two NLC’s γ1 and γ2 is the PCNF of [∨δ1δ2], for every two NLD’s δ1 and δ2

nlc-or-nlc (γ1, γ2) nlc-and-nld (δ1, δ2) is the PDNF of [∨γ1γ2], for every two NLC’s γ1 and γ2 is the PCNF of [∧δ1δ2], for every two NLD’s δ1 and δ2

nlc-and-pdnf (γ, Δ) nld-or-pcnf (δ, Γ) is the PDNF of [∧γΔ], for every NLC γ and PDNF Δ is the PCNF of [∨δΓ], for every NLD δ and PCNF Γ

nlc-or-pdnf (γ, Δ) nld-and-pcnf (δ, Γ) is the PDNF of [∨γΔ], for every NLC γ and PDNF Δ is the PCNF of [∧δΓ], for every NLD δ and PCNF Γ

pdnf-and-pdnf (Δ1, Δ2) pcnf-or-pcnf (Γ1, Γ2) is the PDNF of [∧Δ1Δ2], for every two PDNF’s Δ1 and Δ2 is the PCNF of [∨Γ1Γ2], for every two PCNF’s Γ1 and Γ2

pdnf-or-pdnf (Δ1, Δ2) pcnf-and-pcnf (Γ1, Γ2) is the PDNF of [∨Δ1Δ2], for every two PDNF’s Δ1 and Δ2 is the PCNF of [∧Γ1Γ2], for every two PCNF’s Γ1 and Γ2

pdnf-conj ((Δ1, ..., Δn)) pcnf-disj ((Γ1, ..., Γn)) is the PDNF of [∧Δ1...Δn], for every list (Δ1, ..., Δn) of PDNF’s with n ≥ 0

is the PCNF of [∨Γ1...Γn], for every list (Γ1, ..., Γn) of PCNF’s with n ≥ 0

pdnf-disj ((Δ1, ..., Δn)) pcnf-conj ((Γ1, ..., Γn)) is the PDNF of [∨Δ1...Δn], for every list (Δ1, ..., Δn) of PDNF’s with n ≥ 0

is the PCNF of [∧Γ1...Γn], for every list (Γ1, ..., Γn) of PCNF’s with n ≥ 0

The PDNF system: Implementation The PCNF system: Implementation

pdnf (φ)  pcnf (φ)

:= \{ \begin{matrix}[∨[∧φ]] & if φ is an atom \\ [∨] & if φ = 0 \\ [∨[∧]] & if φ = 1 \\ [∨[∧¬α]] & if φ = ¬α and α is atom \\ [∨[∧]] & if φ = ¬0 \\ [∨] & if φ = ¬1 \\ pdnf (φ′) & if φ = ¬¬φ′ \\ pdnf-disj ((pdnf (¬φ1), ..., pdnf (¬φn))) & if φ = ¬[∧φ1...φn] \\ pdnf-conj ((pdnf (¬φ1), ..., pdnf (¬φn))) & if φ = ¬[∨φ1...φn] \\ pdnf-conj ((pdnf (φ1), ..., pdnf (φn))) & if φ = ¬[\overline{∧}φ1...φn] \\ pdnf-disj ((pdnf (φ1), ..., pdnf (φn))) & if φ = ¬[\overline{∨}φ1...φn] \\ pdnf-and-pdnf (pdnf (φ1), pdnf (¬φ2)) & if φ = ¬[φ1 → φ2] \\ pdnf-or-pdnf ( \\ pdnf-and-pdnf (pdnf (φ1), pdnf (¬φ2)), \\ pdnf-and-pdnf (pdnf (¬φ1), pdnf (φ2))) & if φ = ¬[φ1 ↔ φ2] \\ pdnf-conj (pdnf (φ1), ..., pdnf (φn)) & if φ = [∧φ1...φn] \\ pdnf-disj (pdnf (φ1), ..., pdnf (φn)) & if φ = [∨φ1...φn] \\ pdnf-disj (pdnf (¬φ1), ..., pdnf (¬φn)) & if φ = [\overline{∧}φ1...φn] \\ pdnf-conj (pdnf (¬φ1), ..., pdnf (¬φn)) & if φ = [\overline{∨}φ1...φn] \\ pdnf-or-pdnf (pdnf (¬φ1), pdnf (φ2)) & if φ = [φ1 → φ2] \\ pdnf-or-pdnf ( \\ pdnf-and-pdnf (pdnf (φ1), pdnf (φ2)), \\ pdnf-and-pdnf (pdnf (¬φ1), pdnf (¬φ2))) & if φ = [φ1 ↔ φ2] \end{matrix} := \{ \begin{matrix}[∧[∨φ]] & if φ is an atom \\ [∧[∨]] & if φ = 0 \\ [∧] & if φ = 1 \\ [∧[∨¬α]] & if φ = ¬α and α is atom \\ [∧] & if φ = ¬0 \\ [∧[∨]] & if φ = ¬1 \\ pcnf (φ′) & if φ = ¬¬φ′ \\ pcnf-disj ((pcnf (¬φ1), ..., pcnf (¬φn))) & if φ = ¬[∧φ1...φn] \\ pcnf-conj ((pcnf (¬φ1), ..., pcnf (¬φn))) & if φ = ¬[∨φ1...φn] \\ pcnf-conj ((pcnf (φ1), ..., pcnf (φn))) & if φ = ¬[\overline{∧}φ1...φn] \\ pcnf-disj ((pcnf (φ1), ..., pcnf (φn))) & if φ = ¬[\overline{∨}φ1...φn] \\ pcnf-and-pcnf (pcnf (φ1), pcnf (¬φ2)) & if φ = ¬[φ1 → φ2] \\ pcnf-or-pcnf ( \\ pcnf-and-pcnf (pcnf (φ1), pcnf (¬φ2)), \\ pcnf-and-pcnf (pcnf (¬φ1), pcnf (φ2))) & if φ = ¬[φ1 ↔ φ2] \\ pcnf-conj (pcnf (φ1), ..., pcnf (φn)) & if φ = [∧φ1...φn] \\ pcnf-disj (pcnf (φ1), ..., pcnf (φn)) & if φ = [∨φ1...φn] \\ pcnf-disj (pcnf (¬φ1), ..., pcnf (¬φn)) & if φ = [\overline{∧}φ1...φn] \\ pcnf-conj (pcnf (¬φ1), ..., pcnf (¬φn)) & if φ = [\overline{∨}φ1...φn] \\ pcnf-or-pcnf (pcnf (¬φ1), pcnf (φ2)) & if φ = [φ1 → φ2] \\ pcnf-or-pcnf ( \\ pcnf-and-pcnf (pcnf (φ1), pcnf (φ2)), \\ pcnf-and-pcnf (pcnf (¬φ1), pcnf (¬φ2))) & if φ = [φ1 ↔ φ2] \end{matrix}

nlc-and-nlc (γ1, γ2) nld-or-nld (δ1, δ2)

:= jrec (γ1, γ2, [∧])  := jrec (δ1, δ2, [∨])

nlc-or-nlc (γ1, γ2) nld-and-nld (δ1, δ2)

:= prim (γ1, γ2)  := prim (δ1, δ2)

nlc-and-pdnf (γ, [∨γ1...γn]) nld-or-pcnf (δ, [∧δ1...δn]) := pdnf-disj ((nlc-and-nlc (γ, γ1), ..., nlc-and-nlc (γ, γn))) := pcnf-conj ((nld-or-nld (δ, δ1), ..., nld-or-nld (δ, δn)))

nlc-or-pdnf (γ, Δ) nld-and-pcnf (δ, Γ)

:= prec ([∨γ], [∨], Δ, [∨])  := prec ([∧δ], [∧], Γ, [∧])

pdnf-and-pdnf ([∨γ1...γn], Δ) pcnf-or-pcnf ([∧δ1...δn], Γ) := pdnf-disj ((nlc-and-pdnf (γ1, Δ), ..., nlc-and-pdnf (γn, Δ))) := pcnf-conj ((nld-or-pcnf (δ1, Γ), ..., nld-or-pcnf (δn, Γ)))

pdnf-or-pdnf (Δ1, Δ2) pcnf-and-pcnf (Γ1, Γ2)

:= prec (Δ1, [∨], Δ2, [∨])  := prec (Γ1, [∧], Γ2, [∧])

pdnf-conj ((Δ1, ..., Δn)) pcnf-disj ((Γ1, ..., Γn))

:= \{ \begin{matrix}[∨[∧]] & if n = 0 \\ Δ1 & if n = 1 \\ pdnf-and-pdnf (Δ1, pdnf-conj ((Δ2, ..., Δn))) & if n > 1 \end{matrix} := \{ \begin{matrix}[∧[∨]] & if n = 0 \\ Γ1 & if n = 1 \\ pcnf-and-pcnf (Γ1, pcnf-disj ((Γ2, ..., Γn))) & if n > 1 \end{matrix}

pdnf-disj ((Δ1, ..., Δn)) pcnf-conj ((Γ1, ..., Γn))

:= \{ \begin{matrix}[∨] & if n = 0 \\ Δ1 & if n = 1 \\ pdnf-or-pdnf (Δ1, pdnf-disj ((Δ2, ..., Δn))) & if n > 1 \end{matrix} := \{ \begin{matrix}[∧] & if n = 0 \\ Γ1 & if n = 1 \\ pcnf-and-pcnf (Γ1, pcnf-conj ((Γ2, ..., Γn))) & if n > 1 \end{matrix}

Auxiliary algorithms

\overline{∗} := \{ \begin{matrix}∨ & if ∗ = ∧ \\ ∧ & if ∗ = ∨ \end{matrix} \} for ∗ ∈ \{∧, ∨\}

jrec ([∗λ1...λn], [∗λ′1...λ′m], [∗μ1...μk])

:= \{ \begin{matrix}[\overline{∗}[∗μ1...μkλ′1...λ′m]] & if n = 0 \\ [\overline{∗}[∗μ1...μkλ1...λn]] & if m = 0 \\ jrec ([∗λ2...λn], [∗λ′1...λ′m], [∗μ1...μkλ1]) & if n > 0 and m > 0 and |λ1| < |λ′1| \\ jrec ([∗λ1...λn], [∗λ′2...λ′m], [∗μ1...μkλ′1]) & if n > 0 and m > 0 and |λ′1| < |λ1| \\ jrec ([∗λ2...λn], [∗λ′2...λ′m], [∗μ1...μkλ1]) & if n > 0 and m > 0 and λ1 = λ′1 \\ [\overline{∗}] & if n > 0 and m > 0 and \overline{λ1} = λ′1 \end{matrix}

prec ([∗γ1...γc], [∗μ1...μn], [∗μn+1...μn+m], [∗π1...πp])

:= \{ \begin{matrix}[∗μ1...μnμn+1...μn+m] & if c = 0 and p = 0 \\ prec ([∗π1...πp], [∗], [∗μ1...μnμn+1...μn+m], [∗]) & if c = 0 and p > 0 \\ prec ([∗γ2...γcπ1...πp], [∗], [∗γ1μ1...μn], [∗]) & if c > 0 and m = 0 \\ prec ([∗γ2...γc], [∗], [∗μ1...μnμn+1...μn+m], [∗]) & if c > 0 and m > 0 and xprim (γ1, μn+1) = (“N000”, [∗μn+1]) \\ prec ([∗γ2...γcμn+2...μn+mπ1...πp], [∗], [∗γ1μ1...μn], [∗]) & if c > 0 and m > 0 and xprim (γ1, μn+1) = (“N00P”, [∗γ1]) \\ prec ([∗γ2...γc], [∗], [∗μ1...μnμn+1...μn+m], [∗]) & if c > 0 and m > 0 and xprim (γ1, μn+1) = (“N0P0”, [∗μn+1]) \\ prec ([∗γ1...γc], [∗μ1...μnμn+1], [∗μn+2...μn+m], [∗π1...πp]) & if c > 0 and m > 0 and xprim (γ1, μn+1) = (“N0PP”, [∗γ1μn+1]) \\ prec ([∗γ2...γcγ′], [∗], [∗μ1...μnμn+2...μn+m], [∗]) & if c > 0 and m > 0 and xprim (γ1, μn+1) = (“N100”, [∗γ′]) \\ prec ([∗γ2...γcμ{′ \atop n+1}μn+2...μn+mπ1...πp], [∗], [∗γ1μ1...μn], [∗]) & if c > 0 and m > 0 and xprim (γ1, μn+1) = (“N10P”, [∗γ1μ{′ \atop n+1}]) \\ prec ([∗γ2...γcγ′ 1], [∗], [∗μ1...μnμn+1...μn+m], [∗]) & if c > 0 and m > 0 and xprim (γ1, μn+1) = (“N1P0”, [∗γ′ 1μn+1]) \\ prec ([∗γ1...γc], [∗μ1...μnμn+1], [∗μn+2...μn+m], [∗ππ1...πp]) & if c > 0 and m > 0 and xprim (γ1, μn+1) = (“N1PP”, [∗γ1μn+1π]) \\ prec ([∗γ1...γc], [∗μ1...μnμn+1], [∗μn+2...μn+m], [∗π1...πp]) & if c > 0 and m > 0 and xprim (γ1, μn+1) = (“NMNN”, [∗γ1μn+1]) \end{matrix}

prim ([∗λ1...λx], [∗λ′1...λ′y])

:= Φ, where Φ is defined by (ξ, Φ) := xprim ([∗λ1...λx], [∗λ′1...λ′y])

xprim ([∗λ1...λx], [∗λ′1...λ′y])

:= xprec ([∗], [∗λ1...λx], [∗], [∗λ′1...λ′y], [∗], [∗], [∗], 0, 0, 0)

algorithm xprec ([∗λ1...λi], [∗λi+1...λx], [∗λ′1...λ′j], [∗λ{′ \atop j+1}...λ′y], [∗π1...πa], [∗π′1...π′b], [∗π{′′ \atop 1}...π{′′ \atop c}], r, s, t)

begin

if r > 1

then (“NMNN”, [\overline{∗}[∗λ1...λiλi+1...λx][∗λ′1...λ′j λ{′ \atop j+1}...λ′y]])

else if x = i

then if r = 0

then if s = 0

then if (j = y and t = 0)

then (“N000”, [\overline{∗}[∗λ1...λi]])

else (“N00P”, [\overline{∗}[∗λ1...λi]])

else if (j = y and t = 0)

then (“N0P0”, [\overline{∗}[∗λ′1...λ′j]])

else (“N0PP”, [\overline{∗}[∗λ1...λi][∗λ′1...λ′j λ{′ \atop j+1}...λ′y]])

else if s = 0

then if (j = y and t = 0)

then (“N100”, [\overline{∗}[∗π1...πa]])

else (“N10P”, [\overline{∗}[∗λ1...λi][∗π′1...π′bλ{′ \atop j+1}...λ′y]])

else if (j = y and t = 0)

then (“N1P0”, [\overline{∗}[∗π1...πa][∗λ′1...λ′j λ{′ \atop j+1}...λ′y]])

else (“N1PP”, [\overline{∗}[∗λ1...λi][∗λ′1...λ′j λ{′ \atop j+1}...λ′y][∗π{′′ \atop 1}...π{′′ \atop c}λ{′ \atop j+1}...λ′y]])

else if j = y

then if r = 0

then if t = 0

then (“N0P0”, [\overline{∗}[∗λ′1...λ′j]])

else (“N0PP”, [\overline{∗}[∗λ1...λiλi+1..λx][∗λ′1...λ′j]])

else if t = 0

then (“N1P0”, [\overline{∗}[∗π1...πaλi+1...λx][∗λ′1...λ′j]])

else (“N1PP”, [\overline{∗}[∗λ1...λiλi+1...λx][∗λ′1...λ′j][∗π{′′ \atop 1}...π{′′ \atop c}λi+1...λx]])

else if |λi+1| < |λ{′ \atop j+1}|

then xprec ([∗λ1...λiλi+1], [∗λi+2...λx], [∗λ′1...λ′j], [∗λ{′ \atop j+1}...λ′y], [∗π1...πaλi+1], [∗π′1...π′b], [∗π{′′ \atop 1}...π{′′ \atop c}λi+1], r, s + 1, t)

else if |λ{′ \atop j+1}| < |λi+1|

then xprec ([∗λ1...λi], [∗λi+1...λx], [∗λ′1...λ′j λ{′ \atop j+1}], [∗λ{′ \atop j+2}...λ′y], [∗π1...πa], [∗π′1...π′bλ{′ \atop j+1}], [∗π{′′ \atop 1}...π{′′ \atop c}λ{′ \atop j+1}], r, s, t + 1)

else if λi+1 = λj+1

then xprec ([∗λ1...λiλi+1], [∗λi+2...λx], [∗λ′1...λ′j λ{′ \atop j+1}], [∗λ{′ \atop j+2}...λ′y], [∗π1...πaλi+1], [∗π′1...π′bλ{′ \atop j+1}], [∗π{′′ \atop 1}...π{′′ \atop c}λ{′ \atop j+1}], r, s, t)

else xprec ([∗λ1...λi], [∗λi+2...λx], [∗λ′1...λ′j], [∗λ{′ \atop j+2}...λ′y], [∗π1...πa], [∗π′1...π′b], [∗π{′′ \atop 1}...π{′′ \atop c}], r + 1, s, t)

end.