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.