Package mepk.kernel.util

Class ExpandedAbbreviationsProof

java.lang.Object
mepk.kernel.Proof
mepk.kernel.util.ExpandedAbbreviationsProof
public class ExpandedAbbreviationsProof extends Proof
A proof which wraps another proof, and expands all that proof's abbreviations.

  • Constructor Details

    • ExpandedAbbreviationsProof

      public ExpandedAbbreviationsProof(Proof proof)
      Create a new instance wrapping the given proof.
      Parameters:
      proof - the proof whose abbreviations are to be expanded

  • Method Details

    • getGrounding

      public Set<Statement> getGrounding()
      Description copied from class: Proof
      Return the set of statements which form the basis of this proof.
      Specified by:
      getGrounding in class Proof
      Returns:
      the grounding statements

    • getGrounded

      public Set<Statement> getGrounded()
      Description copied from class: Proof
      Return the set of statements constructed by this proof from the grounding statements.
      Specified by:
      getGrounded in class Proof
      Returns:
      the grounded statements

    • getAbbreviations

      public Map<String,Abbreviation> getAbbreviations()
      Description copied from class: Proof
      Return the abbreviations used by this proof.
      Specified by:
      getAbbreviations in class Proof
      Returns:
      the abbreviations

    • getJustificationFor

      public Justification getJustificationFor(Statement statement)
      Description copied from class: Proof
      Return a justification for the given statement.
      Specified by:
      getJustificationFor in class Proof
      Parameters:
      statement - a statement which is an element of Proof.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.