Le 23/01/2020 à 05:39, Thierry Arnoux a écrit :
Very interesting!
It's nice to see that apart from entering the input at the very
beginning, and apart from the substitutions, you only deal with the
graphical display of the equations.
Do you have any idea how the last use of dummy variables (v1c, v3c),
for substitutions, could be eliminated?
Yes. There is no reason a computer would need 3 substitutions when a
human only uses 1 + mechanical computation.
That is, when you shift an index in a sum, you should just need to give
the amount of shifting
It should be possible to make Mephistolus accomplish this by having it
analyze the hypotheses of a theorem,
find the ones where a substitution or a computation happens to define
another substitution
and only ask for the values needed to infer other substitutions
automatically
That's my plan
I wonder what is the operation "order" towards the top of the list,
which results in "0". Does it mean it cannot be applied?
It is a dud : as I rushed to build mephistolus 6, I display the actions
that could, eventually, be applied to get a mutation
but, as of now, some operations don't work (because hypotheses are
missing or false) or cannot be made to work by himself by mephistolus
(require human help).
Also, I did not filter out some properties, like transitivity, that
populate the action menu with lots of irrelevant possibilities (most of
the time)
Could you then simply omit to list it?
Yes. Next time, I'll do a better job about it :
I'll filter out the garbage, show working operations (or show
potentially working operations tagged with the need for human help),
order the actions with respect to some better category (theorems that
move stuff around (like commutativity), ...) and with some relevance
score (like proximity from the goal, or like less complexity
I mean if you have |- a = b, most of the time, you don't want to have |-
a = b + 0 or |- a = ( b x. 1 ) next
Of course an interesting topic to discuss is the choice of when/where
to add parenthesis, we had an extensive discussion about this when I
introduced the
when you introduced the ?
May I have a link to this discussion (this interests me a lot, as you
can guess).
In the mean time, I'll dig into the metamath discussions, Thierry Arnoux
posts to try to find clues about that
I saw some cases where it seems to be they can obviously be removed,
like in " ( k e. ( { A ... B } ) ) " at 2:10. That's parenthesis where
even set.mm does not have any! ;-)
Yes ^^ :) lol
I have only just started removing useless parenthesis
(like 4 days ago and this is my first try)
I basically walk the tree structure for a metamath statement and, for
each pair of (child, parent),
I decide if the child needs a parenthesis.
There are quite a lot of things that can be done with that.
I mostly look :
- if the child has at least 2 children
- if the child operation priority is less than the parent operation
priority
at the moment, with only partial coverage of the operators I use.
So, there are still parentheses that can be removed (around sums also)
Thanks for the feedback and the pointer (I'll go start looking for your
posts now)
Best regards,
Olivier
On 22/01/2020 05:24, Olivier Binda wrote:
Mephisolus reached Milestone 6
Here is a video, proving that it did :
https://www.youtube.com/watch?v=HuLFpQxwkmU&feature=youtu.be
It shows me a bit stressed (this was my fith attempt, there is always
something going wrong... :) and struggling at the end with html ^^;
Sadly, the exported metamath proof had an issue (I store metamath
theorem with some renaming/shuhhling of variables and It messed up
the exported proof).
I'll fix it at soon as possible and hopefully post a valid exported
proof.
I'm quite happy with the result : it ended up a bit better that I
envisionned and, I already have quite a few ideas about how to
further enhance the user workflow and make it much better.
Hoping to get some feedback now :)
And preparing to start development of Mephistolus Milestone 7...
Best regards,
Olivier
--
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]
<mailto:[email protected]>.
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/af959f49-b997-48f3-9ae8-8705f04da967%40googlegroups.com
<https://groups.google.com/d/msgid/metamath/af959f49-b997-48f3-9ae8-8705f04da967%40googlegroups.com?utm_medium=email&utm_source=footer>.
--
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/d8dc6db1-3af2-e0ac-0448-0ddae3c6ff12%40gmail.com.
