README

//********************************************************************/
//* Copyright (C) 2005 thru 2011                                     */
//* MEL O'CAT : x178g243 at yahoo.com                                */
//* License terms: GNU General Public License Version 2              */
//*                or any later version                              */
//********************************************************************/
//*4567890123456 (71-character line to adjust editor window) 23456789*/

As Of 1-Nov-2011

For Info about the latest release features click on:

• CHGLOG.TXT
• mmj2CommandLineArguments.html
• mmj2\doc\GMFFDoc*
• mmj2.html

See also: QuickStart.html and README.html

---

You can now support mmj2 development with $$$ donations via Paypal to siskiyousis at gmail.com!

And, for questions, bugs, enhancements, etc. contact Mel at X178G243 at yahoo.com

---

-----------------------------------------------------------------
Quick Start CHEAT SHEET!!!  (see also QuickStart.html)
-----------------------------------------------------------------   

   Quick Start!!!:
  
   Windows:  Double-click mmj2jar\mmj2.bat in Windows Explorer
  
   Mac OS-X: Double-click mmj2jar\MacMMJ2.command in Finder

   BUT...WAIT!...before running mmj2, edit, if needed:

   EDIT-->Windows    mmj2jar\RunParms.txt
          using      mmj2jar\mmj2.bat
          Notepad:   mmj2jar\mmj2PATutorial.bat

       -->Mac OS-X   mmj2jar\RunParms.txt
          using      mmj2jar\MacRunParmsPATutorial.txt                
          TextEdit:  mmj2jar\MacMMJ2.command
                     mmj2jar\MacMMJ2PATutorial.command

   (Double-click works well now because the new "mmj2 Fail Popup
   Window" *not only* provides start-up and "fail" error
   messages, but it also forces the Windows Command Prompt (Mac
   OS-X utilities terminal.app) window to stay open, which makes
   it possible to see all of the mmj2 output about the error.)

---

0. mmj2 The key idea of mmj2 and its Proof Assistant -- why you want it --  is that it has a "GUI" Proof Assistant which is said to be much easier to use than Metamath.exe.

mmj2 provides a set of tools designed for use with Metamath.exe and its associated utilities, such as eimm.exe (Import/Export mmj2 Proof Worksheet). In addition to the new and improved mmj2 Proof Assistant GUI -- by far, the most interesting and useful part of mmj2 -- the mmj2 software package provides capabilities such as validation of .mm files; proof verification; grammatical/syntax analysis of .mm files; printing; Text Mode Formula Formatting ("TMFF"), a novel "pretty printing" feature that may facilitate comprehension of complicated math and logic formulas written in Metamath's ASCII shorthand; and MUCH MORE...

1. Installation: Refer to INSTALL.html for instructions on installing and taking the next steps to run and use mmj2. Then visit or return to mmj2.html to see the other documentation, such as the mmj2 Proof Assistant User Guide. Once you have installed mmj2 be sure to try the interactive mmj2 Proof Assistant Tutorial (which ought to take about an hour.)

2. Requirements:

• You should have a modern PC or Mac/Unix/Linux computer with at least 2GB of memory and a good, fast hard drive for a good experience using mmj2, which is a bit of a memory hog and is processor-intensive after start-up. mmj2, like Metamath.exe, loads an entire Metamath .mm database (file) into memory (and then does an unbelievable amount of computation!)
• You will also need Sun Microsystem's Oracle's Java, either the Java Development Kit (JDK aka "J2SE") or the Java Runtime Environment (JRE), version 1.5 or higher.
• Metamath itself, is technically speaking, optional, but in practice a necessity because mmj2 is an add-on, complementary toolkit for Metamath.
• An excellent text editor capable of handling large files and Unix-style line endings (even in Windows) is a necessity. See INSTALL.html for additional info about this.
• A file compression utility such as 7-Zip.

3. Limitations: mmj2 is still in "developmental" status, meaning that it is subject to change, bug fixes and continuing enhancements...at the whim of Mel L. O'Cat (If you don't like the changes you can clone mmj2 under the GNU GENERAL PUBLIC LICENSE and write your own code.) There is NO WARRANTY -- see LICENSE.TXT (GNU GENERAL PUBLIC LICENSE Version 2, June 1991). Use at your own risk. (In any case, you are strongly urged to always backup your data; to secure your machine from hackers and viruses, whether or not you use mmj2; to feed your PC only clean electricity from a battery-powered UPS; and ... to always remember that the only secure computer is one that is unplugged, re-packed in its original shipping container, and safely stacked in a secure warehouse. I recommend using a firewall such as Norton which allows you to specify which programs are allowed to access the internet -- and then to block Java from internet access...better yet, disconnect your computer from the internet while you are using mmj2 :-) Better safe than sorry!)

4. Opportunities: mmj2 was begun as an experimental study of Metamath, and development has proceed in stages, with each new enhancement package designed to be as modular and independent from the others as possible. These developmental stages -- from .mm database validation and printing, proof verification, grammatical analysis, "proof assistanting", Text Mode Formula Formatting, etc. -- have advanced the state of  the art of Metamath programming by a small amount and provide a foundation for further work. mmj2 is now usable (and almost good enough to throw away and rewrite properly!) But there is still more work, more experimentation and more learning to be done. 

mmj2's capabilities are invoked using "RunParm" commands that form a language, albeit without looping or "if" statements. Thus, it is easy to enhance and extend mmj2, even for "one offs": code a new program, a new "RunParm" command or two, and modify the mmj.util.BatchMMJ2.java program, and one can immediately gain programmatic access to a fully parsed, proof-verified Metamath database loaded into memory and ready for use. (Note: the MMJ2 Service Feature allows your program to call mmj2 or to be called by mmj2.)

5. Shortcomings of mmj2:

• It is not a "prover".
• It does not update Metamath .mm databases.
• Its grammatical analysis module does minimal checking for grammatical ambiguity (this section is stubbed out -- very difficult, requiring lots of work in special cases because the general case is impossible to prove :).
• It is a single-user system, not designed for concurrent access throughout (but you can run more than one instance of mmj2's Proof Assistant GUI simultaneously.)
• All messages are output in English.
• All output is left-to-right.
• Support for Unicode or non-ASCII input/output is minimal.
• Metamath RPN-format proofs are only output in the Metamath uncompressed format.
• Severe data validation errors encountered during start-up, such as a Metamath .mm database parse error produce error messages on the operating system Command Prompt window, as well as the mmj2 Fail Popup Window -- and when you click "ok", processing terminates immediately. Unfortunately, some users will find these messages hard to decipher.
• A redesign could make better use of the various Metamath software "objects". To a great extent the "objects" are treated mostly as information hiders and as a way to package program functions written "old school" style.
• The mmj2 object hierarchy -- Stmt <- Hyp < VarHyp, etc. --  has proven to be resilient and extensible. However, it is clear the Axiom should be subclassed with SyntaxAxiom (and perhaps Definition!), which could easily be accomplished if we knew the grammatical Type Codes at file load time. Also, Proof should be an object in its own right. (Other design decisions are dubious and/or debatable.)
• mmj.verify.GRForest.java and GRNode.java can be replaced with a Java TreeSet (they are no longer needed except for duplicate checking now that the Earley Parse algorithm is in use.) Plus mmj.verify.BottomUpParser.java can be eliminated without loss.
• Unification in the mmj2 Proof Assistant depends upon there being a single, unique syntax tree for each valid expression. Grammatical productions intended to support things like "x + y + z" in an unambiguous manner may possibly be defined away using "Syntax Proofs", but little work has been done in this area beyond dealing with weq/wceq, etc. in set.mm for the mmj2 Proof Assistant project (see BasicsOfSyntaxAxiomsAndTypes.html).

6. Next Steps, Possible Enhancements, and Experimental Topics:

• Enhance the mmj2 Service Feature by adding a Ctrl key on the mmj2 Proof Assistant GUI screen to invoke the current mmj2 Service program (plug-in) program, passing the proof worksheet as input. Upon return from the invoked program, the mmj2 Proof Assistant GUI would unify the (possibly) modified proof worksheet and display the results. The would be one way to connect mmj2 and a user-written step "prover" (or other useful proof modifier).
• ?

7. Acknowledgements:

• Norman Megill, Legendary Inventor of Metamath
• Raph Levien, Inventor of mmverify.py and Ghilbert
• Robert M. Solovay, Author of peano.mm
• Dick Grune and Ceriel J.H. Jacobs, Authors of "Parsing Techniques - A Practical Guide"
• Aaron Krowne and Joe Corneli, PlanetMath, the original sponsors of mmj2
• Herbert B. Enderton, Author of "A Mathematical Introduction to Logic" (1972, Academic Press)
• http://www.math.ucla.edu/~hbe/amil/index.html
• Richmond H. Thomason, Author of  "Symbolic Logic, An Introduction" (1970, Macmillan)
• Professor Vann McGee, MIT Open Courseware, Logic I
• Michael Beeson, Explainer Extraordinaire of Unification
• Alin Suciu, Yet Another Efficient Unification Algorithm
• F. Line, Paul Chapman and many others who provided analysis, feedback, ideas, review and/or testing.
• Sci-Fi Inspiration: Greg Egan, "Diaspora"; Charles Stross, "Accelerando"; Bruce Sterling, "Distraction"; Neal Stephenson, "Snow Crash"; and Robert Heinlein, "Gulf".
• Everyone else I forgot to list. Thanks!