Cognitive Tutoring in Mathematics based on Assertion Level Reasoning and Proof Strategies (Extended Abstract)

Serge Autexier, Dominik Dietrich, Marvin Schiller

In: Pedro Quaresma , Ralph-Johan Back (Hrsg.). THedu'11, Workshop associated to CADE-23. THedu - CTP Components for Educational Software (ThEdu-11) befindet sich Conference on Automated Deduction July 31 Wroclaw Poland Seiten 11-15 CISUC Technical Report 2011/001 University of Coimbra, Portugal 7/2011.


To know how to do proofs is a skill that is essential for every mathematician and scientist. Hence, learning how to do proofs is a major part in the education of students of mathematics and modern science. Intelligent tutoring systems are an attractive vehicle to make high-quality teaching and training environments available for a wide public. There are two main approaches: Model tracing tutors, which are process-centric and try to fathom the process a student arrived at a solution, and constraint based tutors, which are product-centric and are based on the idea that diagnostic information is not in the sequence of actions leading to the problem state, but solely in the problem state itself. This paper gives a concise summary of our work in the context of computer theorem proving, highlighting the techniques from the theorem proving community that are used and which have been successfully evaluated in experiments with computer-based tutoring of proofs in naive set theory.


Weitere Links

ThEdu11.pdf (pdf, 291 KB )

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence