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

## Abstract

A literal conjunction γ = [λ1 ∧ ... ∧ λk] is a prime factor of a disjunctive normal form (DNF) Δ =[[λ1,1 ∧ ... ∧ λ1,m1] ∨ ... ∨ [λn,1 ∧ ... ∧ λn,mn]] iff γ ⇒ Δ and none of the λ1,...,λk 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 potential 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.

## The text PNFCanon.pdf (333 KB) PNFCanon.ps (495 KB) PNFCanon.dvi (227 KB)

first version May 1999, revised version September 2002, 36 pages

## Remarks

• The blog entry A fast SAT solver provides a brief sketch of the main idea behind the algorithms.
• This revised version basically corrects a number of errors without changing the character of the original version. The changes are documented on the four print pages of errata.(pdf|ps|dvi). The original version is available as PNFCanon1.(pdf|ps|dvi).
• In more recent works I replaced the term "sentential logic" by its synonym "propositional logic".

## Bugs

• Section 11 proofs the Completeness Theorem and defines the `P-Procedure`, Section 12 merges the loop of the `P-Procedure` into a recursive function `prec`.
The Haskell implementation of `prec` (see PropLogic) produced (correct) results in all tests, except when fed with the I-Form
`[[-1,2,3,4], [1,-3,4], [-1,-2,-3,-4], [1,-2,3,4], [3,4], [-1,3,-4], [1,-3,-4]]`
in which case the procedure didn't terminate. In terms of Section 12 that would mean that `prec(Δ,[∨],[∨],[∨])` might not terminate if `Δ` is
`[[¬a∧b∧c∧d] ∨ [a∧¬c∧d] ∨ [¬a∧¬b∧¬c∧¬d] ∨ [a∧¬b∧c∧d] ∨ [c∧d] ∨ [¬a∧c∧¬d] ∨ [a∧¬c∧¬d]]`
The Haskell `PropLogic` package therefore uses the original `P-Procedure` in its current version `0.9`.
At the moment, I cannot see where the error is hidden.