Package mepk.kernel

Class ProofStep

java.lang.Object
mepk.kernel.Proof
mepk.kernel.ProofStep
public final class ProofStep extends Proof
A proof step is the smallest step in a proof: it shows how to create a new statement from existing ones. Proof steps are values: they cannot be modified after they have been created. It is only possible to create an instance using the static methods in this class.

  • Method Details

    • Substitute

      public static ProofStep Substitute(Statement statement, String varName, Expression replacement, Map<String,String> typesOfNewVars)
      Create a substitution proof step, which takes a statement s and a substitution, and constructs (grounds) the statement resulting from the substitution.
      Parameters:
      statement - the grounding statement
      varName - the variable name
      replacement - the replacement expression
      typesOfNewVars - the additional type expressions
      Returns:
      the created proof step

    • Weaken

      public static ProofStep Weaken(Statement statement, DVRSet addedDVRs, Expression... addedHypotheses)
      Create a weakening proof step, which takes a statement and adds hypotheses and DVRs.
      Parameters:
      statement - the grounding statement
      addedHypotheses - the added hypotheses
      addedDVRs - the added DVRs
      Returns:
      the created proof step

    • Compose

      public static ProofStep Compose(Statement statement, Statement... statements)
      Create a compose proof step, which unifies the conclusions of the given statements with the hypotheses of the given statement
      Parameters:
      statement - the statement which is 'applied'
      statements - the statements to which the statement parameter is 'applied'
      Returns:
      the created proof step

    • getGrounding

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

    • getGrounded1

      public Statement getGrounded1()
      Return the statement constructed by this proof step.
      Returns:
      the grounded statement

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