back to mmj2
These all seem like "nice-to-have" features, but they do not seem to more mmj2 forward on the prime salient.
For example, improved "Hint" processing is almost beside the point when what a power-user would really want is a prover – to at least, finish up the boolean stuff, or the predicate calculus details.
Likewise with output of compressed proofs. Who cares? Just use eimm.exe and export the finished Proof Worksheet directly to your .mm file.
I think these ideas should be retained for possible consideration later. For now, mmj2 is a very good tool that exceeds its initial goals (by a lot). Better not to add complexity unless there is a really good reason! I'm happy now just using mmj2 (working on shortening "hbimd" in set.mm – now that is fun!)
--ocat 4-Aug-2007
1. Provide a "ProofAsstHintSequence?" RunParm? and Edit menu option.
This runparm benefits the user when a large number of hints are generated (see RunParm? "ProofAsstMaxUnifyHints?".)
A greater tree depth may correspond, loosely, to a "better fit", and if tree depths are equal, it may be that a longer formula is "better". (Note that "better" is arbitrary in this context, subject to human preferences – "syl" and "ax-mp" are the most commonly referenced assertions, yet have shallow trees and short formulas…)
2. Add a "MaxUnifyHints?" option to the Proof Assistant Edit Menu.
3. Add a "[MORE]" message to the Hints messsage generated for a proof step if the number of available hints exceeds the "MaxUnifyHints?" option value.
4. Provide an "ProofAsstExpandHints?" RunParm? and Proof Assistant Edit menu option. ExpandHints? = "Yes" will, if Hints are available following unification, generate a window containing the actual Hint hypotheses and conclusions instead of just assertion labels on the Request Message screen. For example ax-mp would be output on a separate line of the new Hints Screen as "ax-mp : ( ph → ps ) && ph ==> ps". Naturally, the expanded hints will be displayed on the Hints Screen in the order requested by the "ProofAsstHintSequence?" option.
5. Provide a "ProofAsstCompressProofs?" RunParm? and Proof Assistant Edit Menu option (default = "No"). If set to "Yes" the generated RPN-format Metamath proofs generated by the Proof Assistant GUI will be in Metamath "compressed" format (see Metamath.pdf).
6. Provide a new Unify Menu option "Unify+CompareToDB?" which compares a new proof to the proof already in the input Metamath (.mm file) database. Comparison metrics will indicate whether or not a new proof is a good candidate, subject to double-checking against set.mm's listed criteria, for inclusion in the Metamath database. The metrics to be computed and output in a Request Messages screen message are:
7. If time permits, create a "OptionalDjVars?" RunParm? to disable Optional Disjoint Variable Restriction "soft" Errors (default setting = "enabled".)
In view of the fact that Metamath is one of the "crown jewels" of Planet Earth and the human species, it is inevitable that one day "soft" Dj Vars Error reporting will be eliminated, along with $d statements for optional variables; when that day arrives, mmj2 will be ready.
The amount of redundant storage and processing, not to mention human resources expended on these indicates a clearly beneficial Opportunity For Achievement. Optional Disjoint Variable Restrictions complicate the Metamath language and databases yet provide no benefits. Given that the mmj2 "engine" will be up on the mechanics rack one more time, it makes sense to do the work sooner than later.