Justification

class Assumption(**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 assumption.

dependency_type: Literal[JustificationType.ASSUMPTION]

model_config: ClassVar[ConfigDict] = {}

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

class NumericalCheck(**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 numerical check.

dependency_type: Literal[JustificationType.NUMERICAL_CHECK]

model_config: ClassVar[ConfigDict] = {}

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

class Reflexivity(**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 trivially true by reflexivity.

dependency_type: Literal[JustificationType.REFLEXIVITY]

model_config: ClassVar[ConfigDict] = {}

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

class DirectConsequence(**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 direct consequences.

model_config: ClassVar[ConfigDict] = {}

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

premises: tuple[Predicate, ...]

The premises of the direct consequences.

dependency_type: Literal[JustificationType.DIRECT_CONSEQUENCE]

justify_dependency(dep, proof_state)

Return type:

tuple[Circumcenter | Cong | Coll | NColl | Cyclic | ConstantAngle | ACompute | LCompute | ConstantLength | ConstantRatio | EqAngle | Diff | RCompute | ObtuseAngle | MidPoint | EqRatio | Perp | NPerp | Para | NPara | SameClock | SameSide | NSameSide | PythagoreanPremises | PythagoreanConclusions | SquaredConstantLength | SquaredConstantRatio | SimtriClock | SimtriReflect | ContriClock | ContriReflect | AngleEquation | LengthEquation, ...]