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


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



[home] [blog]