Sets with Cardinality Constraints

Boolean Normal Forms

logic1.theories.Sets.bnf.cnf(f: Formula) → Formula

logic1.theories.Sets.bnf.dnf(f: Formula) → Formula

Compute a conjunctive or disjunctive normal form of f. If f contains quantifiers, then the result is an equivalent prenex normal form whose matrix is in CNF or DNF, respectively.

Some examples

>>> from logic1 import *
>>> from logic1.theories.Sets import *
>>> a, b, c, d = VV.get('a', 'b', 'c', 'd')

>>> f = Equivalent(a == d, b == d)
>>> cnf(f)
And(Or(a == b, a != d), Or(a == b, b != d))
>>> dnf(f)
Or(a == b, And(a != d, b != d))

>>> f = And(Or(a == d, b != d), Or(a != d, b == d))
>>> cnf(f)
And(Or(a == b, a != d), Or(a == b, b != d))
>>> dnf(f)
Or(a == b, And(a != d, b != d))

>>> f = And(Or(a != d, b == d), Or(a == d, b == d))
>>> cnf(f)
And(Or(a == b, a != d), Or(a == d, b == d))
>>> dnf(f)
Or(And(a == b, a == d), And(b == d, a != b))

See also

BooleanNormalForm

Its inherited methods BooleanNormalForm.cnf() and BooleanNormalForm.dnf() are wrapped by the functions cnf() and dnf(), respectively.

Simplification

for the simplifier that is used to simplify intermediate results throughout the CNF and DNF computation.

Details

Attention

The material below addresses implementers rather than users.

class logic1.theories.Sets.bnf.BooleanNormalForm

Bases: BooleanNormalForm[AtomicFormula, Variable, Variable, Never]

Implements the abstract method simplify of its super class abc.bnf.BooleanNormalForm. In addition, this class inherits cnf and dnf, which should be called via cnf() and dnf() as described below, respectively.