public class VerifyProofs extends java.lang.Object implements ProofVerifier
It also has a new feature, verifying a syntax RPN as if it were a proof (in a sense, Stmt.exprRPN is a proof, a proof that Stmt.formula can be generated using the grammar embodied in the Metamath file...) The purpose of this feature is primarily to test the grammatical parser's output -- a double-check of the results.
The code is optimized for batch processing of a large number of proofs, one after the other.
The main "optimization" was to re-use arrays instead of allocating them for each proof. The arrays are initially allocated at a size that fits set.mm, which has some massive proofs. If an ArrayIndexOutOfBounds exception is detected, the arrays are reallocated with a larger size (an upper limit halts this process), and a "retry" is performed.
VerifyProofs uses class SubstMapEntry which is a simple data structure that should probably be an inner class of VerifyProofs. Other clean-ups are probably at hand for reworking this *thing*. One thing is sure, the error messages provided by VerifyProofs are much less helpful than those from metamath.exe -- but, on the other hand, since Proof Assistant is the best way to create proofs, a proof error in an existing file should be rare (creating a Metamath proof by hand is like writing assembler code.)
FYI, here is the basic verification algorithm, which leaves out the ugly details of disjoint variable restrictions and substitutions:
1. init proof work stack, etc. 2. loop through theorem proof array, for each proof[] step: - if null, exception ==> proof incomplete - if stmt is a Hyp, ==> push stmt.formula onto stack - else if stmt.mandFrame.hypArray.length = zero ==> push stmt.formula onto stack (see ccau, for ex.) - else (assertion w/hyp): findVarSubstMap for assertion if notfnd ==> exception...various else, - check DjVars restrictions - pop 'n' entries from stack ('n' = nbr of mand hyps) - throw exception if stack underflow! - push substituted assertion formula onto stack. 3. if stack has more than one entry left, ==>exception, > 1 stack entry left, disproved! 4. if stack entry not equal to stmt to be proved formula ==>exception, last entry not equal! disproved! 5. ok! proved.
Constructor and Description |
---|
VerifyProofs()
Constructor - default.
|
Modifier and Type | Method and Description |
---|---|
Formula |
convertRPNToFormula(ParseTree.RPNStep[] formulaRPN,
java.lang.String stepLabelForMessages)
Generate Formula from RPN.
|
int |
getPExprHighwater() |
java.util.List<ProofDerivationStepEntry> |
getProofDerivationSteps(Theorem theorem,
boolean exportFormatUnified,
HypsOrder hypsOrder,
Cnst provableLogicStmtTyp)
Builds and returns an ArrayList of proof steps for export via the Proof
Assistant.
|
int |
getPStackHighwater() |
int |
getSubstHighwater() |
void |
raiseVerifyException(java.lang.String stepLabel,
ErrorCode code,
java.lang.Object... args) |
void |
verifyAllExprRPNAsProofs(Messages messages,
java.util.Map<java.lang.String,Stmt> stmtTbl)
Verify all Statements' grammatical parse RPNs.
|
void |
verifyAllProofs(Messages messages,
java.util.Map<java.lang.String,Stmt> stmtTbl)
Verify all proofs in Statement Table.
|
VerifyException |
verifyDerivStepDjVars(java.lang.String derivStepNbr,
java.lang.String derivStepStmtLabel,
Assrt derivStepRef,
ParseNode[] derivStepAssrtSubst,
ScopeFrame derivStepComboFrame,
PaConstants.DjVarsSoftErrors djVarsSoftErrors,
java.util.List<DjVars> softDjVarsErrorList)
Verify that a single proof derivation step does not violate the Distinct
Variable Restrictions of the step's Ref assertion.
|
VerifyException |
verifyDerivStepProof(java.lang.String derivStepStmtLabel,
Formula derivStepFormula,
ParseTree derivStepProofTree,
ScopeFrame derivStepComboFrame)
Verify a single proof derivation step.
|
VerifyException |
verifyExprRPNAsProof(Stmt exprRPNStmt)
Verify grammatical parse RPN as if it were a proof.
|
VerifyException |
verifyOneProof(Theorem theorem)
Verify a single proof.
|
public void verifyAllProofs(Messages messages, java.util.Map<java.lang.String,Stmt> stmtTbl)
verifyAllProofs
in interface ProofVerifier
messages
- Messages object for output error messages.stmtTbl
- Statement Table (map).public VerifyException verifyOneProof(Theorem theorem)
verifyOneProof
in interface ProofVerifier
theorem
- Theorem object reference.public void verifyAllExprRPNAsProofs(Messages messages, java.util.Map<java.lang.String,Stmt> stmtTbl)
Note: even VarHyp and Syntax Axioms are assigned default RPN's, so this should work -- unless there are errors in the Metamath file, or in the grammar itself.
verifyAllExprRPNAsProofs
in interface ProofVerifier
messages
- Messages object for output error messages.stmtTbl
- Statement Table (map).public VerifyException verifyExprRPNAsProof(Stmt exprRPNStmt)
Note: even VarHyp and Syntax Axioms are assigned default RPN's, so this should work -- unless there are errors in the Metamath file, or in the grammar itself.
verifyExprRPNAsProof
in interface ProofVerifier
exprRPNStmt
- Stmt with RPN to verify.public VerifyException verifyDerivStepProof(java.lang.String derivStepStmtLabel, Formula derivStepFormula, ParseTree derivStepProofTree, ScopeFrame derivStepComboFrame)
Note: the "comboFrame" contains the mandatory and optional information as a matter of convenience. The "optional" information is kept separate in Metamath because it needs to be available in Proof Verifier (and elsewhere), but must not be used when the Assertion is referenced in a proof (especially not be pushed onto the stack!)
derivStepStmtLabel
- label + "Step" + step numberderivStepFormula
- formula of proof stepderivStepProofTree
- step proof tree.derivStepComboFrame
- MandFrame for step.public VerifyException verifyDerivStepDjVars(java.lang.String derivStepNbr, java.lang.String derivStepStmtLabel, Assrt derivStepRef, ParseNode[] derivStepAssrtSubst, ScopeFrame derivStepComboFrame, PaConstants.DjVarsSoftErrors djVarsSoftErrors, java.util.List<DjVars> softDjVarsErrorList)
The main complication here is converting the parse subtrees that comprise the variable substitutions into the form required by method checkDjVars().
Note: the "comboFrame" contains the mandatory and optional information as a matter of convenience. The "optional" information is kept separate in Metamath because it needs to be available in Proof Verifier (and elsewhere), but must not be used when the Assertion is referenced in a proof (especially not be pushed onto the stack!)
derivStepNbr
- string, may equal "qed"derivStepStmtLabel
- label + "Step" + step numberderivStepRef
- Assertion justifying the stepderivStepAssrtSubst
- array of substitution subtreesderivStepComboFrame
- MandFrame for step.djVarsSoftErrors
- whether to ignore or generate missing DjVars
restrictionssoftDjVarsErrorList
- the output list of violated DjVarspublic java.util.List<ProofDerivationStepEntry> getProofDerivationSteps(Theorem theorem, boolean exportFormatUnified, HypsOrder hypsOrder, Cnst provableLogicStmtTyp) throws VerifyException
theorem
- the theorem whose proof will be exportedexportFormatUnified
- set to true if proof step label is output on
each step (else, it is only output on Logical Hypothesis
steps.)hypsOrder
- the order in which step hyps should be arranged (a
testing feature.)provableLogicStmtTyp
- type code of proof derivation steps to
return.VerifyException
- if the proof is invalid.public void raiseVerifyException(java.lang.String stepLabel, ErrorCode code, java.lang.Object... args) throws VerifyException
VerifyException
public int getPStackHighwater()
public int getPExprHighwater()
public int getSubstHighwater()
public Formula convertRPNToFormula(ParseTree.RPNStep[] formulaRPN, java.lang.String stepLabelForMessages)
formulaRPN
- to be converted to a FormulastepLabelForMessages
- used for abend message :)