Generating hints and feedback for Hilbert-style axiomatic proofs

Josje Lodder; B.J. Heeren; J.T. Jeuring

doi:10.1145/3017680.3017736

Generating hints and feedback for Hilbert-style axiomatic proofs

Josje Lodder, B.J. Heeren, J.T. Jeuring

Dept of Information and Computing Sciences

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

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.

Original language	English
Title of host publication	SIGCSE '17: Proceedings of the 2017 ACM SIGCSE Technical Symposium on Computer Science Education
Publisher	Association for Computing Machinery
Pages	387-392
Number of pages	6
ISBN (Print)	978-1-4503-4698-6
DOIs	https://doi.org/10.1145/3017680.3017736
Publication status	Published - 2017

Keywords

propositional logic
axiomatic proofs
Hilbert axiom system
feedback
hints
intelligent tutoring
e-learning

Access to Document

10.1145/3017680.3017736

HilbertFinal published version, 320 KBLicence: Taverne

Cite this

@inproceedings{4cdacfe793ea4cdeba1ecda643aefd74,

title = "Generating hints and feedback for Hilbert-style axiomatic proofs",

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",

author = "Josje Lodder and B.J. Heeren and J.T. Jeuring",

year = "2017",

doi = "10.1145/3017680.3017736",

language = "English",

isbn = "978-1-4503-4698-6",

pages = "387--392",

booktitle = "SIGCSE '17: Proceedings of the 2017 ACM SIGCSE Technical Symposium on Computer Science Education",

publisher = "Association for Computing Machinery",

address = "United States",

}

Generating hints and feedback for Hilbert-style axiomatic proofs. / Lodder, Josje; Heeren, B.J.; Jeuring, J.T.
SIGCSE '17: Proceedings of the 2017 ACM SIGCSE Technical Symposium on Computer Science Education. Association for Computing Machinery, 2017. p. 387-392.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Generating hints and feedback for Hilbert-style axiomatic proofs

AU - Lodder, Josje

AU - Heeren, B.J.

AU - Jeuring, J.T.

PY - 2017

Y1 - 2017

N2 - 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.

AB - 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.

KW - propositional logic

KW - axiomatic proofs

KW - Hilbert axiom system

KW - feedback

KW - hints

KW - intelligent tutoring

KW - e-learning

U2 - 10.1145/3017680.3017736

DO - 10.1145/3017680.3017736

M3 - Conference contribution

SN - 978-1-4503-4698-6

SP - 387

EP - 392

BT - SIGCSE '17: Proceedings of the 2017 ACM SIGCSE Technical Symposium on Computer Science Education

PB - Association for Computing Machinery

ER -

Generating hints and feedback for Hilbert-style axiomatic proofs

Abstract

Keywords

Access to Document

Fingerprint

Cite this