public class ProofUnifier
extends java.lang.Object
The job here is to unify the steps in a ProofWorksheet and build the proof trees for the derivation steps in the proof. The proof tree of the 'qed' step equals the proof of the Theorem, fyi.
There are five main things happening here (whew!):
The algorithm to do these things is not godlike :) It searches for the first Assrt that successfully unifies with each proof step -- if the Ref is not input. But there may be multiple assertions that unify with a step, and it is possible that unification as a whole fails because an earlier step's Ref label is wrong. The "unification" process means finding a consistent set of variable substitutions. To unify an entire proof the requirement is that the substitutions be consistent across the entire proof. However, the algorithm does work for set.mm and ql.mm without any false positives. (As a fallback, the user can input Ref to avoid the problem of multiple possible unifications.)
Also, a RunParm is provided to specify double-checking each unification using the VerifyProofs.java object -- i.e. the Metamath "Proof Verification Engine" . The default option is NO, but should probably be YES in practice given that response time is not a problem (yet?) This will catch false unifications early.
It should also be noted that ProofUnifier does check Distinct Variable ($d) restrictions as it works on each proof step. This feature is an enhancement to the Metamath Proof Assistant, which does not check $d's. By checking $d's here we also avoid false unification positives and improve the results of the algorithm.
Modifier and Type | Class and Description |
---|---|
static interface |
ProofUnifier.PostUnifyHook |
Modifier and Type | Field and Description |
---|---|
ProofUnifier.PostUnifyHook |
postUnifyHook |
Constructor and Description |
---|
ProofUnifier(ProofAsst proofAsst)
Standard constructor for set up.
|
Modifier and Type | Method and Description |
---|---|
<T extends MMJException> |
addStepContext(T e) |
ProofAsstException |
getException(ErrorCode code,
java.lang.Object... args) |
java.util.List<Assrt> |
getSortedAssrtSearchList() |
boolean |
getTablesInitialized() |
java.util.List<Assrt> |
getUnifySearchListByMObjSeq() |
boolean |
initializeLookupTables(Messages messages)
Initialize lookup tables to be used across multiple executions of the
GUI.
|
void |
mergeListOfAssrtAddsSortedBySeq(java.util.List<Theorem> listOfAssrtAddsSortedBySeq)
Merges a list of added Assrt objects sorted by MObj seq into the
unifySearchList and passes the list on to the StepSelectorSearch for its
updates.
|
void |
reportUnificationFailures() |
static void |
separateMandAndOptFrame(ProofWorksheet proofWorksheet,
DerivationStep qedStep,
java.util.List<? super VarHyp> mandHypList,
java.util.List<VarHyp> optionalVarHypList,
boolean addLogHyps) |
void |
setTransformationManager(TransformationManager trManager) |
void |
unifyAllProofDerivationSteps(ProofWorksheet proofWorksheet,
Messages messages,
boolean noConvertWV)
Unifies the proof steps in a Proof Worksheet.
|
boolean |
unifyHypsWithoutWorkVarsGeneralCase(ParseNode[][] assrtLogHypSubstArray)
General case of hypothesis unification
|
public ProofUnifier.PostUnifyHook postUnifyHook
public ProofUnifier(ProofAsst proofAsst)
proofAsst
- the main ProofAsst objectpublic java.util.List<Assrt> getUnifySearchListByMObjSeq()
public boolean getTablesInitialized()
public boolean initializeLookupTables(Messages messages)
This is the place to create optimizations of search tables, etc. for the Unification process.
messages
- the mmj.lang.Messages object used to store error and
informational messages.public java.util.List<Assrt> getSortedAssrtSearchList()
public void mergeListOfAssrtAddsSortedBySeq(java.util.List<Theorem> listOfAssrtAddsSortedBySeq)
listOfAssrtAddsSortedBySeq
- List of Assrt sorted by MObj.seq
representing new assertions which were added to the
LogicalSystem.public void unifyAllProofDerivationSteps(ProofWorksheet proofWorksheet, Messages messages, boolean noConvertWV) throws VerifyException
This is called by ProofAsst.java.
The "parallelStepUnificationMethod()" is used for unification. This means that one pass is made through LogicalSystem.stmtTbl and for each Stmt, an attempt is made to unify each un-unified proof step with that Stmt. Speed-wise, this works fine now. In theory, if set.mm had 1 million Theorems things would be uglier and it might be better to use Stmt lookup tables to unify each proof step, one by one. But today the extra coding effort to build those tables might not even produce an improvement in performance. The longest Theorem proof unification is around 500,000,000 nanoseconds -- or 1/2 second -- which is acceptable for the ProofAsstGUI's response time. (The average unification time is much less, like 1/10 second.)
proofWorksheet
- proof in progressmessages
- the mmj.lang.Messages object used to store error and
informational messages.noConvertWV
- true if we should not replace work vars with dummy
vars in derivation stepsVerifyException
- if unification was unsuccessfulpublic boolean unifyHypsWithoutWorkVarsGeneralCase(ParseNode[][] assrtLogHypSubstArray)
assrtLogHypSubstArray
- a temporary-use array with some unification
resultspublic void reportUnificationFailures()
public static void separateMandAndOptFrame(ProofWorksheet proofWorksheet, DerivationStep qedStep, java.util.List<? super VarHyp> mandHypList, java.util.List<VarHyp> optionalVarHypList, boolean addLogHyps)
public void setTransformationManager(TransformationManager trManager)
public <T extends MMJException> T addStepContext(T e)
public ProofAsstException getException(ErrorCode code, java.lang.Object... args)