All Classes and Interfaces

Class	Description
Abbreviation	An abbreviation.
App	A constant-application expression.
Compose	A compose proof takes statements x, y, ..., each with hypotheses Hx1, Hx2, ... and conclusion Cx, ..., and a statement with exactly the same hypotheses Cx, Cy, ... and conclusion C: it 'applies' the latter statement, by constructing the statement with hypotheses Hx1, Hx2, ..., Hy1, Hy2, ..., and conclusion C.
DVRSet	A set of 'distinct variable restrictions', each of which is an unordered pair of different variable names.
ExpandedAbbreviationsProof	A proof which wraps another proof, and expands all that proof's abbreviations.
Expression	This class represents an expression, i.e., either a variable, or a constant applied to a list of subexpressions.
Expression.Internal	An internal version of an Expression.
Expression.Internal.Wrapper	An object that can wrap an Expression.Internal up as an Expression.
Justification	A justification gives a ProofStep that constructs a statement, and a Proof that constructs all prerequisites of the proof step.
MEPKException	The common base class for all MEPK-related exceptions.
MEPKParseException	This exception indicates that a String could not be parsed to an Expression, a Statement, or a Set of Statements.
MEPKParsers	Parsers for expressions, etc.
MEPKVerificationException	This exception indicates that a Proof did not Proof.verify() correctly.
ParProof	A 'parallel proof' merges two proofs 'in parallel', so that the new proof just collects everything which the two parts prove.
Proof	A proof is a recipe for constructing one set of statements from another using only ProofSteps.
ProofStep	A proof step is the smallest step in a proof: it shows how to create a new statement from existing ones.
ProofStep.Internal	An internal version of a ProofStep.
SeqProof	A 'sequential proof' merges two proofs 'in sequence', where the second proof builds on the second one.
Statement	This class represents an statement.
StatementAbbrExpState	The state that is kept while expanding an Abbreviation throughout a Statement.
Substitute	A substitution proof step takes a statement, and constructs a structurally similar statement by substituting one variable for a (typed) expression.
TrivialProof	A trivial proof grounds exactly its grounding statements, and therefore it does not have to construct anything.
TrivialProof	A proof which trivially grounds exactly its grounding statements.
TrustedProof	A trusted proof is a Proof which is built on the trusted kernel.
TrustedProof.Internal	An internal version of a TrustedProof.
Types	A helper class for easily creating a Map<String,String>, which maps variable names to type expressions.
Types.TypeMapBuilder	A HashMap<String,String> mapping variables to type expressions.
Var	A variable expression.
Weaken	A weakening proof step constructs a new statement by adding DVRs and/or hypotheses to an existing statement.