Abstract Base Classes
Boolean Normal Forms#
Attention
This documentation page addresses implementers rather than users. Concrete implemtations of the abstract classes described here are documented in the corresponding sections of the various domains:
This module logic1.abc.bnf provides a generic abstract implementation
of boolean normal form computations using the famous Espresso algorithm in
combination with boolean abstraction. Techincally, we use the python package
PyEDA, which in turns
wraps a C extension
of the famous Berkeley Espresso library [BraytonEtAl-1984].
Generic Types#
We use type variables bnf.α, bnf.τ, bnf.χ,
bnf.σ in anology to their counterparts in formula.
- logic1.abc.bnf.α = TypeVar('α', bound='AtomicFormula')#
- logic1.abc.bnf.τ = TypeVar('τ', bound='Term')#
- logic1.abc.bnf.χ = TypeVar('χ', bound='Variable')#
- logic1.abc.bnf.σ = TypeVar('σ')#
Boolean Normal Forms#
- class logic1.abc.bnf.BooleanNormalForm[source]#
-
Boolean normal form computation.
- cnf(f: Formula[α, τ, χ, σ]) Formula[α, τ, χ, σ][source]#
Compute a conjunctive normal form. If f contains quantifiers, then the result is a prenex normal form whose matrix is in CNF.