Providing On-Demand Feedback for Improved Learning of Logical Reasoning in Computer Science and Software Engineering

For teaching introductory courses on logics and discrete mathematics for computer science students, there have been several attempts to use support by existing established “professional” proof assistants. In contrast, we have developed a proof checker the feature set of which is motivated by the educational application. Students access our system via a web-app, which they use to write proofs in the rigorous but mostly-conventional mathematical language of the textbook, and obtain fine-grained on-demand feedback on the correctness of their proof attempts.