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.
PNFCanon.pdf (333 KB) | |
PNFCanon.ps (495 KB) | |
PNFCanon.dvi (227 KB) |
P-Procedure
, Section 12 merges the loop of the P-Procedure
into a recursive function prec
.
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
.