Deductor Interface

class ARCoefficient(**data)

Bases: BaseModel

A premise of an AR deduction.

Create a new model by parsing and validating input data from keyword arguments.

Raises [ValidationError][pydantic_core.ValidationError] if the input data cannot be validated to form a valid model.

self is explicitly positional-only to allow self as a field name.

coeff: Fraction

The coefficient with which the predicate is multiplied to get the final equation for the wanted predicate.

lhs_terms: dict[str, Fraction]

The left-hand side terms of the equation in the table.

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

class ARPremise(**data)

Bases: BaseModel

A premise of an AR deduction.

Create a new model by parsing and validating input data from keyword arguments.

Raises [ValidationError][pydantic_core.ValidationError] if the input data cannot be validated to form a valid model.

self is explicitly positional-only to allow self as a field name.

predicate: Predicate

The predicate construction of the premise.

coefficient: ARCoefficient

The coefficient of the premise.

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

class ARDeduction(**data)

Bases: BaseModel

Create a new model by parsing and validating input data from keyword arguments.

Raises [ValidationError][pydantic_core.ValidationError] if the input data cannot be validated to form a valid model.

self is explicitly positional-only to allow self as a field name.

predicate: Predicate

The predicate justified by the AR deduction.

ar_reason: ARReason

The reason for the AR deduction.

ar_premises: tuple[ARPremise, ...] | None

The AR premises of the AR deduction.

dependency_type: Literal[JustificationType.AR_DEDUCTION]

canonicalize()

Return type:

Self

model_config: ClassVar[ConfigDict] = {}

Configuration for the model, should be a dictionary conforming to [ConfigDict][pydantic.config.ConfigDict].

class Deductor

Bases: ABC

abstractmethod deduce(symbols_registry)

Deduce dependencies o new predicates from the current dependency graph.

Return type:

Iterator[Assumption | NumericalCheck | RuleApplication | ARDeduction | CircleMerge | LineMerge | DirectConsequence | Reflexivity]

abstractmethod add_dependency(dependency, symbols_registry)

Add a predicate to the deductor.

Return type:

None

abstractmethod check_predicate(predicate, symbols_registry)

Check if a predicate is valid for the deductor.

Return type:

bool

abstractmethod justify_predicate(predicate, symbols_registry)

Justify a predicate with a dependency.

Return type:

Union[Assumption, NumericalCheck, RuleApplication, ARDeduction, CircleMerge, LineMerge, DirectConsequence, Reflexivity, None]

add_to_deductors(dependency, deductors, symbols_registry)

Return type:

None

check_from_deductors(predicate, deductors, symbols_registry)

Return type:

bool

justify_from_deductors(predicate, deductors, symbols_registry)

Return type:

Union[Assumption, NumericalCheck, RuleApplication, ARDeduction, CircleMerge, LineMerge, DirectConsequence, Reflexivity, None]