Constructor
A conclusion is a single Formula.
The actual lines of the proof.
The list of premises of the proof.
Add a LineOfProof to the proof.
the line to be added
Add a premise to the proof.
String representation of the premise.
Check whether all moves are valid and the conclusion is reached.
Get the assumptions that a line of proof assumes.
We search recursively through the cited lines
and look for a line that is justified as an Assumption. We store any such
assumptions in an array. If a line refers directly to an Assumption,
but it correctly applies either Conditional Proof or Indirect Proof,
then the assumption is "discharged" at that point. The new line would
refer to the assumption as a cited line, but it will not assume the
assumptions as one of its non-discharged assumptions.
The line to be analyzed.
Set the conclusion of the proof.
The conclusion.
Generated using TypeDoc
Class representing a natural deduction proof.