Creates a new Hilbert proof with a goal formula.
The target formula to prove
Gets the number of steps in the proof.
The current step count
Gets a specific step by index (1-based).
The step number (1-based)
The proof step, or undefined if not found
Adds a premise (given assumption) to the proof.
The premise formula
Optionalcomment: stringOptional explanation for the premise
The added proof step
Adds an axiom step to the proof.
The axiom payload containing formulas and schema
Optionalcomment: stringOptional explanation for the axiom
The added proof step
Adds a derived step to the proof using a Hilbert calculus rule.
The derived step payload containing formulas, schema, and step references
Optionalcomment: stringOptional explanation for the derivation
The added proof step
Checks if the proof is complete (last step matches the goal).
True if the last step's formula matches the goal
Gets the last step in the proof (which should be the goal).
The final proof step, or undefined if no steps exist
Reiterates (repeats) a previously proved step. Allows referring to a formula from an earlier step in the proof.
The index of the step to reiterate (1-based)
Optionalcomment: stringOptional explanation for the reiteration
The added reiteration step
Clears all steps from the proof.
Represents a complete proof in Hilbert-style calculus. Manages a sequence of proof steps where the final step is the goal formula. Each step can be an axiom, premise, or derived from previous steps.