Proof Data

Define the proof data outputed by Newclid then used to write and display the proof.

class PredicateInProof(**data)

Bases: BaseModel

A predicate in the proof with its unique id.

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.

id: ProofId

predicate: Predicate

model_config: ClassVar[ConfigDict] = {}

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

class ProofStep(**data)

Bases: BaseModel

A deduction step of the proof.

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.

proven_predicate: PredicateInProof

justification: Justification

applied_on_predicates: tuple[ProofId, ...]

model_config: ClassVar[ConfigDict] = {}

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

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

proof_length: int

Total length of the proof.

proof_rules_length: int

Number of rule applications in the proof.

points: list[Point]

Points in the initial problem setup.

proven_goals: list[PredicateInProof]

Predicate in proof of goals that were proved.

unproven_goals: list[Predicate]

Goals to prove from the initial problem that were not proved.

construction_assumptions: list[PredicateInProof]

Assumptions made initialy by construction.

model_config: ClassVar[ConfigDict] = {}

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

numerical_checks: list[PredicateInProof]

Assumptions made by numerical checks.

trivial_predicates: list[PredicateInProof]

Predicates that are considered trivialy true within the proof.

proof_steps: list[ProofStep]

Proof steps.

set_proof_length()

Return type:

Self

proof_data_from_state(goals_constructions, proof_state)

Return type:

ProofData

proof_justifications_to_proof_data(proof_justifications, proof_state, goal_is_proven)

Return type:

ProofData