Changes made in “Theory and implementation of efficient canonical systems for sentential calculus,

based on Prime Normal Forms”

www.bucephalus.org

September 5, 2002

1 Update from the first version May 1999 to the revised version from September 2002

1.1 Significant changes of the content

On page 5 the following footnote was added:

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.

A footnote on page 15 claimed:

... I conjecture that the MDNF is always at least half as long as the PDNF.

In the revised edition the following remark has been added:

[Comment September 2002: Actually, this conjecture is not correct in general.]

1.2 Corrections of errors

Some spelling and interpunction mistakes have been corrected, but most of them are not worth mentioning because the context makes the correct or intended version obvious. However, there have also been some nasty and misleading mistakes:

• page 12, left column, second line of the first definition:

(disjunctive) functor or implicand

has to be replaced by (disjunctive) factor or implicand • page 15, right column, the example formula of the proof:

Δ′ = [∨[∧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}C]]

is now

Δ′ = [∨[∧\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]]

• page 17, first footnote:

or “f–complete” to be precise; see below.

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

• page 18, right column of the table:

                       pcnf-cov-cnf(Γ_{1},Γ_{2})

must be

                       pcnf-sub-cnf(Γ_{1},Γ_{2})

• page 18, last line of the table, both left and right column:

the left side

                     := dnf-cov-pdnf(Δ_{1},Δ_{2})

must be

                      := dnf-cov-dnf(Δ_{1},Δ_{2})

and the right side

                      := pcnf-cov-cnf(Γ_{1},Γ_{2})

must be

                      := cnf-cov-cnf(Γ_{1},Γ_{2})

• page 20 and at more places later in the text: The undefined symbol

ˆ∧

suddenly occurs. Of course it stands for the symbol

˙∧

as defined on page 19.

• page 22, second last line of the algorithm: the line

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

must be replaced by

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

• page 24, left column, third line from below:

the phrase

When we continue and if we reach Δ = [∨], we put ...

must be When we continue and if we reach Δ_{2} = [∨], we put ...

• page 25, right column, below:

The block inside the parentheses contains two occurences of the expression

vol(Δ′_{0} ∨ Δ′_{1} ∨ Δ′_{2}) = vol(Δ_{0} ∨ Δ_{1} ∨ Δ_{2})

and lg(Δ′_{0}) < lg(Δ_{0})

One of this double occurence can be deleted.

• page 26, the little table:

The three occurences of

lg(Δ_{2}^{i})

in the right column of the table must be replaced by

lg(Δ_{2}^{i}) − 1

• page 29, left column, proof of lemma 2:

The layout of the proof has changed. But in particular the line

γ′_{c} := [ˆ∧π_{1} … π_{p}σ_{1} … σ_{s}τ_{1} … τ_{t}] is the prime factor

should be

γ′_{c} := [ ˙∧π_{1} … π_{p}σ_{1} … σ_{s}τ_{1} … τ_{t}] is the c–prime factor

• page 30, right column, Proof (Termination of the P–Procedure), line 5

and 6 of this proof:

... and so At(Δ^{1}) ⊆ At(Δ^{i}) ...

should be

... and so At(Δ^{i}) ⊆ At(Δ) ...

• page 31, the picture:

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

is wrong and should be

Δ

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

• page 36:

The algorithm xprec contains some mistakes. It must be identical with the one on page 21.

1.3 References inside the text

Unfortunately, the definitions, lemmata and theorems were not numbered and I forgot to fill in some of the references.

• page 12, left column, line 14:

theorem ...

is now replaced by a theorem in chapter 3

• page 14, left column, second item (bullet) of the proof:

DNF’s are 0-canonic according to theorem ... and as such MCNF’s are 0-canonic.

is now replaced by

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

(note also the change from the wrong “MCNF” to the correct “MDNF”)

• page 21, the first block (Declarations) of the table: the four occurences of

the phrase

table ...

are replaced by the table in chapter 7