Uses of Class
mepk.kernel.Statement

Packages that use Statement

Package	Description
mepk.builtin	This package implements extensions on top of the mepk.kernel.
mepk.builtin.internal	This package contains internal implementations for the concepts in the mepk.builtin package.
mepk.kernel	This package implements the trusted kernel of MEPK.
mepk.kernel.internal	This package contains internal implementations for the concepts in the mepk.kernel package.
mepk.kernel.util	This package contains utilities which are necessary for the kernel, but which are also useful outside of it.

Uses of Statement in mepk.builtin

Methods in mepk.builtin that return Statement

Modifier and Type	Method	Description
static Statement	MEPKParsers.Stat(String statementAsString)	Parse the given statement string to a Statement instance.

Methods in mepk.builtin that return types with arguments of type Statement

Modifier and Type	Method	Description
Set<Statement>	TrustedProof.getGrounded()
Set<Statement>	TrustedProof.Internal.getGrounded()	Return the set of statements constructed by this proof from the grounding statements.
Set<Statement>	TrustedProof.getGrounding()
Set<Statement>	TrustedProof.Internal.getGrounding()	Return the set of statements which form the basis of this proof.

Methods in mepk.builtin with parameters of type Statement

Modifier and Type	Method	Description
Justification	TrustedProof.getJustificationFor(Statement statement)
Justification	TrustedProof.Internal.getJustificationFor(Statement statement)	Return a justification for the given statement.

Method parameters in mepk.builtin with type arguments of type Statement

Modifier and Type	Method	Description
static Proof	TrustedProof.Trivial(Set<Statement> statements)	Create a trivial proof, which does no construction at all: both its grounding and grounded statements are just the given statements.

Uses of Statement in mepk.builtin.internal

Methods in mepk.builtin.internal that return types with arguments of type Statement

Modifier and Type	Method	Description
Set<Statement>	ParProof.getGrounded()
Set<Statement>	SeqProof.getGrounded()
Set<Statement>	TrivialProof.getGrounded()
Set<Statement>	ParProof.getGrounding()
Set<Statement>	SeqProof.getGrounding()
Set<Statement>	TrivialProof.getGrounding()

Methods in mepk.builtin.internal with parameters of type Statement

Modifier and Type	Method	Description
Justification	ParProof.getJustificationFor(Statement statement)
Justification	SeqProof.getJustificationFor(Statement statement)
Justification	TrivialProof.getJustificationFor(Statement statement)

Constructor parameters in mepk.builtin.internal with type arguments of type Statement

Modifier	Constructor	Description
	TrivialProof(Set<Statement> statements)	Create an instance.

Uses of Statement in mepk.kernel

Methods in mepk.kernel that return Statement

Modifier and Type	Method	Description
Statement	ProofStep.getGrounded1()	Return the statement constructed by this proof step.
Statement	ProofStep.Internal.getGrounded1()	Return the statement constructed by this proof step.
static Statement	Statement.Stat(List<Expression> hypotheses, Expression conclusion)	Create a new instance with an empty set of DVRs.
static Statement	Statement.Stat(DVRSet dvrs, List<Expression> hypotheses, Expression conclusion)	Create a new instance.
Statement	Statement.substitute(String varName, Expression replacement, Map<String,String> typesOfNewVars)	Create a new statement, by replacing one variable in this statement by an expression, and optionally adding type expressions (to make resulting statement type-correct).
Statement	Statement.weaken(DVRSet addedDVRs, Expression... addedHypotheses)	Create a new statement, by adding hypotheses and DVRs to this statement.

Methods in mepk.kernel that return types with arguments of type Statement

Modifier and Type	Method	Description
Set<Statement>	Statement.expand(Abbreviation abbreviation)	Expand this statement by applying the given abbreviation.
abstract Set<Statement>	Proof.getGrounded()	Return the set of statements constructed by this proof from the grounding statements.
Set<Statement>	ProofStep.getGrounded()
abstract Set<Statement>	Proof.getGrounding()	Return the set of statements which form the basis of this proof.
Set<Statement>	ProofStep.getGrounding()	Return the set of statements which form the basis of this proof step.
Set<Statement>	ProofStep.Internal.getGrounding()	Return the set of statements which form the basis of this proof step.

Methods in mepk.kernel with parameters of type Statement

Modifier and Type	Method	Description
static ProofStep	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
abstract Justification	Proof.getJustificationFor(Statement statement)	Return a justification for the given statement.
Justification	ProofStep.getJustificationFor(Statement statement)
static ProofStep	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.
static ProofStep	ProofStep.Weaken(Statement statement, DVRSet addedDVRs, Expression... addedHypotheses)	Create a weakening proof step, which takes a statement and adds hypotheses and DVRs.

Method parameters in mepk.kernel with type arguments of type Statement

Modifier and Type	Method	Description
protected final void	Proof.verifyStatementsAreJustified(Set<Statement> grounded)	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).

Uses of Statement in mepk.kernel.internal

Methods in mepk.kernel.internal that return Statement

Modifier and Type	Method	Description
Statement	Compose.getGrounded1()
Statement	Substitute.getGrounded1()
Statement	Weaken.getGrounded1()

Methods in mepk.kernel.internal that return types with arguments of type Statement

Modifier and Type	Method	Description
Set<Statement>	Compose.getGrounding()
Set<Statement>	Substitute.getGrounding()
Set<Statement>	Weaken.getGrounding()

Constructors in mepk.kernel.internal with parameters of type Statement

Modifier	Constructor	Description
	Compose(Statement statement, Statement... statements)	Create an instance.
	Substitute(Statement statement, String varName, Expression replacement, Map<String,String> typesOfNewVars)	Create an instance.
	Weaken(Statement statement, DVRSet addedDVRs, Expression... addedHypotheses)	Create an instance.

Uses of Statement in mepk.kernel.util

Methods in mepk.kernel.util that return types with arguments of type Statement

Modifier and Type	Method	Description
Set<Statement>	ExpandedAbbreviationsProof.getGrounded()
Set<Statement>	TrivialProof.getGrounded()
Set<Statement>	ExpandedAbbreviationsProof.getGrounding()
Set<Statement>	TrivialProof.getGrounding()

Methods in mepk.kernel.util with parameters of type Statement

Modifier and Type	Method	Description
Justification	ExpandedAbbreviationsProof.getJustificationFor(Statement statement)
Justification	TrivialProof.getJustificationFor(Statement statement)

Constructor parameters in mepk.kernel.util with type arguments of type Statement

Modifier	Constructor	Description
	TrivialProof(Set<Statement> statements)	Create a new instance.