mmj2 Proof Assistant Proof Worksheet

(back to Start.html)
"Proof Worksheet" refers to the contents of the mmj2 Proof Assistant GUI screen.

Here is what an actual Proof Worksheet looks like after "Unification" (Theorem "a1i" from Metamath's set.mm):
$( <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.

Proof Worksheets can be -- usually are -- stored in text files with file type ".txt" or ".mmp".

A valid Proof Worksheet has the format of a Metamath "Comment" -- the first line of a Proof Worksheet begins with "$(" and the last line begins with "$)". In theory a Proof Worksheet could be copied into a Metamath .mm database file and cause no errors, although this would be counter-productive if you had thousands of Proof Worksheets in your Metamath file!

Unfortunately, the mmj2 Proof Assistant does not directly update Metamath .mm database files at this time. So the Metamath RPN-format proofs created using the mmj2 Proof Assistant must be manually copied into the Metamath .mm database file, and for new theorems to become visible in mmj2, the mmj2 Proof Assistant must be restarted.

Note: Metamath's "eimm.exe" utility exports and imports Metamath proofs to and from Proof Worksheet files. Refer to the documentation at www.metamath.com for details.

There is a lot of helpful information related to  Proof Worksheets here:
 
(back to Start.html)