Package mepk.builtin.internal

Class ParProof

java.lang.Object

mepk.builtin.internal.ParProof

All Implemented Interfaces:

TrustedProof.Internal

public class ParProof
extends Object
implements TrustedProof.Internal

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

Constructor Summary

Constructors

Constructor	Description
ParProof(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

ParProof

public ParProof(Proof proof1,
 Proof proof2)

Create an instance from two proofs.

Parameters:

proof1 - one proof

proof2 - another 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.