Generating Hints and Feedback for Hilbert-style Axiomatic Proofs
Josje Lodder, Bastiaan Heeren, and Johan Jeuring
This paper describes an algorithm to generate Hilbert-style
axiomatic proofs. Based on this algorithm we develop Logax,
a new interactive tutoring tool that provides hints and
feedback to a student who stepwise constructs an axiomatic
proof. We compare the generated proofs with expert and
student solutions, and conclude that the quality of the generated
proofs is comparable to that of expert proofs. Logax
recognizes most steps that students take when constructing
a proof. If a student diverges from the generated solution,
logax can still provide hints and feedback.
In Proceedings of the 2017 ACM SIGCSE Technical Symposium on Computer Science Education, SIGCSE '17, pages 387-392, 2017.
Links