Abstract
This paper describes LOGAX, an interactive tutoring tool that gives hints and feedback
to a student who stepwise constructs a Hilbert-style axiomatic proof in propositional
logic. LOGAX generates proofs to calculate hints and feedback. We compare these
generated proofs with expert proofs 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. Even if a student
diverges from the generated solution, LOGAX still provides hints, including next steps
or reachable subgoals, and feedback. With a few improvements in the design of the
set of buggy rules, LOGAX will cover about 80% of the mistakes made by students
by buggy rules. The hints help students to complete the exercises.
to a student who stepwise constructs a Hilbert-style axiomatic proof in propositional
logic. LOGAX generates proofs to calculate hints and feedback. We compare these
generated proofs with expert proofs 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. Even if a student
diverges from the generated solution, LOGAX still provides hints, including next steps
or reachable subgoals, and feedback. With a few improvements in the design of the
set of buggy rules, LOGAX will cover about 80% of the mistakes made by students
by buggy rules. The hints help students to complete the exercises.
| Original language | English |
|---|---|
| Pages (from-to) | 99–133 |
| Number of pages | 35 |
| Journal | International Journal of Artificial Intelligence in Education |
| Volume | 31 |
| Early online date | 2020 |
| DOIs | |
| Publication status | Published - 2021 |
Keywords
- Propositional logic
- Axiomatic proofs
- Hilbert axiom system
- Feedback
- Intelligent tutoring