Sets
Boolean Normal Forms#
- class logic1.theories.Sets.bnf.BooleanNormalForm[source]#
Bases:
BooleanNormalForm
[AtomicFormula
,Variable
,Variable
,Never
]Implements the abstract method
simplify
of its super classabc.bnf.BooleanNormalForm
. In addition, this class inheritscnf
anddnf
, which should be called viacnf()
anddnf()
as described below, respectively.
User Interface#
- logic1.theories.Sets.bnf.cnf(f: Formula) Formula #
- logic1.theories.Sets.bnf.dnf(f: Formula) Formula #
Compute a conjunctive or disjunctive normal form, respectively.
- Parameters:
f – The input formula
- Returns:
Returns a CNF or DNF of f, respectively. If f contains quantifiers, then the result is an equivalent prenex normal form whose matrix is in CND 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))