Package mepk.builtin.internal

Class SeqProof

java.lang.Object

mepk.builtin.internal.SeqProof

All Implemented Interfaces:

TrustedProof.Internal

public class SeqProof
extends Object
implements TrustedProof.Internal

A 'sequential proof' merges two proofs 'in sequence', where the second proof builds on the second one.

Constructor Summary

Constructors

Constructor	Description
SeqProof(Proof proof1, Proof proof2)	Create an instance from two proofs.

Method Summary

Modifier and Type	Method	Description
Map<String,Abbreviation>	getAbbreviations()	Return the abbreviations used by this proof.
Set<Statement>	getGrounded()	Return the set of statements constructed by this proof from the grounding statements.
Set<Statement>	getGrounding()	Return the set of statements which form the basis of this proof.
Justification	getJustificationFor(Statement statement)	Return a justification for the given statement.

Methods inherited from class java.lang.Object

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

Constructor Details

SeqProof

public SeqProof(Proof proof1,
 Proof proof2)

Create an instance from two proofs.

Parameters:

proof1 - the first proof

proof2 - the second proof

Method Details

getGrounding

public Set<Statement> getGrounding()

Description copied from interface: TrustedProof.Internal

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

Specified by:

getGrounding in interface TrustedProof.Internal

Returns:

the grounding statements

getGrounded

public Set<Statement> getGrounded()

Description copied from interface: TrustedProof.Internal

Return the set of statements constructed by this proof from the grounding statements.

Specified by:

getGrounded in interface TrustedProof.Internal

Returns:

the grounded statements

getAbbreviations

public Map<String,Abbreviation> getAbbreviations()

Description copied from interface: TrustedProof.Internal

Return the abbreviations used by this proof.

Specified by:

getAbbreviations in interface TrustedProof.Internal

Returns:

the abbreviations

getJustificationFor

public Justification getJustificationFor(Statement statement)

Description copied from interface: TrustedProof.Internal

Return a justification for the given statement.

Specified by:

getJustificationFor in interface TrustedProof.Internal

Parameters:

statement - a statement which is an element of TrustedProof.Internal.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.