OS Math. Logik, Mengenlehre und Modelltheorie: Diproche - Automated Proof Checking for Didactical Applications

Montag, 01. Juli 2019
15:15 – 16:45 Uhr

F 426

C. Antos-Kuby, S. Kuhlmann

Merlin Carl

Diese Veranstaltung ist Teil der Veranstaltungsreihe „Oberseminar Mathematische Logik, Mengenlehre und Modelltheorie“.

We present the Diproche (Didactical Proof Checking) system (a software inspired by the Naproche (Natural language Proof Checking) system (developed by Koepke, Cramer, Schröder and others) which uses techniques from computational linguistics and automated theorem proving to provide an automated proof checker for proofs written in a fragment of natural mathematical language specifically designed to express solutions to typical proving exercises for beginner students. The aim of Diproche is to serve as an automatic tutor for students learning how to prove. In addition to reporting gaps in proofs, Diproche provides a detailed feedback on linguistic mistakes, failures to meet the goal of the exercise or self-formulated subgoals, type errors and diagnosis of possible formal fallacies. Moreover, users can obtain hints when getting stuck while searching for a solution.