Embedded Systems Group (ES)

Propositional Logic Tools

Using this tool, various computations can be performed for given propositional logic formulas.

truth table
CCNF (canonical conjunctive normal form)
CDNF (canonical disjunctive normal form)
SNF (Shannon normal form)
RMNF (Reed-Muller normal form)
FDD (functional decision diagram)
ZDD (zero-suppressed binary decision diagram)
BDD (binary decision diagram)
Shannon graph
sequent calculus proof tree
linear equi-satisfiable clause set
SAT solver (DPLL with non-chronological backtracking aka clause learning)

remark: This is false for N≤3 and true for N>3.