Hello Filip :)
Le 29/05/2019 à 10:01, 'Filip Cernatescu' via Metamath a écrit :
Hello Olivier!
Good luck with your CAS implementation! It is a wonderful work!
But I have 2 question for you:
1. The proofs of your calculations would be in formal math not in
classic math, do you think that would be a segment of population that
would need your proofs?
The segments of the population that I am targeting are :
-the average math student
-the professional math researcher
Basically, humans would enter the proof either
- through a well thought UI, that looks and behaves as much as it can as
traditional/classic math
(which makes it usable to the average math student).
- optionaly/additionaly, through text input (for power users like
professional mathematicians, they know what they do and it is faster
this way)
Basically, at the moment, it works this way :
You may have hypothesis/antecedent like
x = -2
y e. ZZ
You start with a (valid) math statement like
( x x. ; 1 2 ) + y
and then you may point to (select) parts of the statement and apply
operations
like reduction, commutativity, associativity to transform the Statement
(with theorems the way you want/can) and the api makes sure that, at
then end, you get
- a formal proof of the resulting statement
- a formal proof of the transition
like |- ( x = 1 -> ( y e. ZZ -> ( x x. ; 1 2 ) + y = ; 1 2 + y ) )
It is still a work in progress though. At the moment, I'm refactoring
the api to make it work nicely with antecedents. I have made some
progress but I have still work to do to make
the usual operations (+ - * /) work with rationals AND antecedents,
after which I should get sum, product and function support quite
effortlessly
Once I get that to work, I'll :
1) work on the export step from my theorem format to mm (or mm0 ?).
Because I'm no longer using regular set.mm theorems (got to call too
many of them to handle 1 operation with antecedents)
2) start building a prototype app and a UI :
to allow the first beta users to build formal proofs interactively and
export them to mm (or mm0 ?)
2. Lots of math formulas are non-existent in set.mm,how do you deal
with that?
At the moment, to develop my app,
I'm using my own theorems like this one
val A_plus_0 =tf("( ∨1c + 0 ) = ∨1c", "∨1c e. CC")
tf stands for "theorem family" because it also allows one to use it with
antecedents like
|- ( v2w -> v1c e. CC )
gives
|- ( v2w -> (v1c + 0 ) = v1c )
v1c is for class
v1s for set
v1w for wff
Also, it removes the need for variants for
|- v1c = v2c
|- v3c = v4c
gives
|- ; v1c v3c = v2c v4c
like
|- v1c = v2c
gives
|- ; v1c v3c = v2c v3c
(you have to use such variants to lessen the huge amount of hypothesis
that the system has to prove automatically to use the theorems)
such a theorem family could be easily proven (I believe) with the
theorems that are in set.mm
But mm lacks variadic arguments and it makes it painfull to work with
antecedents, so this is the way I decided to use to work around that (my
app would first create a proof relying on some theorem family and then
it would prove all the specialized theorems it uses)
As soon as I get arithmetic operations to work nicely, I'll post a
progress update
Thank you very much!
Filip
Thank you for the interest :)
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/11dc6086-2cf5-4c81-bcef-e6a58978b234%40googlegroups.com
<https://groups.google.com/d/msgid/metamath/11dc6086-2cf5-4c81-bcef-e6a58978b234%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/fe62112e-0dc3-d2f0-6ca0-9bdb8b8a005d%40gmail.com.
