Creates a new proof builder with a goal formula.
The target formula to prove
Adds a premise (given assumption) to the proof at the current level.
The premise formula
Optionalcomment: stringOptional explanation for the premise
This builder instance for chaining
Adds an assumption to open a sub-proof. This increases the nesting level and starts a new sub-proof.
The assumption formula
Optionalcomment: stringOptional explanation for the assumption
This builder instance for chaining
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
This builder instance for chaining
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
This builder instance for chaining
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
This builder instance for chaining
Adds multiple steps in sequence using a callback function. Useful for building complex proofs programmatically.
A callback that receives the current builder and adds steps
This builder instance for chaining
Gets the current state of the proof without building. Useful for inspection during construction.
The current NaturalProof instance
A builder class for constructing Natural Deduction style proofs. Provides a chainable API for adding proof steps including premises, assumptions (sub-proofs), derived steps, and sub-proof closures.
Example