Index (MEPK 0.0.1-SNAPSHOT API)

A C D E G H I J M P S T V W
All Classes and Interfaces|All Packages|Serialized Form

A

Abbreviation - Class in mepk.kernel: An abbreviation.
Abbreviation(Expression, Expression, Expression...) - Constructor for class mepk.kernel.Abbreviation: Create a new abbreviation.
addVarNamesTo(Set<String>) - Method in class mepk.kernel.App
addVarNamesTo(Set<String>) - Method in class mepk.kernel.Expression: Find all variable names in this expression, and add them to the given set.
addVarNamesTo(Set<String>) - Method in interface mepk.kernel.Expression.Internal: Find all variable names in this expression, and add them to the given set.
addVarNamesTo(Set<String>) - Method in class mepk.kernel.Var
andDistinct(String...) - Method in class mepk.kernel.DVRSet: Create a new DVR set by adding a DVR for each pair of the given variable names.
andDistinct(DVRSet) - Method in class mepk.kernel.DVRSet: Create a new DVR set by adding the given DVRs.
App - Class in mepk.kernel: A constant-application expression.
App(String, Expression...) - Static method in class mepk.kernel.Expression: Create an application of a constant to a list of subexpressions.
AppV(String, String...) - Static method in class mepk.kernel.Expression: Create an application of a constant to a list of variable names.
asApp() - Method in class mepk.kernel.Expression: Cast this expression to a constant-application expression.
asVar() - Method in class mepk.kernel.Expression: Cast this expression to a variable expression.

C

Compose - Class in mepk.kernel.internal: 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.
Compose(Statement, Statement...) - Constructor for class mepk.kernel.internal.Compose: Create an instance.
Compose(Statement, Statement...) - Static method in class mepk.kernel.ProofStep: Create a compose proof step, which unifies the conclusions of the given statements with the hypotheses of the given statement

D

Distinct(Iterable<DVRSet>) - Static method in class mepk.kernel.DVRSet: Create the union of multiple DVRSets.
Distinct(String...) - Static method in class mepk.kernel.DVRSet: Create a DVRSet.
Distinct(List<String>) - Static method in class mepk.kernel.DVRSet: Create a DVRSet.
DVRSet - Class in mepk.kernel: A set of 'distinct variable restrictions', each of which is an unordered pair of different variable names.

E

EMPTY - Static variable in class mepk.kernel.DVRSet: The empty DVRSet.
EmptyMap() - Static method in class mepk.builtin.Types: Create an empty type map.
equals(Object) - Method in class mepk.kernel.App
equals(Object) - Method in class mepk.kernel.DVRSet
equals(Object) - Method in class mepk.kernel.Expression
equals(Object) - Method in interface mepk.kernel.Expression.Internal
equals(Object) - Method in class mepk.kernel.Proof
equals(Object) - Method in class mepk.kernel.Statement
equals(Object) - Method in class mepk.kernel.Var
expand(Abbreviation) - Method in class mepk.kernel.Statement: Expand this statement by applying the given abbreviation.
expand(Abbreviation, StatementAbbrExpState) - Method in class mepk.kernel.Expression: Create a new expression by expanding all instances of the given abbreviation, and collect all conditions in accu.
expand(Abbreviation, StatementAbbrExpState, Expression.Internal.Wrapper) - Method in class mepk.kernel.App
expand(Abbreviation, StatementAbbrExpState, Expression.Internal.Wrapper) - Method in interface mepk.kernel.Expression.Internal: Create a new expression by expanding all instances of the given abbreviation, and collect all conditions in accu.
expand(Abbreviation, StatementAbbrExpState, Expression.Internal.Wrapper) - Method in class mepk.kernel.Var
ExpandedAbbreviationsProof - Class in mepk.kernel.util: A proof which wraps another proof, and expands all that proof's abbreviations.
ExpandedAbbreviationsProof(Proof) - Constructor for class mepk.kernel.util.ExpandedAbbreviationsProof: Create a new instance wrapping the given proof.
Expr(String) - Static method in class mepk.builtin.MEPKParsers: Parse the given expression string (in "Ghilbert format") to an Expression instance.
Expression - Class in mepk.kernel: This class represents an expression, i.e., either a variable, or a constant applied to a list of subexpressions.
Expression.Internal - Interface in mepk.kernel: An internal version of an Expression.
Expression.Internal.Wrapper - Interface in mepk.kernel: An object that can wrap an Expression.Internal up as an Expression.

G

getAbbreviations() - Method in class mepk.builtin.internal.ParProof
getAbbreviations() - Method in class mepk.builtin.internal.SeqProof
getAbbreviations() - Method in class mepk.builtin.internal.TrivialProof
getAbbreviations() - Method in class mepk.builtin.TrustedProof
getAbbreviations() - Method in interface mepk.builtin.TrustedProof.Internal: Return the abbreviations used by this proof.
getAbbreviations() - Method in class mepk.kernel.Proof: Return the abbreviations used by this proof.
getAbbreviations() - Method in class mepk.kernel.ProofStep
getAbbreviations() - Method in class mepk.kernel.util.ExpandedAbbreviationsProof
getAbbreviations() - Method in class mepk.kernel.util.TrivialProof
getConclusion() - Method in class mepk.kernel.Statement: Returns the conclusion of this statement.
getConstName() - Method in class mepk.kernel.Abbreviation: Returns the name of this abbreviation.
getConstName() - Method in class mepk.kernel.App: Returns the constant name of this constant-application expression.
getDVRs() - Method in class mepk.kernel.Statement: Returns the distinct-variable restrictions (DVRs) of this statement.
getExpansion() - Method in class mepk.kernel.Abbreviation: Returns the expansion of the abbreviation.
getGrounded() - Method in class mepk.builtin.internal.ParProof
getGrounded() - Method in class mepk.builtin.internal.SeqProof
getGrounded() - Method in class mepk.builtin.internal.TrivialProof
getGrounded() - Method in class mepk.builtin.TrustedProof
getGrounded() - Method in interface mepk.builtin.TrustedProof.Internal: Return the set of statements constructed by this proof from the grounding statements.
getGrounded() - Method in class mepk.kernel.Proof: Return the set of statements constructed by this proof from the grounding statements.
getGrounded() - Method in class mepk.kernel.ProofStep
getGrounded() - Method in class mepk.kernel.util.ExpandedAbbreviationsProof
getGrounded() - Method in class mepk.kernel.util.TrivialProof
getGrounded1() - Method in class mepk.kernel.internal.Compose
getGrounded1() - Method in class mepk.kernel.internal.Substitute
getGrounded1() - Method in class mepk.kernel.internal.Weaken
getGrounded1() - Method in class mepk.kernel.ProofStep: Return the statement constructed by this proof step.
getGrounded1() - Method in interface mepk.kernel.ProofStep.Internal: Return the statement constructed by this proof step.
getGrounding() - Method in class mepk.builtin.internal.ParProof
getGrounding() - Method in class mepk.builtin.internal.SeqProof
getGrounding() - Method in class mepk.builtin.internal.TrivialProof
getGrounding() - Method in class mepk.builtin.TrustedProof
getGrounding() - Method in interface mepk.builtin.TrustedProof.Internal: Return the set of statements which form the basis of this proof.
getGrounding() - Method in class mepk.kernel.internal.Compose
getGrounding() - Method in class mepk.kernel.internal.Substitute
getGrounding() - Method in class mepk.kernel.internal.Weaken
getGrounding() - Method in class mepk.kernel.Proof: Return the set of statements which form the basis of this proof.
getGrounding() - Method in class mepk.kernel.ProofStep: Return the set of statements which form the basis of this proof step.
getGrounding() - Method in interface mepk.kernel.ProofStep.Internal: Return the set of statements which form the basis of this proof step.
getGrounding() - Method in class mepk.kernel.util.ExpandedAbbreviationsProof
getGrounding() - Method in class mepk.kernel.util.TrivialProof
getHypotheses() - Method in class mepk.kernel.Statement: Returns the hypotheses of this statement.
getInternalExpression() - Method in class mepk.kernel.Expression: Returns the internal representation of this expression.
getJustificationFor(Statement) - Method in class mepk.builtin.internal.ParProof
getJustificationFor(Statement) - Method in class mepk.builtin.internal.SeqProof
getJustificationFor(Statement) - Method in class mepk.builtin.internal.TrivialProof
getJustificationFor(Statement) - Method in class mepk.builtin.TrustedProof
getJustificationFor(Statement) - Method in interface mepk.builtin.TrustedProof.Internal: Return a justification for the given statement.
getJustificationFor(Statement) - Method in class mepk.kernel.Proof: Return a justification for the given statement.
getJustificationFor(Statement) - Method in class mepk.kernel.ProofStep
getJustificationFor(Statement) - Method in class mepk.kernel.util.ExpandedAbbreviationsProof
getJustificationFor(Statement) - Method in class mepk.kernel.util.TrivialProof
getNormalVarNames() - Method in class mepk.kernel.Abbreviation: Returns the 'normal' variable names used in this abbreviation, so excluding the 'floating' variable names that are only used in the expansion (TODO: What terminology does Ghilbert use here?).
getProof() - Method in class mepk.kernel.Justification: Return the proof.
getProofStep() - Method in class mepk.kernel.Justification: Return the proof step.
getSubexpressions() - Method in class mepk.kernel.App: Returns the subexpressions of this constant-application expression.
getVarName() - Method in class mepk.kernel.Var: Returns the name of this variable.
getVarNames() - Method in class mepk.kernel.Expression: Return all variables in this expression.

H

hashCode() - Method in class mepk.kernel.App
hashCode() - Method in class mepk.kernel.DVRSet
hashCode() - Method in class mepk.kernel.Expression
hashCode() - Method in interface mepk.kernel.Expression.Internal
hashCode() - Method in class mepk.kernel.Proof
hashCode() - Method in class mepk.kernel.Statement
hashCode() - Method in class mepk.kernel.Var

I

isSimpleApp() - Method in class mepk.kernel.Expression: Is this a simple App expression, i.e., one that contains no nested App expressions?

J

Justification - Class in mepk.kernel: A justification gives a ProofStep that constructs a statement, and a Proof that constructs all prerequisites of the proof step.
Justification(ProofStep, Proof) - Constructor for class mepk.kernel.Justification: Create a new justification.

M

map(String, String) - Static method in class mepk.builtin.Types: Create a single-entry type map.
map(String, String) - Method in class mepk.builtin.Types.TypeMapBuilder: Add the given entry to the type map.
mepk - package mepk: This package implements MEPK, a minimal extensible proof kernel, with a Metamath/Ghilbert-like language.
mepk.builtin - package mepk.builtin: This package implements extensions on top of the mepk.kernel.
mepk.builtin.internal - package mepk.builtin.internal: This package contains internal implementations for the concepts in the mepk.builtin package.
mepk.kernel - package mepk.kernel: This package implements the trusted kernel of MEPK.
mepk.kernel.internal - package mepk.kernel.internal: This package contains internal implementations for the concepts in the mepk.kernel package.
mepk.kernel.util - package mepk.kernel.util: This package contains utilities which are necessary for the kernel, but which are also useful outside of it.
MEPKException - Exception in mepk.kernel: The common base class for all MEPK-related exceptions.
MEPKException(String) - Constructor for exception mepk.kernel.MEPKException: Create an new instance.
MEPKException(Throwable) - Constructor for exception mepk.kernel.MEPKException: Create a new instance.
MEPKParseException - Exception in mepk.builtin: This exception indicates that a String could not be parsed to an Expression, a Statement, or a Set of Statements.
MEPKParseException(Throwable) - Constructor for exception mepk.builtin.MEPKParseException: Create new instance.
MEPKParsers - Class in mepk.builtin: Parsers for expressions, etc.
MEPKVerificationException - Exception in mepk.kernel: This exception indicates that a Proof did not Proof.verify() correctly.
MEPKVerificationException(String) - Constructor for exception mepk.kernel.MEPKVerificationException: Create new instance.

P

Par(Proof, Proof) - Static method in class mepk.builtin.TrustedProof: Merge two proofs 'in parallel', so that the new proof just collects everything which the two parts prove.
ParProof - Class in mepk.builtin.internal: A 'parallel proof' merges two proofs 'in parallel', so that the new proof just collects everything which the two parts prove.
ParProof(Proof, Proof) - Constructor for class mepk.builtin.internal.ParProof: Create an instance from two proofs.
Proof - Class in mepk.kernel: A proof is a recipe for constructing one set of statements from another using only ProofSteps.
Proof() - Constructor for class mepk.kernel.Proof: Create a new proof.
ProofStep - Class in mepk.kernel: A proof step is the smallest step in a proof: it shows how to create a new statement from existing ones.
ProofStep.Internal - Interface in mepk.kernel: An internal version of a ProofStep.

S

Seq(Proof, Proof) - Static method in class mepk.builtin.TrustedProof: Merge two proofs 'in sequence', where the second proof builds on the second one.
SeqProof - Class in mepk.builtin.internal: A 'sequential proof' merges two proofs 'in sequence', where the second proof builds on the second one.
SeqProof(Proof, Proof) - Constructor for class mepk.builtin.internal.SeqProof: Create an instance from two proofs.
Stat(String) - Static method in class mepk.builtin.MEPKParsers: Parse the given statement string to a Statement instance.
Stat(List<Expression>, Expression) - Static method in class mepk.kernel.Statement: Create a new instance with an empty set of DVRs.
Stat(DVRSet, List<Expression>, Expression) - Static method in class mepk.kernel.Statement: Create a new instance.
Statement - Class in mepk.kernel: This class represents an statement.
StatementAbbrExpState - Class in mepk.builtin.internal: The state that is kept while expanding an Abbreviation throughout a Statement.
StatementAbbrExpState() - Constructor for class mepk.builtin.internal.StatementAbbrExpState
substitute(String, Iterable<String>) - Method in class mepk.kernel.DVRSet: Replace the given variable name by the given set of variable names.
substitute(String, Expression) - Method in class mepk.kernel.Expression: Create a new expression by replacing a variable by an expression.
substitute(String, Expression.Internal, Expression.Internal.Wrapper) - Method in class mepk.kernel.App
substitute(String, Expression.Internal, Expression.Internal.Wrapper) - Method in interface mepk.kernel.Expression.Internal: Create a new internal expression by replacing a variable by an internal expression.
substitute(String, Expression.Internal, Expression.Internal.Wrapper) - Method in class mepk.kernel.Var
substitute(String, Expression, Map<String, String>) - Method in class mepk.kernel.Statement: Create a new statement, by replacing one variable in this statement by an expression, and optionally adding type expressions (to make resulting statement type-correct).
Substitute - Class in mepk.kernel.internal: A substitution proof step takes a statement, and constructs a structurally similar statement by substituting one variable for a (typed) expression.
Substitute(Statement, String, Expression, Map<String, String>) - Constructor for class mepk.kernel.internal.Substitute: Create an instance.
Substitute(Statement, String, Expression, Map<String, String>) - Static method in class mepk.kernel.ProofStep: Create a substitution proof step, which takes a statement s and a substitution, and constructs (grounds) the statement resulting from the substitution.

T

toString() - Method in class mepk.kernel.App
toString() - Method in class mepk.kernel.DVRSet
toString() - Method in class mepk.kernel.Expression
toString() - Method in class mepk.kernel.Statement
toString() - Method in class mepk.kernel.Var
Trivial(Set<Statement>) - Static method in class mepk.builtin.TrustedProof: Create a trivial proof, which does no construction at all: both its grounding and grounded statements are just the given statements.
TrivialProof - Class in mepk.builtin.internal: A trivial proof grounds exactly its grounding statements, and therefore it does not have to construct anything.
TrivialProof - Class in mepk.kernel.util: A proof which trivially grounds exactly its grounding statements.
TrivialProof(Set<Statement>) - Constructor for class mepk.builtin.internal.TrivialProof: Create an instance.
TrivialProof(Set<Statement>) - Constructor for class mepk.kernel.util.TrivialProof: Create a new instance.
TrustedProof - Class in mepk.builtin: A trusted proof is a Proof which is built on the trusted kernel.
TrustedProof.Internal - Interface in mepk.builtin: An internal version of a TrustedProof.
Type(String, String) - Static method in class mepk.kernel.Expression: Create a new expression saying 'this variable has that type'.
Type(Expression, String) - Static method in class mepk.kernel.Expression: Create a new expression saying 'this expression has that type'.
Types - Class in mepk.builtin: A helper class for easily creating a Map<String,String>, which maps variable names to type expressions.
Types.TypeMapBuilder - Class in mepk.builtin: A HashMap<String,String> mapping variables to type expressions.

V

Var - Class in mepk.kernel: A variable expression.
Var(String) - Static method in class mepk.kernel.Expression: Create a variable expression.
verify() - Method in class mepk.kernel.Proof: Verify this proof, by checking its justifications and recursively verifying their proofs.
verifyStatementsAreJustified(Set<Statement>) - Method in class mepk.kernel.Proof: Recursively check that each of the given statements is justified: it must either be one of this proof's grounding statements, or have a Justification whose ProofStep yields it and whose proof justifies that step's prerequisites (which are checked recursively).

W

weaken(DVRSet, Expression...) - Method in class mepk.kernel.Statement: Create a new statement, by adding hypotheses and DVRs to this statement.
Weaken - Class in mepk.kernel.internal: A weakening proof step constructs a new statement by adding DVRs and/or hypotheses to an existing statement.
Weaken(Statement, DVRSet, Expression...) - Constructor for class mepk.kernel.internal.Weaken: Create an instance.
Weaken(Statement, DVRSet, Expression...) - Static method in class mepk.kernel.ProofStep: Create a weakening proof step, which takes a statement and adds hypotheses and DVRs.
wrap(Expression.Internal) - Method in interface mepk.kernel.Expression.Internal.Wrapper: Wrap the given internal expression.

A C D E G H I J M P S T V W
All Classes and Interfaces|All Packages|Serialized Form