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/86b8b35a-cc1a-4fbb-b10e-a7af392cbbde%40googlegroups.com.
