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]#

Bases: Generic[α, τ, χ, σ]

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.

dnf(f: Formula[α, τ, χ, σ]) Formula[α, τ, χ, σ][source]#

Compute a disjunctive normal form. If f contains quantifiers, then the result is a prenex normal form whose matrix is in DNF.

abstract simplify(f: Formula[α, τ, χ, σ]) Formula[α, τ, χ, σ][source]#

Compute a simplified equivalent of f.