Package mepk.kernel.internal

Class Substitute

java.lang.Object

mepk.kernel.internal.Substitute

All Implemented Interfaces:

ProofStep.Internal

public class Substitute
extends Object
implements ProofStep.Internal

A substitution proof step takes a statement, and constructs a structurally similar statement by substituting one variable for a (typed) expression.

Constructor Summary

Constructors

Constructor	Description
Substitute(Statement statement, String varName, Expression replacement, Map<String,String> typesOfNewVars)	Create an instance.

Method Summary

Modifier and Type	Method	Description
Statement	getGrounded1()	Return the statement constructed by this proof step.
Set<Statement>	getGrounding()	Return the set of statements which form the basis of this proof step.

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Details

Substitute

public Substitute(Statement statement,
 String varName,
 Expression replacement,
 Map<String,String> typesOfNewVars)

Create an instance.

Parameters:

statement - the grounding statement

varName - the variable name

replacement - the replacement expression

typesOfNewVars - the additional type expressions

Method Details

getGrounding

public Set<Statement> getGrounding()

Description copied from interface: ProofStep.Internal

Return the set of statements which form the basis of this proof step.

Specified by:

getGrounding in interface ProofStep.Internal

Returns:

the grounding statements

getGrounded1

public Statement getGrounded1()

Description copied from interface: ProofStep.Internal

Return the statement constructed by this proof step.

Specified by:

getGrounded1 in interface ProofStep.Internal

Returns:

the grounded statement