tangles.util.logic.term#
A logcial term made up of “conjunctions of clauses which themselves are disjunctions of literals” is said to be in
Conjuctive Normal Form (CNF),
i.e. (A or not B or C) and (B or not C).
On the other hand a disjunction of conjunctions is said to be in
Disjunctive Normal Form (DNF),
i.e. (A and B) or C or (not A).
We encode both of these forms in matrices. Each row represents one of the variables, each column one of the clauses. Thus (A or not B or C) and (B or not C) would be encoded as
( 1 0)
(-1 1)
( 1 -1)
On the other hand (A and B) or C or (not A) would be encoded as
(1 0 -1)
(1 0 0)
(0 1 0)
As you can see, it is not possible from the matrix to tell which of these two normal forms the matrices are in.
Classes