I had to downgrade my requirements for reaching Milestone 5 as I am
entering harder country.
Today I downloaded metamath, compiled it on linux and tried proof checking
Mephistolus proven theorems.
I was successfull with
${
eqEq.1 $e |- ( ph -> ( ps -> ( ka -> ( la <-> rh ) ) ) ) $.
eqEq.2 $e |- ( ph -> ( ps -> ( ka -> ( mu <-> si ) ) ) ) $.
$( (Contributed by Mephistolus, 4-Nov-2019.) $)
eqEq $p |- ( ph -> ( ps -> ( ka -> ( ( la <-> mu ) <-> ( rh <-> si ) )
) ) )
$= wph wps wa wka wla wmu wb wrh wsi wb wb wi wi wph wps wka wla wmu
wb wrh
wsi wb wb wi wi wi wph wps wa wka wa wla wmu wb wrh wsi wb wb wi wph
wps
wa wka wla wmu wb wrh wsi wb wb wi wi wph wps wa wka wa wla wrh wmu
wsi wph
wps wa wka wa wla wrh wb wi wph wps wa wka wla wrh wb wi wi wph wps
wa
wka wla wrh wb wi wi wph wps wka wla wrh wb wi wi wi eqEq.1 wph wps
wka wla
wrh wb wi impexp mpbir wph wps wa wka wla wrh wb impexp mpbir wph wps
wa
wka wa wmu wsi wb wi wph wps wa wka wmu wsi wb wi wi wph wps wa wka
wmu
wsi wb wi wi wph wps wka wmu wsi wb wi wi wi eqEq.2 wph wps wka wmu
wsi wb
wi impexp mpbir wph wps wa wka wmu wsi wb impexp mpbir bibi12d wph
wps wa
wka wla wmu wb wrh wsi wb wb impexp mpbi wph wps wka wla wmu wb wrh
wsi
wb wb wi impexp mpbi
$.
$}
I tried exporting proofs in the compress format, but it is too much a
bother (with floating hypotheses that don't appear in the labels + I got it
working at 90% before I realized that metamath can read uncompressed proofs
and compress them,
which is much easier to do. Besides, computing compressed proofs needs
quite a lot of computations, and processing uncompressed proofs is a lot
easier and faster for mephistolus...So, I gave up on compressed proofs.
Now, I should be able to export Mephistolus proof easily to the set.mm
format and get them proofchecked by a battletested proof checker,in
addition to my own.
Le vendredi 18 octobre 2019 11:21:25 UTC+2, Olivier Binda a écrit :
>
> I do a lot of cow boy coding and nothing is set in stone but :
>
> 1) I would like to start looking into mm0 and building Mephistolus over mm0
> (because at one point, I will want user to be able to add definitions of
> their own and I will need the added soundness, as well as the simpler
> parsing, and maybee other stuff that I don't understand yet)
>
> Also, by building mephistolus on mm and mm0, It'll become more generic and
> probably better (closer to true maths).
>
>
> 2) I need to extend the capacities of Mephistolus
> I couldn't export a few mephistolus theorems to metamath because the
> Mephistolus 4 features wre lacking (regarding location of expression in
> various sets, proving that some stuff is =/= 0 ).
> Exporting them to metamath will drive Mephistolus features developement
>
> Also, Mephistolus only supports a very limited set of operators as of now
> (->, <->, -., +, -, x, /, -u). I need to slowly add more operators (I have
> to rework the quickly hacked sum_ support I had, prod_, forall, exists...)
> to make Mephistolus more useful
>
> 3) Some core Statement api may still be improved
>
> a) I just realized today that I had to enable the user to apply a theorem
> to an equality like in
>
> |- 2 < 3
>
> apply x |-> -u x to get
>
> |- -u 3 < -u 2
>
> We have all used this process so many times that we would miss it if it
> wasn't there...
> I just have to figure out a good way to bake it in
>
>
> b) my current api (with .eq, .imp, .a .b .c ...) is quite nice to work
> with but I got another idea to make it more generic and simpler, I want to
> explore that
>
>
> 4) making metamath theorems available in mephistolus
>
> a) now that I have proved a lot of Mephistolus theorems in metamath, and
> that I know what I am doing, I should write a method to enhance most
> metamath theorems into mephistolus theorems.
> I should be able to convert 10000+ metamath theorems into mephistolus to
> make them available (Mephistolus can, out of the box, use any metamath
> theorem but Mephistolus theorems are a lot better to work with because the
> Mephistolus api is designed to work with them)
>
> b) I should implement something that makes it easy for a user (not me) to
> select a mephistolus theorem
>
> For example, I don't want user to have to learn ids like "ltsubrpd" to be
> able to call |- ( ph -> ( A - B ) < A )
>
> Maybee something like select("a-b<a") where you can select a theorem by
> giving a utf8 string (that's right, NOT ASCII), with alternatives so ascii
> could still be an option
> It doesn't have to be perfect as, later, if there are ambiguities, the api
> would suggest completions
>
> Later on, a database with powerfull full text search/indexing capabilities
> would be used (issue, find a library available in Native, JVM, browser that
> enable that. I have experience with Janusgraph and Lucene on the JVM, but
> they are not multi platform (yet))
> to help with that
>
>
>
> And that is already enough to make Milestone 5 a lot of work, let's end it
> here ^^;
>
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/0b289ae3-7b5f-4a5e-8053-a348d541c7be%40googlegroups.com.
