mmj2 Export GMMF

[LM]

I am confused how to export proofs so I can include them in my sandbox.mm file (which includes $[ set.mm $] )

My RunParams load syllogism on startup, which is trivially proven by CTRL + U nification

After unification, trying to export it, it errors on the first non hypothesis statement.

Is there some guide or tutorial on exporting proofs to .mm format?

What does GMMF stand for? Did I forget to install something?

Greetings,

Ludwig

[Mázsa Péter]

On Wed, Apr 19, 2023 at 1:49 PM LM <ludwi...@gmail.com> wrote:
> I am confused how to export proofs so I can include them in my sandbox.mm file (which includes $[ set.mm $] )

mmj2 loads your set.mm file: try to edit you local set.mm. When you
are ready with a proof in mmj2, you should format it similarly to what
you see in set.mm.
For example, this proof in mmj2
$( <MM> <PROOF_ASST> THEOREM=dfcnvasymrel4 LOC_AFTER=?
* Alternate definition of the converse asymmetric relation predicate.
(Contributed by Peter Mazsa, 25-Mar-2023.)
50::dfcnvasymrel2 |- ( CnvASymRel R <-> ( ( ( _V X. _V ) \ R ) C_ `'
R /\ Rel R ) )
51::relcnv |- Rel `' R
52::relvvdifss |- ( ( Rel R /\ Rel `' R ) -> ( ( ( _V X. _V ) \
R ) C_ `' R <-> ( R u. `' R ) = ( _V X. _V ) ) )
53:51,52:mpan2 |- ( Rel R -> ( ( ( _V X. _V ) \ R ) C_ `' R <->
( R u. `' R ) = ( _V X. _V ) ) )
54:53:pm5.32ri |- ( ( ( ( _V X. _V ) \ R ) C_ `' R /\ Rel R )
<-> ( ( R u. `' R ) = ( _V X. _V ) /\ Rel R ) )
qed:50,54:bitri |- ( CnvASymRel R <-> ( ( R u. `' R ) = ( _V X.
_V ) /\ Rel R ) )
$= ( wcnvasymrel cvv cxp cdif ccnv wss wrel wa wceq dfcnvasymrel2 wb
cun relcnv relvvdifss mpan2 pm5.32ri bitri ) ABCCDZAEAFZGZAHZIATM
SJZUBIAKUBUAUCUBTHUAUCLANATOPQR $.
$)
should be
$( Alternate definition of the converse asymmetric relation predicate.
(Contributed by Peter Mazsa, 25-Mar-2023.) $)
dfcnvasymrel4 $p |- ( CnvASymRel R <-> ( ( R u. `' R ) = ( _V X. _V
) /\ Rel R ) ) $=
( wcnvasymrel cvv cxp cdif ccnv wss wrel wa wceq dfcnvasymrel2 wb
cun relcnv relvvdifss mpan2 pm5.32ri bitri ) ABCCDZAEAFZGZAHZIATMSJ
ZUBIAKUBUAUCUBTHUAUCLANATOPQR $.
at the end of your local set.mm .
This must solve some of your problems.

P.

[LM]

Thanks!

Yes I also just discovered the MMT functionality, so I can set a folder and I don't need to edit anything manually.

The menu "TL"->"Unify+Store in MMT folder"  apparently emits a directly suitable MMT file, which I just append with "cat myMMT/theproof.mmt >> Sandbox.mm"

Sandbox.mm was initially just an empty file with "$[ Sandbox.mm $]"

It took me a while to figure out...

Thanks for your help!

Ludwig

Op woensdag 19 april 2023 om 15:13:40 UTC+2 schreef Peter Mazsa:

[LM]

Correction, the Sandbox.mm includes set.mm:

...

Sandbox.mm was initially just an empty file with "$[ set.mm $]"

...

Op woensdag 19 april 2023 om 16:22:24 UTC+2 schreef LM: