Chop Logic Core - v1.6.0
    Preparing search index...

    Class NaturalProofBuilder

    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.

    const proof = new NaturalProofBuilder(implicationAB)
    .addPremise(A, "First premise")
    .addAssumption(B, "Assume B")
    .closeSubProof()
    .build();
    Index

    Constructors

    Methods

    • 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.

      Parameters

      • Optionalcomment: string

        Optional explanation for the implication closure

      Returns this

      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.

      Parameters

      • fromIndex: number

        The index of the step to reiterate (1-based)

      • Optionalcomment: string

        Optional explanation for the reiteration

      Returns this

      This builder instance for chaining

    • Adds multiple steps in sequence using a callback function. Useful for building complex proofs programmatically.

      Parameters

      • stepsFn: (builder: this) => void

        A callback that receives the current builder and adds steps

      Returns this

      This builder instance for chaining

      proof.buildSteps((builder) => {
      builder.addPremise(p);
      builder.addAssumption(q);
      builder.addDerivedStep(derived1);
      builder.closeSubProof();
      });