Number Theory and Axiomatic Geometry in the Diproche System

Merlin Carl
(Europa-Universität Flensburg)

Diproche ("Didactical Proof Checking") is an automatic system for supporting the acquistion of elementary proving skills in the initial phase of university education in mathematics. A key feature of Diproche - which is designed by the example of the Naproche system developed by M. Cramer and others - is an automated proof checker for proofs written in a controlled fragment of natural language specifically designed to capture the language of beginners' proving exercises in mathematics. Both the accepted language and proof methods depend on the didactical and mathematical context and vary with the level of education and the topic proposed. An overall presentation of the system in general was given in Carl and Krapf 2019. Here, we briefly recall the basic architecture of Diproche and then focus on explaining key features and the working principles of Diproche in the sample topics of elementary number theory and axiomatic geometry.

In Pedro Quaresma, Walther Neuper and João Marcos: Proceedings 9th International Workshop on Theorem Proving Components for Educational Software (ThEdu'20), Paris, France, 29th June 2020, Electronic Proceedings in Theoretical Computer Science 328, pp. 56–78.
Published: 30th October 2020.

ArXived at: https://dx.doi.org/10.4204/EPTCS.328.4 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org