mmj2 Proof Assistant GUI

mmj2 Proof Assistant GUI

(back to Start.html)

Here is a mock-up of the Proof Assistant GUI screen:

ProofAsstGUI X

File Edit Cancel Unify Help

$( <MM> <PROOF_ASST> THEOREM=a1i LOC_AFTER=?

* Inference derived from axiom ~ ax-1 . See ~
a1d for an explanation of our informal use of
the terms "inference" and "deduction".

h1::a1i.1          |- ph
2::ax-1            |- ( ph -> ( ps -> ph ) )
qed:1,2:ax-mp      |- ( ps -> ph )

$= wph wps wph wi a1i.1 wph wps ax-1 ax-mp $.
$)

The Proof Assistant GUI allows users to enter, update, validate, unify and browse Proof Worksheets.

Key points to understand about this screen:

The GUI is displayed only if the input Metamath .mm database file is loaded and parsed successfully, with no serious errors.
The data area (under the menu) consists of one large text area. The GUI program has no knowledge of what is in the text, and knows nothing about math or logic. It is basically just a text editor with connections to other programs, and it relays all processing requests to the (server) main Proof Assistant program. (Eventually a more sophisticated and graphically oriented GUI may be coded.)
When the Proof Assistant GUI sends a processing request for the proof on the screen, such as "Unify/Unify (check proof)" to the main (server) Proof Assistant program, the entire Proof Worksheet is parsed and re-validated before satisfying the request. The system doesn't keep memory about the contents of the Proof Worksheet between requests -- that means that you could completely replace the contents of the screen (Cut and Paste), and select "Unify/Unify (check proof)" to unify a completely different proof. It also means that a serious error in the Proof Worksheet will halt processing and your request to renumber or unify the proof will not be processed (until the error is corrected.)
Errors and informational messages are displayed on a pop-up "Request Messages" window (seen below). Hint: alt-Tab carefully back to the ProofAsstGUI window -- the cursor should be positioned very close to the first error in the Proof Worksheet.

Request Messages X

Edit

E-PA-0410
Theorem welcome Step qed: Unification failure in derivation proof
step.ax-2. The step's formula and/or its hypotheses could not be
reconciled with the referenced Assertion. A list of unifying assertion
alternates (if any) will be presented in a subsequent message.

 --------------------------------------------------------- 

      

I-PA-0402 Theorem welcome Step qed: Alternate unification Ref assertions found: ax-1

 ---------------------------------------------------------

There is a lot of helpful information related to the Proof Assistant GUI here:

mmj2jar\mmj2PATutorial.bat - Interactive tutorial that uses the mmj2 Proof Assistant and a set of valid Proof Worksheets containing instructional text.
doc\ProofAssistantGUIQuickHOWTO.html - Brief overview on the use of 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...

(back to Start.html)