Package mepk.builtin

Class TrustedProof

java.lang.Object

mepk.kernel.Proof

mepk.builtin.TrustedProof

public final class TrustedProof
extends Proof

A trusted proof is a Proof which is built on the trusted kernel. Trusted proofs 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.

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
static interface	TrustedProof.Internal	An internal version of a TrustedProof.

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.
static Proof	Par(Proof proof1, Proof proof2)	Merge two proofs 'in parallel', so that the new proof just collects everything which the two parts prove.
static Proof	Seq(Proof proof1, Proof proof2)	Merge two proofs 'in sequence', where the second proof builds on the second one.
static Proof	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.

Methods inherited from class mepk.kernel.Proof

equals, hashCode, verify, verifyStatementsAreJustified

Methods inherited from class java.lang.Object

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

Method Details

Trivial

public static Proof 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.

Parameters:

statements - the statements that will be returned by both getGrounding() and getGrounded().

Returns:

the created proof

Par

public static Proof Par(Proof proof1,
 Proof proof2)

Merge two proofs 'in parallel', so that the new proof just collects everything which the two parts prove.

Parameters:

proof1 - one proof

proof2 - another proof

Returns:

the created proof

Seq

public static Proof Seq(Proof proof1,
 Proof proof2)

Merge two proofs 'in sequence', where the second proof builds on the second one.

Parameters:

proof1 - the first proof

proof2 - the second proof

Returns:

the created proof

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.