Are Automated theorem provers really useful to help students to know and understand how to proof? Is there any research about it?
"...assuming you can find one!..."
I don't get it, really. Are you wanna say that there is no such thing like automated theorem prover? or are you wanna say that automated theorem prover has no benefit for mathematics education?
If you say that I can't find one such thing like automated theorem prover, yeah you're so true, because I find MANY of them, not just one.
http://en.wikipedia.org/wiki/Automated_theorem_proving
It shock me when I check you are PhD from School of Computer Science but (pardon me) have no little knowledge about Automated Theorem Prover (ATP). As your information I'm still undergraduate student in mathematics department and I hear about ATP a lot.
The problem is I don't know what is the benefit of these thing for mathematics education.
Ah... I get the point now.
# "... the output is incomprehensible to a human..."
I get this point long before you tell it to me. I've seen some theorem that has to be proved by this ATP and the result often unreadable or the language make it too complex to understand. But I heard there conference that talk about the implementation of ATP or ITP for mathematics education like TheDu, but I don't know the result from that conference about implementation of ATP or ITP in education. That's why I ask this question, man!
# " ...Secondly, YOU don't have one. Reading about the existence of is not having in your hand, set up on your machine, with the resources required, and trained how to use it. "
I have Coq installed in my notebook, yeah I have one, they say it interactive theorem prover, but when I use it, it take a long time to proof some basic logic problems like proving the transitivity of equality (x=y/\y=z->x=z).
# "finding one" _is_ your first stumbling block. Try it! :-)"
If you wanna say that the ATP that suitable for teaching method of proof or readable enough so high school student can understand it, Yeah you're right, I can't find one.
# "Have you got the right kind of household dust?"
I don't think so. The right kind for me is doesn't mean it the right kind for another.
Yes, you're right. That's pretty hard without any operator terms available. I need 1 month just to understand how to proof classical logic properties like p -> q ~q -> ~p using Coq.
Especially for Coq (I don't know about another ATP), sometime it's not take a long time to prove, but not simple as doing proof on paper. That's right, maybe ATP is not suitable for teaching (for high school student, it's impossible!) proof.
"I really believe a proof assistant would be better for you."
But, Coq is proof assistant too :o
I find another software called DC Proof 2.0, the proof-writing software not an ATP. It might be useful for teaching proof to students.
- Badges
- Science topic
- Similar topics
- Philosophy
- Philosophy Of Science
- Reasoning