Skip to content

Convert Proposition Trees to Conjunctive Normal Form (CNF) or Disjunctive Normal Form (DNF)

Notifications You must be signed in to change notification settings

lancejpollard/cnf.js

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

4 Commits
 
 
 
 

Repository files navigation

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

HT

About

Convert Proposition Trees to Conjunctive Normal Form (CNF) or Disjunctive Normal Form (DNF)

Topics

Resources

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published