-
Notifications
You must be signed in to change notification settings - Fork 26
/
mmj2.html
286 lines (286 loc) · 14.5 KB
/
mmj2.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
<!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>mmj2.html</title>
</head>
<body style="color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);"
vlink="#ff0000" alink="#000088" link="#0000ff">
<pre style="font-weight: bold;"><big><big><big><big><span
style="text-decoration: underline;">mmj2 - 01-Nov-2011 Release</span><br></big></big></big></big><br></pre>
<small style="font-weight: bold;"><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>
<span style="font-weight: normal;"></span></code></small>
<br>
The mmj2.zip download is available at:<br>
<br>
<a href="http://us2.metamath.org:8888/ocat/mmj2/">http://us2.metamath.org:8888/ocat/mmj2/</a><br>
<span style="font-family: monospace;"><span
style="text-decoration: underline;"><br>
</span></span>The links on this page point to documents contained in
the unzipped "<code>mmj2</code>"
directory.<br>
<h3><span style="font-weight: normal;">General Documentation:<a
href="README.html"><br>
</a>
</span></h3>
<ul>
<li><a href="QuickStart.html">QuickStart.html</a> - How to install
and start-up mmj2 for the first time<br>
</li>
<li><a href="README.html">README.html</a> - Information about mmj2,
its status, acknowledgements, etc.</li>
<li><a href="doc/PAUserGuide/Start.html">doc\PAUserGuide\start.html</a>
- Proof Assistant User Guide.</li>
<li><a href="LICENSE.TXT">LICENSE.TXT</a> - GNU GENERAL PUBLIC
LICENSE Version 2, June 1991<br>
</li>
<li><a href="INSTALL.html">INSTALL.html</a> - Detailed instructions
for installing mmj2 and taking the next step...<br>
</li>
<li><a href="SunJavaTutorialLicense.html">SunJavaTutorialLicense.html</a>
- Sun Microsystems license requirements (included because
mmj.pa.ProofAsstGUI.java<br>
has several snippets of code that are very similar, if not identical to
snippets of code in the Java Tutorial.) </li>
<li><a href="CHGLOG.TXT">CHGLOG.TXT</a> - Log of mmj2 changes,
sequenced by software release.<br>
</li>
</ul>
<span style="font-family: mon;"></span><span
style="font-weight: normal;"></span><br>
<h3><span style="font-weight: normal;">User Documentation:</span></h3>
<ul>
<li><a href="doc/PAUserGuide/Start.html">doc\PAUserGuide\start.html</a>
- 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.</li>
<li><a href="mmj2jar/mmj2PATutorial.bat">mmj2jar\mmj2PATutorial.bat</a>
- Interactive tutorial that uses the mmj2 Proof Assistant and a set of
valid Proof Worksheets containing instructional text.</li>
<li><a href="data%5Crunparm%5Cwindows%5CAnnotatedRunParms.txt">data\runparm\windows\AnnotatedRunParms.txt</a>
- 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. </li>
<li><a href="mmj2jar/RunParms.txt">mmj2jar\RunParmsComplete.txt</a>
- 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.)<br>
</li>
<li><a href="doc/ProofAssistantGUIQuickHOWTO.html">doc\ProofAssistantGUIQuickHOWTO.html</a>
- Brief overview on the use of the Proof Assistant GUI program.<br>
</li>
<li>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.<br>
</li>
<li><a href="doc/ProofAssistantGUIDetailedInfo.html">doc\ProofAssistantGUIDetailedInfo.html</a>
- 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...<br>
</li>
<li><a href="doc/ProofAsstGUICursorHandling.html">doc\ProofAsstGUICursorHandling.html</a>
- 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 :)</li>
<li><a href="doc/TheoremLoaderOverview.html">doc\TheoremLoaderOverview.html</a>
- Information about the new (1-Aug-2008 release) Theorem Loader
enhancement (plus some info about the new "mmj2 Service" feature!)<br>
</li>
<li><a href="doc/TextModeFormulaFormatting.html">doc\TextModeFormulaFormatting.html</a>
- 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.)</li>
<li><a href="doc/GMFFDoc">doc\GMFFDoc\*</a> - A set of folders and
files that document the GMFF -- Graphics Mode Formula Formatting --
(i.e. html) feature. <br>
</li>
<li><a href="doc/StepUnifier.html">doc\StepUnifier.html</a> -
Somewhat technical, but with lots of diagrams and examples,
StepUnifier.html explains unification from the perspective of mmj2. <br>
</li>
<li><a href="doc/WorkVariables.html">doc\WorkVariables.html</a> -
Explains the new Work Variables used in mmj2!</li>
<li><a href="doc/StepSelectorSearch.html">doc\StepSelectorSearch.html</a>
- Documentation of the new Unify menu item on the Proof Assistant GUI.</li>
<li><a href="doc/UnifyEraseAndRederiveFormulasFeature.html">doc\UnifyEraseAndRederiveFormulasFeature.html</a>
- Documentation of the new Unify menu item on the Proof Assistant GUI.<br>
</li>
<li><a href="doc/BottomUpProving-ByNormMegill.html">doc\BottomUpProving-ByNormMegill.html</a>
- 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.<br>
</li>
</ul>
<br>
<br>
<h3><span style="font-weight: normal;">Technically-Oriented (Programmer
stuff) Documentation:</span></h3>
<ul>
<li><a href="doc/MMJ2DirectoryStructure.txt">MMJ2DirectoryStructure.txt</a>
- The hierarchy of directories contained in mmj2.zip.<br>
</li>
<li><a href="doc/RunningTheMMJ2TestSuite.html">RunningTheMMJ2TestSuite.html</a>
- Cookbook for running the built-in mmj2 tests used to verify each new
mmj2 software release.</li>
<li>doc\mmj2Service\ -- The mmj2 Service feature with samples
invoking mmj2 using the "mmj2 Service" feature.<br>
</li>
<li><a href="doc/MetamathERNotes.html">MetamathERNotes.html</a>
- 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 :)<br>
</li>
<li><a href="doc/mmjProofVerification.html">mmjProofVerification.html</a>
- 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, "<code>a1i</code>", 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!!!) <br>
</li>
<li><a href="doc/BasicsOfSyntaxAxiomsAndTypes.html">BasicsOfSyntaxAxiomsAndTypes.html</a>
- Introductory information about Metamath Syntax Axioms and Type Codes.<br>
</li>
<li><a href="doc/SyntaxAxiomRulesAndConventions.html">SyntaxAxiomRulesAndConventions.html</a>
- More about Syntax Axioms plus "The (Previously) Unwritten Rules for
Syntax Axioms".<br>
</li>
<li><a href="doc/ExampleMetamathDatabase.html">ExampleMetamathDatabase.html</a>
- Extensively annotated Metamath file showing syntax declarations.<br>
</li>
<li><a href="doc/ExampleMetamathGrammar.html">ExampleMetamathGrammar.html</a>
- 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.<br>
</li>
<li><a href="doc/ConsolidatedListOfGrammarValidations.html">ConsolidatedListOfGrammarValidations.html</a>
- Grammar validation (edits) performed by mmj2 (see <code>mmj.verify.Grammar.java</code>).<br>
</li>
<li><a href="doc/EssentialAmbiguityExamples.html">EssentialAmbiguityExamples.html</a>
- 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 <code>mmj.verify.GrammarAmbiguity.java</code>
for more information.) <br>
</li>
<li><a href="doc/CreatingGrammarRulesFromSyntaxAxioms.html">CreatingGrammarRulesFromSyntaxAxioms.html</a>
- 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).
<br>
</li>
<li><a href="doc/GrammarRuleTreeNotes.html">GrammarRuleTreeNotes.html</a>
- 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 <code>mmj2.verify.Grammar.java</code>.)<br>
</li>
<li><a href="doc/EarleyParseFunctionAlgorithm.html">EarleyParseFunctionAlgorithm.html</a>
- Code level documentation about <code>mmj.verify.EarleyParse.java</code>
-- 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 <code>mmj.verify.EarleyParse.java</code>.)<br>
</li>
<li><a href="doc/EarleyTreeBuilder.html">EarleyTreeBuilder.html</a>
- 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 <code>mmj.verify.EarleyParse.buildTrees()</code>.
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.)<br>
</li>
<li><a href="doc/EarleyParseCompletedItemSetsExample.html">EarleyParseCompletedItemSetsExample.html</a>
- Documents the contents of an Earley CompletedItemSet for a
hypothetical formula. <br>
</li>
<li><a href="doc/ProofAssistant-Unification.txt">ProofAssistant-Unification.txt</a>
- 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. </li>
<li><a href="doc/UnificationNotes20060104.txt">UnificationNotes20060104.txt</a>
- 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.</li>
<li><a href="doc/PAFeasibility01RootTotals.txt">PAFeasibility01RootTotals.txt</a>
- Statistics from set.mm as of June, 2005 showing the distribution of
Syntax Axioms in set.mm syntax tree root nodes. <br>
</li>
</ul>
<br>
<br>
<br>
<br>
<br>
<br>
<br>
<br>
<br>
<br>
<br>
<br>
<big><big><small><small><br>
<span style="font-style: italic;"></span></small></small></big></big>
</body>
</html>