mmj2 - 01-Nov-2011 Release

General Documentation:

• QuickStart.html - How to install and start-up mmj2 for the first time
  
• README.html - Information about mmj2, its status, acknowledgements, etc.
• doc\PAUserGuide\start.html - Proof Assistant User Guide.
• LICENSE.TXT - GNU GENERAL PUBLIC LICENSE Version 2, June 1991
  
• INSTALL.html - Detailed instructions for installing mmj2 and taking the next step...
  
• SunJavaTutorialLicense.html - Sun Microsystems license requirements (included because mmj.pa.ProofAsstGUI.java
  has several snippets of code that are very similar, if not identical to snippets of code in the Java Tutorial.)
• CHGLOG.TXT - Log of mmj2 changes, sequenced by software release.
  

User Documentation:

• doc\PAUserGuide\start.html - Proof Assistant User Guide. Assumes mmj2 INSTALL.TXT has been completed and that the user is able to start the mmj2 Proof Assistant GUI screen.
• mmj2jar\mmj2PATutorial.bat - Interactive tutorial that uses the mmj2 Proof Assistant and a set of valid Proof Worksheets containing instructional text.
• data\runparm\windows\AnnotatedRunParms.txt - This is a valid RunParm file which contains extensive RunParm Comment lines that describe every RunParm command defined in mmj2. RunParms are commands that either alter user preference settings or provide the programs the names of input and output folders/files, (like "set.mm"), and which initiate processing, such as initiation of the Proof Assistant GUI program. The file name of a RunParm file is passed on the command line to the mmj2jar.jar file to run mmj2. 
• mmj2jar\RunParmsComplete.txt - Is functionally equivalent to RunParms.txt but contains every possible RunParm command either with default settings or "asterisked out" (whereas RunParms.txt contains only the necessary minimum.)
  
• doc\ProofAssistantGUIQuickHOWTO.html - Brief overview on the use of the Proof Assistant GUI program.
  
• doc\ProofAssistantTutorial.html - A brief explanation of how to use the Proof Assistant Tutorial which consists of  commented Proof Worksheet files for interactive self-study use within the Proof Assistant GUI program.
  
• doc\ProofAssistantGUIDetailedInfo.html - An in-depth reference documente reviewing of the nitty-gritty details of the Proof Assistant GUI screen, its fields and validation edits. This is not a pleasant document to read, but it may help clarify certain points about what is going on...
  
• doc\ProofAsstGUICursorHandling.html - A brief explanation of how the Proof Assistant positions the cursor in various circumstances. This is another document written in "legalese" that you will most likely feel is difficult, poorly written and unpleasant :)
• doc\TheoremLoaderOverview.html - Information about the new (1-Aug-2008 release) Theorem Loader enhancement (plus some info about the new "mmj2 Service" feature!)
  
• doc\TextModeFormulaFormatting.html - A lengthy review of "TMFF", the new Text Mode Formula Formatting feature. You will want to read this if you plan to alter the default TMFF RunParm settings that define the built-in TMFF Formats and formatting Schemes -- or if you are dissatisfied with TMFF and want to suggest a new algorithm (TMFF was coded in a way that will, it is hoped, facilitate adding new formatting algorithms.)
• doc\GMFFDoc\* - A set of folders and files that document the GMFF -- Graphics Mode Formula Formatting -- (i.e. html) feature.
  
• doc\StepUnifier.html - Somewhat technical, but with lots of diagrams and examples, StepUnifier.html explains unification from the perspective of mmj2.
  
• doc\WorkVariables.html - Explains the new Work Variables used in mmj2!
• doc\StepSelectorSearch.html - Documentation of the new Unify menu item on the Proof Assistant GUI.
• doc\UnifyEraseAndRederiveFormulasFeature.html - Documentation of the new Unify menu item on the Proof Assistant GUI.
  
• doc\BottomUpProving-ByNormMegill.html - Tutorial written by Norm Megill about using mmj2 to emulate the Metamath "Solitaire" prover, and in general, how to prove theorems using the "Bottom Up" method with mmj2.
  

Technically-Oriented (Programmer stuff) Documentation:

• MMJ2DirectoryStructure.txt - The hierarchy of directories contained in mmj2.zip.
  
• RunningTheMMJ2TestSuite.html - Cookbook for running the built-in mmj2 tests used to verify each new mmj2 software release.
• doc\mmj2Service\ -- The mmj2 Service feature with samples invoking mmj2 using the "mmj2 Service" feature.
  
• MetamathERNotes.html - This document provides some very useful information about the nomenclature used in the mmj2 programs as well as the various objects ("Entities") and their Relationships used to construct the "LogicalSystem" from an input .mm database. This may be of some use to the general reader as it may be that error messages containing abbreviations such as "Sym" will be more comprehensible after reading this document. What this document mainly provides is the vital facts such as the two types of Sym (Cnst and Var), the two types of Stmt (Hyp and Assrt), the two types of Hyp (VarHyp and LogHyp), and so on. (This is the "Rosetta Stone" for deciphering the mmj2.lang java code :)
  
• mmjProofVerification.html - This document restates the Metamath Proof Verification algorithm (excluding $d 's) and provides two fully worked-out examples showing the contents of the Proof Work and Hypothesis stacks at each point during the proofs. (It is interesting to note that the proof details of even the simplest theorem, "a1i", are mind-bogglingly tedious and intricate -- virtually impossible to read -- and yet the most complex Metamath proofs require a Proof Work stack thousands of items deep!!!)
  
• BasicsOfSyntaxAxiomsAndTypes.html - Introductory information about Metamath Syntax Axioms and Type Codes.
  
• SyntaxAxiomRulesAndConventions.html - More about Syntax Axioms plus "The (Previously) Unwritten Rules for Syntax Axioms".
  
• ExampleMetamathDatabase.html - Extensively annotated Metamath file showing syntax declarations.
  
• ExampleMetamathGrammar.html - An attempt to illustrate a way to create a grammar from the Example Metamath Database taking into account the interaction of Type Conversion Syntax Axioms with the Notation Syntax Axioms.
  
• ConsolidatedListOfGrammarValidations.html - Grammar validation (edits) performed by mmj2 (see mmj.verify.Grammar.java).
  
• EssentialAmbiguityExamples.html - An interesting exercise in working out ways to create ambiguous grammars in Metamath .mm files. Note: mmj2 has very limited ambiguity checking now -- that is one of the "stubs" left for later due to the great scope and difficulty of the task versus the marginal rewards of this effort (how many people actually invent new .mm databases? See mmj.verify.GrammarAmbiguity.java for more information.) 
  
• CreatingGrammarRulesFromSyntaxAxioms.html - A very involved description of the methods used to generate a Grammar from Metamath Syntax Axioms with particular attention devoted to Nulls Permitted and Type Conversion Syntax Axioms (and combinations thereof).
  
• GrammarRuleTreeNotes.html - This document discusses a method used to build a tree structure containing all grammar rules for a Metamath database. (Note: use of the Earley Parser used now eliminates the need for the "Grammar Rule Tree" except for finding duplicate Grammar Rules -- and that could be done using a java TreeSet, which would eliminate a fair amount of code without appreciably slowing mmj2.verify.Grammar.java.)
  
• EarleyParseFunctionAlgorithm.html - Code level documentation about mmj.verify.EarleyParse.java -- good, but incomplete, was written before the code (specifically, pPredictorTyp and pBringForwardTyp are not discussed in this document, but are mentioned in the "javadoc" comments in mmj.verify.EarleyParse.java.)
  
• EarleyTreeBuilder.html - An attempt to explain the way that a Syntax Tree is constructed from an Earley "Completed Item Sets" data structure. Both tasks are tricky, the 'splaining and the doing. See also mmj.verify.EarleyParse.buildTrees(). One tricky aspect of the tree building operation is that mmj2 allows for production of an unlimited number of parse trees when used with an ambiguous grammar -- and that complicates the algorithm (it was coded twice -- the rewrite happened after an initial recursive method was found to be valid but totally incomprehensible to the original programmer.)
  
• EarleyParseCompletedItemSetsExample.html - Documents the contents of an Earley CompletedItemSet for a hypothetical formula.
  
• ProofAssistant-Unification.txt - Notes about Unification for mmj2 and various approaches to the problem. Written before the code. Contains tree diagram illustrating the geometric approach to understanding unification. This is an interesting topic that is worthy of more investigation. For one thing, the search strategy employed now by mmj2 will benefit from a "rethink" as the size of set.mm doubles and redoubles; a million theorem database would likely increase elapsed time for unification from 1/10th of a second to perhaps 10 seconds! Thus, an alternative, such as a two dimensional search algorithm willbe needed.
• UnificationNotes20060104.txt - Contains a description of the "signature" metrics dynamically computed about theorems and their logical hypotheses. Together these "signatures" enable the mmj2 Unification search algorithm to "fast fail" (reject) candidate assertions for Unification with a given proof step. Instead of having to compare two syntax trees node by node for every proof step and database assertion pair, we compare the two computed signatures -- which are analogous to hash totals, for example. Only candidate assertions that pass the "fast fail" comparison tests need to go through the slow and tedious node-by-node syntax tree comparison process.
• PAFeasibility01RootTotals.txt - Statistics from set.mm as of June, 2005 showing the distribution of Syntax Axioms in set.mm syntax tree root nodes.