Real Closed Fields

Boolean Normal Forms

Boolean normal forms are computed by applying the normal form algorithms provided by PyEDA to Boolean abstractions of the formulas. The results are then converted back to formulas.

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

logic1.theories.RCF.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.RCF import *
>>> a, b, c = VV.get('a', 'b', 'c')

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

>>> f = And(Or(a > 0, b == 0), Or(a <= 0, b == 0))
>>> cnf(f)
b == 0
>>> dnf(f)
b == 0

>>> f = Ex([a, b], All([c], Equivalent(c == 0, And(a == 0, b == 0))))
>>> cnf(f)
Ex(a, Ex(b, All(c, And(Or(c == 0, b != 0, a != 0),
                       Or(c != 0, b == 0),
                       Or(c != 0, a == 0)))))
>>> dnf(f)
Ex(a, Ex(b, All(c, Or(And(c == 0, b == 0, a == 0),
                      And(c != 0, b != 0),
                      And(c != 0, a != 0)))))

>>> f = Equivalent(Ex([a, b], And(a == 0, b == 0)),
...                All(c, And(a == 0, c == 0)))
>>> dnf(f)
Ex(G0001_c, Ex(G0002_a, Ex(G0001_b, All(G0001_a, All(b, All(c,
    Or(And(c == 0, a == 0, G0002_a == 0, G0001_b == 0),
       And(c == 0, a == 0, G0001_c != 0),
       And(b != 0, a != 0),
       And(b != 0, G0002_a == 0, G0001_b == 0),
       And(b != 0, G0001_c != 0),
       And(a != 0, G0001_a != 0),
       And(G0002_a == 0, G0001_b == 0, G0001_a != 0),
       And(G0001_c != 0, G0001_a != 0))))))))
>>> cnf(f)
All(G0003_a, All(b, All(c, Ex(G0002_c, Ex(G0004_a, Ex(G0002_b,
    And(Or(c == 0, b != 0, G0003_a != 0),
        Or(b != 0, a == 0, G0003_a != 0),
        Or(a != 0, G0004_a == 0, G0002_c != 0),
        Or(a != 0, G0002_c != 0, G0002_b == 0))))))))

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.RCF.bnf.BooleanNormalForm

Bases: BooleanNormalForm[AtomicFormula, Term, Variable, int]

Implements the abstract methods simplify and final_simplify of its super class abc.bnf.BooleanNormalForm. Inherits the methods cnf and dnf, which should be called via the functions cnf() and dnf(), respectively.