bucephalus.org

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

Abstract

A literal conjunction γ = [λ₁ ∧ ... ∧ λ_k] is a prime factor of a disjunctive normal form (DNF) Δ =[[λ_1,1 ∧ ... ∧ λ_1,m1] ∨ ... ∨ [λ_n,1 ∧ ... ∧ λ_n,mn]] iff γ ⇒ Δ and none of the λ₁,...,λ_k could be deleted without violating γ ⇒ Δ. A DNF Δ=[γ₁ ∨ ... ∨ γ_n] is a prime DNF (PDNF) iff {γ₁,...,γ_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)

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.

[home] [blog]