CNF.js

NOT WORKING, WORK IN PROGRESS.

Convert propositional formula trees into Conjunctive Normal Form (CNF). Might also convert predicate formulae to CNF as well.

const CNF = require('@lancejpollard/cnf.js')

CNF.convert()

Data Structure

There are 2 main types, which are all subtypes of formula: variable, and connective. There are 3 types of connective: negation, disjunction and conjunction.

Variable

Such as X.

{
  type: 'variable',
  name: string,
  value: boolean,
}

Negation

Such as ¬X.

{
  type: 'negation',
  formula: formula
}

Disjunction

Such as (A ∨ B).

{
  type: 'disjunction',
  base: formula,
  head: formula,
}

Conjunction

Such as (A ∧ B).

{
  type: 'conjunction',
  base: formula,
  head: formula,
}

Equivalencies

Every propositional formula can be converted into an equivalent formula that is in CNF. This transformation is based on rules about logical equivalences: double negation elimination, De Morgan's laws, and the distributive law.

Equivalency	Name
p∧⊤≡p p∨⊥≡p	Identity laws
p∨⊤≡⊤ p∧⊥≡⊥	Domination laws
p∨p≡p p∧p≡p	Idempotent or tautology laws
¬(¬p)≡p	Double negation law
p∨q≡q∨p p∧q≡q∧p	Commutative laws
(p∨q)∨r≡p∨(q∨r) (p∧q)∧r≡p∧(q∧r)	Associative laws
p∨(q∧r)≡(p∨q)∧(p∨r) p∧(q∨r)≡(p∧q)∨(p∧r)	Distributive laws
¬(p∧q)≡¬p∨¬q ¬(p∨q)≡¬p∧¬q	De Morgan's laws
p∨(p∧q)≡p p∧(p∨q)≡p	Absorption laws
p∨¬p≡⊤ p∧¬p≡⊥	Negation laws

lancejpollard/cnf.js