Class HilbertProofBuilder

A builder class for constructing Hilbert-style proofs. Provides a chainable API for adding proof steps.

Example

const proof = new HilbertProofBuilder(implicationAB)
	.addPremise(A, "First premise")
	.addPremise(B, "Second premise")
	.build();

Index

Constructors

constructor

Methods

addPremise addAxiom addDerivedStep reiterateStep replace build buildSteps preview

Constructors

constructor

new HilbertProofBuilder(goal: PropFormula): HilbertProofBuilder
Creates a new proof builder with a goal formula.
Parameters
- goal: PropFormula
  The target formula to prove
Returns HilbertProofBuilder
- Defined in propositional/hilbert-calculus/classes/hilbert-proof-builder.ts:30

Methods

addPremise

addPremise(formula: PropFormula, comment?: string): this
Adds a premise (given assumption) to the proof.
Parameters
- formula: PropFormula
  The premise formula
- Optionalcomment: string
  Optional explanation for the premise
Returns this
This builder instance for chaining
- Defined in propositional/hilbert-calculus/classes/hilbert-proof-builder.ts:40

addAxiom

addAxiom(payload: HilbertAxiomPayload, comment?: string): this
Adds an axiom step to the proof.
Parameters
- payload: HilbertAxiomPayload
  The axiom payload containing formulas and schema
- Optionalcomment: string
  Optional explanation for the axiom
Returns this
This builder instance for chaining
- Defined in propositional/hilbert-calculus/classes/hilbert-proof-builder.ts:51

addDerivedStep

addDerivedStep(payload: HilbertDerivedPayload, comment?: string): this
Adds a derived step to the proof using a Hilbert calculus rule.
Parameters
- payload: HilbertDerivedPayload
  The derived step payload containing formulas, schema, and step references
- Optionalcomment: string
  Optional explanation for the derivation
Returns this
This builder instance for chaining
- Defined in propositional/hilbert-calculus/classes/hilbert-proof-builder.ts:62

reiterateStep

reiterateStep(fromIndex: number, comment?: string): this
Reiterates (repeats) a previously proved step. Allows referring to a formula from an earlier step in the 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
- Defined in propositional/hilbert-calculus/classes/hilbert-proof-builder.ts:74

replace

replace(atom: PropAtom, substitute: PropAtom | PropFormula): this
Replaces all occurrences of an atom with a formula or atom in all proof steps. The goal formula is not modified.
Parameters
- atom: PropAtom
  The atomic proposition to replace
- substitute: PropAtom | PropFormula
  The formula or atom to substitute
Returns this
This builder instance for chaining
- Defined in propositional/hilbert-calculus/classes/hilbert-proof-builder.ts:87

build

build(): HilbertProof
Constructs the proof and returns it.

Returns HilbertProof
The completed HilbertProof instance
- Defined in propositional/hilbert-calculus/classes/hilbert-proof-builder.ts:96

buildSteps

buildSteps(stepsFn: (builder: this) => void): this
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
Example
```
proof.buildSteps((builder) => {
  builder.addPremise(p);
  builder.addAxiom(axiom1);
  builder.addDerivedStep(derived1);
});
```
- Defined in propositional/hilbert-calculus/classes/hilbert-proof-builder.ts:116

preview

preview(): HilbertProof
Gets the current state of the proof without building. Useful for inspection during construction.

Returns HilbertProof
The current HilbertProof instance
- Defined in propositional/hilbert-calculus/classes/hilbert-proof-builder.ts:126

Class HilbertProofBuilder

Example

Index

Constructors

Methods

Constructors

constructor

Parameters

Returns HilbertProofBuilder

Methods

addPremise

Parameters

Returns this

addAxiom

Parameters

Returns this

addDerivedStep

Parameters

Returns this

reiterateStep

Parameters

Returns this

replace

Parameters

Returns this

build

Returns HilbertProof

buildSteps

Parameters

Returns this

Example

preview

Returns HilbertProof

Settings

On This Page