Creates a new Natural Deduction 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
Gets the current nesting level for sub-proofs.
The current level (0 = main proof, > 0 = inside assumption)
Adds a premise (given assumption) to the proof at the current level.
The premise formula
Optionalcomment: stringOptional explanation for the premise
The added proof step
Adds an assumption (opens a sub-proof) at the next level. Creates a new assumption that increases the nesting level.
The assumption formula
Optionalcomment: stringOptional explanation for the assumption
The added proof step
Adds a derived step using a Natural Deduction rule. Can be used to apply rules within the current level (including sub-proofs).
The derived step payload containing formulas, rule, and step references
Optionalcomment: stringOptional explanation for the derivation
The array of added proof steps
Reiterates (repeats) a previously proved step at the current level (inside a sub-proof). Allows referring to a formula from an outer level within an inner sub-proof.
The index of the step to reiterate (1-based)
Optionalcomment: stringOptional explanation for the reiteration
The added reiteration step
Closes a sub-proof by applying Implication Introduction. Automatically takes the assumption (most recent step at current level) and the derived conclusion (last step at current level) to create an implication F=>G, then adds this implication at level-1.
Optionalcomment: stringOptional explanation for the implication closure
The added proof step
Gets the last step in the proof.
The final proof step, or undefined if no steps exist
Checks if the proof is complete. A proof is complete when:
True if the proof is complete
Clears all steps from the proof and resets the level to 0.
Represents a complete proof in Natural Deduction style calculus. Manages a sequence of proof steps where the final step is the goal formula. Supports premises, assumptions (sub-proofs), and derived steps using natural deduction rules. Tracks nesting levels to manage sub-proofs and ensures proofs are properly closed at level 0.