Generating hints and feedback for Hilbert-style axiomatic proofs
Files
Publication date
2017
Authors
Lodder, Josje
Heeren, Bastiaan
Jeuring, J.T.
Editors
Advisors
Supervisors
Document Type
Part of book
Metadata
Show full item recordCollections
License
taverne
Abstract
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.
Keywords
propositional logic, axiomatic proofs, Hilbert axiom system, feedback, hints, intelligent tutoring, e-learning, Taverne
Citation
Lodder, J, Heeren, B J & Jeuring, J T 2017, Generating hints and feedback for Hilbert-style axiomatic proofs. in SIGCSE '17: Proceedings of the 2017 ACM SIGCSE Technical Symposium on Computer Science Education. Association for Computing Machinery, pp. 387-392. https://doi.org/10.1145/3017680.3017736