forked from digama0/mmj2
-
Notifications
You must be signed in to change notification settings - Fork 0
/
README.html
446 lines (425 loc) · 20 KB
/
README.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
<head>
<meta content="text/html; charset=ISO-8859-1"
http-equiv="content-type">
<title>README</title>
</head>
<body style="color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);"
vlink="#ff0000" alink="#000088" link="#0000ff">
<small><code>//********************************************************************/<br>
//* Copyright (C) 2005 thru 2011
*/<br>
//* MEL O'CAT : x178g243 at yahoo.com
*/<br>
//* License terms: GNU General Public License Version
2
*/<br>
//*
or
any
later
version
*/<br>
//********************************************************************/<br>
//*4567890123456 (71-character line to adjust editor window) 23456789*/<br>
</code></small><br>
<h3>As Of 1-Nov-2011</h3>
<br>
<big style="font-weight: bold;">For Info about the latest release
features click on:<br>
</big>
<ul>
<li><big style="font-weight: bold;"><a href="CHGLOG.TXT">CHGLOG.TXT</a></big></li>
<li><big style="font-weight: bold;"><a
href="doc/mmj2CommandLineArguments.html">mmj2CommandLineArguments.html
</a></big></li>
<li><big style="font-weight: bold;"><a href="doc%5CGMFFDoc">mmj2\doc\GMFFDoc\*</a></big></li>
<li><big style="font-weight: bold;"><a href="mmj2.html">mmj2.html</a>
</big></li>
</ul>
See also: <big><a style="font-weight: bold;" href="QuickStart.html">QuickStart.html</a></big>
And
<big style="font-weight: bold;"><a href="README.html">README.html</a></big><br>
<br>
<hr style="width: 100%; height: 2px;"><br>
<big><span
style="font-weight: bold; font-style: italic; color: rgb(0, 153, 0);">You
can
now
support
mmj2
development
with
$$$ donations via Paypal to siskiyousis at gmail.com!<br>
<br>
<span style="color: rgb(204, 0, 0);">And, for questions, bugs,
enhancements, etc. contact Mel at X178G243 at yahoo.com</span></span><br
style="font-weight: bold; font-style: italic; color: rgb(0, 153, 0);">
</big><big style="font-weight: bold;"><br>
</big><big style="font-weight: bold;"><span
style="font-family: monospace; color: rgb(0, 102, 0);"></span></big>
<hr style="width: 100%; height: 2px;"><big style="font-weight: bold;"><span
style="font-family: monospace; color: rgb(0, 102, 0);">
-----------------------------------------------------------------</span><br
style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">
Quick
Start CHEAT SHEET!!! (see also mmj2\QuickStart.html)</span><br
style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">
-----------------------------------------------------------------
</span><br style="font-family: monospace; color: rgb(0, 102, 0);">
<br style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">
Quick
Start!!!:</span><br
style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">
</span><br style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">
Windows:
Double-click <code>mmj2\mmj2jar\mmj2.bat</code> in
Windows Explorer</span><br
style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">
</span><br style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">
Mac
OS-X: Double-click mmj2\mmj2jar\MacMMJ2.command in Finder</span><br
style="font-family: monospace; color: rgb(0, 102, 0);">
<br style="font-family: monospace; color: rgb(0, 102, 0);">
<br style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">
BUT...WAIT!...before
running mmj2, edit, if needed:</span><br
style="font-family: monospace; color: rgb(0, 102, 0);">
<br style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">
EDIT-->Windows
mmj2\mmj2jar\RunParms.txt</span><br
style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">
using
mmj2\mmj2jar\mmj2.bat</span><br
style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">
Notepad:
mmj2\mmj2jar\mmj2PATutorial.bat</span><br
style="font-family: monospace; color: rgb(0, 102, 0);">
<br style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">
-->Mac
OS-X mmj2\mmj2jar\RunParms.txt</span><br
style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">
using
mmj2\mmj2jar\MacRunParmsPATutorial.txt
</span><br style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">
TextEdit:
mmj2\mmj2jar\MacMMJ2.command</span><br
style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">
mmj2\mmj2jar\MacMMJ2PATutorial.command</span><br
style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);"> </span><br
style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">
(Double-click
works well now because the new "mmj2 Fail Popup</span><br
style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">
Window"
*not only* provides start-up and "fail" error</span><br
style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">
messages,
but it also forces the Windows Command Prompt (Mac</span><br
style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">
OS-X
utilities\terminal.app) window to stay open, which makes</span><br
style="font-family: monospace; color: rgb(0, 102, 0);">
<span style="font-family: monospace; color: rgb(0, 102, 0);">
it
possible to see all of the mmj2 output about the error.)</span></big><big
style="font-weight: bold;"><br>
</big>
<hr style="width: 100%; height: 2px;"><big style="font-weight: bold;"><br>
0.</big> <span style="font-weight: bold;">mmj2</span>
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.<br>
<br>
mmj2 provides a set of tools designed for use <span
style="font-style: italic;">with</span> <code>Metamath.exe</code> and
its
associated utilities, such as <code>eimm.exe</code>
(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<span
style="font-weight: bold;"> MUCH MORE...<br>
<br>
</span><big style="font-weight: bold;">1.</big> <span
style="font-weight: bold;">Installation:</span> Refer
to <a href="INSTALL.html">INSTALL.html</a> for
instructions on installing and taking the next steps to run and use
mmj2. Then visit or return to <a href="mmj2.html">mmj2.html</a> to see
the other documentation,
such as the <a href="doc/PAUserGuide/Start.html">mmj2 Proof Assistant
User Guide</a>. Once you have installed mmj2 be sure to try the
interactive <a href="mmj2jar/mmj2PATutorial.bat">mmj2
Proof
Assistant
Tutorial</a> (which ought to take about an hour.)<br>
<br>
<br>
<big><span style="font-weight: bold;">2.</span></big> <span
style="font-weight: bold;">Requirements:</span> <br>
<ul>
<li>You should have a modern PC or Mac/Unix/Linux computer with at
least <span style="text-decoration: underline;">2GB of memory</span>
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!)</li>
<li>You will also need <span style="text-decoration: line-through;">Sun
Microsystem's</span> Oracle's <span style="text-decoration: underline;">Java</span>,
either
the
Java
Development
Kit
(<span style="text-decoration: underline;">JDK</span>
aka "J2SE") <span style="text-decoration: underline;">or</span> the
Java Runtime Environment (<span style="text-decoration: underline;">JRE</span>),
version
<span style="text-decoration: underline;">1.5 or higher</span>.</li>
<li><span style="text-decoration: underline;">Metamath</span>
itself, is technically speaking, optional, but in practice a necessity
because mmj2 is an add-on, complementary toolkit for Metamath.</li>
<li>An excellent <a href="http://www.textpad.com/"><span
style="text-decoration: underline;">text
editor</span></a> capable of handling large files and Unix-style
line endings (even in Windows) is a necessity. See <a
href="INSTALL.html">INSTALL.html</a> for additional info about
this.</li>
<li>A file compression utility such as <a
href="http://www.7-zip.org/">7-Zip</a>.<br>
</li>
</ul>
<br>
<big style="font-weight: bold;">3.</big> <span
style="font-weight: bold;">Limitations:</span> 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.) <span
style="font-weight: bold; font-style: italic; text-decoration: underline; color: rgb(153, 0, 0);">There
is
NO
WARRANTY</span>
-- see <a href="LICENSE.TXT">LICENSE.TXT</a> (GNU GENERAL PUBLIC
LICENSE Version 2, June 1991). Use at your own risk. (In any case, you
are <span style="text-decoration: underline;">strongly</span> urged to
always backup your data; to secure your machine from hackers and
viruses, <span style="text-decoration: underline;">whether or not</span>
you use mmj2; to feed your PC only clean electricity from a
battery-powered UPS; <span style="font-style: italic;">and</span> ...
to <span style="font-style: italic;">always</span>
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 <a
href="http://us.norton.com/internet-security/">Norton</a> 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!)<br>
<br>
<br>
<big style="font-weight: bold;">4.</big> <span
style="font-weight: bold;">Opportunities:</span>
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. <br>
<br>
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 <a href="doc%5Cmmj2service">MMJ2 Service</a>
Feature allows your program to call mmj2 or to be called by mmj2.)<br>
<br>
<br>
<big><span style="font-weight: bold;">5.</span></big> <span
style="font-weight: bold;">Shortcomings of mmj2:</span><br>
<ul>
<li>It is not a "prover".</li>
<li>It does not update Metamath .mm databases.</li>
<li>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 :).</li>
<li>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.)<br>
</li>
<li>All messages are output in English.<br>
</li>
<li>All output is left-to-right.</li>
<li>Support for Unicode or non-ASCII input/output is minimal.</li>
<li>Metamath RPN-format proofs are only output in the Metamath
uncompressed format.</li>
<li>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.<br>
</li>
<li>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.</li>
<li>The mmj2 object hierarchy -- <code>Stmt <- Hyp < VarHyp</code>,
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.)<br>
</li>
<li><code>mmj.verify.GRForest.java</code> and <code>GRNode.java</code>
can be replaced with a Java <code>TreeSet</code> (they are no longer
needed except for duplicate checking now that the Earley Parse
algorithm is in use.) Plus<code> mmj.verify.BottomUpParser.java</code>
can be eliminated without loss. <br>
</li>
<li>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 <a
href="doc/BasicsOfSyntaxAxiomsAndTypes.html">BasicsOfSyntaxAxiomsAndTypes.html</a>).</li>
</ul>
<br>
<big><span style="font-weight: bold;">6.</span></big> <span
style="font-weight: bold;">Next Steps, Possible Enhancements, and
Experimental Topics:</span><br>
<br>
<ul>
<li>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).</li>
<li><big style="color: rgb(204, 51, 204);"><big>?</big></big><br>
</li>
</ul>
<br>
<big><span style="font-weight: bold;">7.</span></big> <span
style="font-weight: bold;">Acknowledgements:</span><br>
<ul>
<li>Norman Megill, Legendary Inventor of Metamath [<a
href="http://www.metamath.org">http://www.metamath.org</a>] <br>
</li>
<li>Raph Levien [<a href="http://www.levien.com/">http://www.levien.com/</a>],
Inventor
of
<code>mmverify.py</code> and Ghilbert [<a
href="http://ghilbert.org/">http://ghilbert.org/</a>]</li>
<li>Robert M. Solovay, Author of <code>peano.mm</code> [<a
href="http://math.berkeley.edu/%7Esolovay/">http://math.berkeley.edu/~solovay/</a>]</li>
<li>Dick Grune and Ceriel J.H. Jacobs, Authors of "Parsing Techniques
- A Practical Guide" [<a href="http://www.cs.vu.nl/%7Edick/PTAPG.html">http://www.cs.vu.nl/~dick/PTAPG.html</a>]</li>
<li>Aaron Krowne and Joe Corneli, PlanetMath [<a
href="http://planetmath.org/">http://planetmath.org/</a>], the
original sponsors of mmj2<br>
</li>
<li> Herbert B. Enderton, Author of "A Mathematical Introduction to
Logic" (1972, Academic Press)<br>
</li>
<li> [<a href="http://www.math.ucla.edu/%7Ehbe/amil/index.html">http://www.math.ucla.edu/~hbe/amil/index.html</a>]</li>
<li>Richmond H. Thomason, Author of "Symbolic Logic, An
Introduction" (1970, Macmillan)<br>
</li>
<li>Professor Vann McGee, <a
href="http://ocw.mit.edu/OcwWeb/Linguistics-and-Philosophy/24-241Logic-IFall2002/CourseHome/index.htm">MIT
Open
Courseware,
Logic
I</a></li>
<li>Michael Beeson, Explainer Extraordinaire of Unification [<a
href="http://michaelbeeson.com/research/otter-lambda/index.php?include=Unification">http://michaelbeeson.com/research/otter-lambda/index.php?include=Unification</a>]
<br>
</li>
<li>Alin Suciu, Yet Another Efficient Unification Algorithm [<a
href="http://arxiv.org/pdf/cs/0603080">http://arxiv.org/pdf/cs/0603080</a>]<a
class="url" href="http://arxiv.org/pdf/cs/0603080"><br>
</a></li>
<li>F. Line, Paul Chapman and many others who provided analysis,
feedback, ideas, review and/or testing.<br>
</li>
<li>Sci-Fi Inspiration: Greg Egan, "<a
href="http://gregegan.customer.netspace.net.au/DIASPORA/DIASPORA.html">Diaspora</a>";
Charles
Stross,
"<a
href="http://www.antipope.org/charlie/blog-static/fiction/accelerando/accelerando-intro.html">Accelerando</a>";
Bruce
Sterling,
"<a
href="http://www.amazon.com/Distraction-Bruce-Sterling/dp/0553576399">Distraction</a>";
Neal
Stephenson,
"<a
href="http://www.amazon.com/Snow-Crash-Bantam-Spectra-Book/dp/0553380958">Snow
Crash</a>"; and Robert Heinlein, "<a
href="http://www.amazon.com/Assignment-Eternity-Robert-Heinlein/dp/0671578650">Gulf</a>".</li>
<li>Everyone else I forgot to list. Thanks! <br>
</li>
</ul>
<br>
<br>
<br>
<br>
</body>
</html>