Abstract Base Classes

Simplification#

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.simplify provides a generic abstract implementation of deep simplifcication based on generating and propagating internal representations during recursion. This is essentially the standard simplifier, which has been proposed for Ordered Fields in [DolzmannSturm-1997].

Generic Types#

We use type variables simplify.α, simplify.τ, simplify.χ, simplify.σ in anology to their counterparts in formula.

logic1.abc.simplify.α = TypeVar('α', bound='AtomicFormula')#

logic1.abc.simplify.τ = TypeVar('τ', bound='Term')#

logic1.abc.simplify.χ = TypeVar('χ', bound='Variable')#

logic1.abc.simplify.σ = TypeVar('σ')#

Additionally, we introduce a type variable ρ for internal representations used by the simplifier.

logic1.abc.simplify.ρ = TypeVar('ρ', bound='InternalRepresentation')#: A type variable denoting a type of variables with upper bound logic1.abc.simplify.InternalRepresentation.

Internal Representations#

class logic1.abc.simplify.InternalRepresentation[source]#

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

This abstract class serves as an upper bound for the type variable ρ in abc.simplify.Simplify. It specifies an interface comprising methods required there.

The principal idea is that a InternalRepresentation should hold two abstract pieces of information, reference and current. Both reference and current hold information that is equivalent to a conjunction of atomic formulas. In the course of recursive simplification in abc.simplify.Simplify, reference is inherited from above; current starts with the information from reference and is enriched with information from all atomic formulas on the toplevel of the subformula currently under consideration.

abstract add(gand: type[And[α, τ, χ, σ] | Or[α, τ, χ, σ]], atoms: Iterable[α]) → Restart[source]#: Add current information originating from atoms. If gand is And, consider atoms. If gand is Or, consider (Not(at) for at in atoms). This is where simplification is supposed to take place.

abstract extract(gand: type[And[α, τ, χ, σ] | Or[α, τ, χ, σ]]) → Iterable[α][source]#: Comapare current and reference to identify and extract information that must be represented on the toplevel of the subformula currently under consideration. If gand is And, the result represents a conjunction. If gand is Or, it represents a disjunction.

abstract next_(remove: χ | None = None) → Self[source]#: Copy current to reference, removing all information involving the variable remove. If not None, the variable remove is quantified in the current recursion step.

Simplification and Validity#

class logic1.abc.simplify.Simplify[source]#

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

Deep simplification following [DolzmannSturm-1997].

Simplification

Contents

Simplification#

Generic Types#

Internal Representations#

Simplification and Validity#