Package mepk.kernel
The basic building block is a Statement, representing statements like "for every
natural number n, n >= 0". Any syntactically correct statement can be constructed, and
statements represent both axioms and theorems.
Then a ProofStep shows how to construct new statements from
existing statements: there are only a few built-in proof steps (substitute, compose, weaken)
and none can be added.
Finally a Proof represents a recipe for constructing one set of
statements from another using only ProofSteps.
The language of statements and their expressions is that of Ghilbert,
but using Metamath's philosophy of types:
expressions are trees of constants and variables;
statements have hypotheses
and a conclusion;
and dummy variables are handled using 'distinct variable restrictions'.
Every Proof can be verified mechanically by asking it to justify each of its
statements: this is implemented in Proof.verify().
It should then provide a ProofStep which constructs that statement,
together with Proofs for the prerequisites of that ProofStep.
-
ClassDescriptionAn abbreviation.A constant-application expression.A set of 'distinct variable restrictions', each of which is an unordered pair of different variable names.This class represents an expression, i.e., either a variable, or a constant applied to a list of subexpressions.An internal version of an
Expression.An object that can wrap anExpression.Internalup as anExpression.The common base class for all MEPK-related exceptions.This exception indicates that aProofdid notProof.verify()correctly.A proof is a recipe for constructing one set of statements from another using onlyProofSteps.A proof step is the smallest step in a proof: it shows how to create a new statement from existing ones.An internal version of aProofStep.This class represents an statement.A variable expression.