Package mepk.kernel

Class Proof

java.lang.Object
mepk.kernel.Proof
Direct Known Subclasses:
ExpandedAbbreviationsProof, ProofStep, TrivialProof, TrustedProof
public abstract class Proof extends Object
A proof is a recipe for constructing one set of statements from another using only ProofSteps. Proofs should be values: it should not be possible to modify them after they have been created.

  • Constructor Details

    • Proof

      protected Proof()
      Create a new proof.

  • Method Details

    • getGrounding

      public abstract Set<Statement> getGrounding()
      Return the set of statements which form the basis of this proof.
      Returns:
      the grounding statements

    • getGrounded

      public abstract Set<Statement> getGrounded()
      Return the set of statements constructed by this proof from the grounding statements.
      Returns:
      the grounded statements

    • getAbbreviations

      public abstract Map<String,Abbreviation> getAbbreviations()
      Return the abbreviations used by this proof.
      Returns:
      the abbreviations

    • getJustificationFor

      public abstract Justification getJustificationFor(Statement statement)
      Return a justification for the given statement.
      Parameters:
      statement - a statement which is an element of getGrounded()
      Returns:
      either null, meaning that no justification is necessary because getGrounding().contains(statement); or a Justification which gives a proof step that constructs the statement, and a proof that constructs all prerequisites of the proof step.

    • hashCode

      public final int hashCode()
      Overrides:
      hashCode in class Object

    • equals

      public final boolean equals(Object other)
      Overrides:
      equals in class Object

    • verify

      public final void verify() throws MEPKVerificationException
      Verify this proof, by checking its justifications and recursively verifying their proofs.
      Throws:
      MEPKVerificationException - if the verification fails.

    • verifyStatementsAreJustified

      protected final void verifyStatementsAreJustified(Set<Statement> grounded) throws MEPKVerificationException
      Recursively check that each of the given statements is justified: it must either be one of this proof's grounding statements, or have a Justification whose ProofStep yields it and whose proof justifies that step's prerequisites (which are checked recursively). This proof must not have any abbreviations left to expand.
      Parameters:
      grounded - the statements to check; must be a subset of getGrounded()
      Throws:
      MEPKVerificationException - if any statement is not justified