Proofs generated by LOGAX are comparable to expert proofs¶

Claim · All claims
Evidence · 1 study (2 entries) · design r2 · q2
Currency · newest study 2021 · not yet checked against its sources · not reviewed by a person

Subclaims¶

q2 i? Eight of ten textbook and lecture-note expert proofs are equal to the LOGAX-generated proofs. → Josje Lodder 2021 q2 i? In a comparison with 24 Metamath theorems using lemmas, nearly two thirds of LOGAX proofs are equal to Metamath proofs except for line order, and the LOGAX proof is shorter in eight cases. → Josje Lodder 2021 (2)

Evidence¶

Josje Lodder 2021¶

Josje Lodder, Bastiaan Heeren, Johan Jeuring, Wendy Neijenhuis. (2021). Generation and Use of Hints and Feedback in a Hilbert-Style Axiomatic Proof Tutor. International Journal of Artificial Intelligence in Education 31:99-133. https://doi.org/10.1007/s40593-020-00222-2

q2 · i? · design · r2

Comparison of LOGAX proofs without lemmas against 10 expert proofs from textbooks of Ben-Ari, Kelly, and Goldrei and logic lecture notes (Table 1). "Eight of the ten expert proofs are equal to the LOGAX proofs"; the two mismatches differ in strategy or length.

"Eight of the ten expert proofs are equal to the LOGAX proofs. In exercise 6, LOGAX uses the deduction theorem instead of Axiom a."

Josje Lodder 2021 (2)¶

Josje Lodder, Bastiaan Heeren, Johan Jeuring, Wendy Neijenhuis. (2021). Generation and Use of Hints and Feedback in a Hilbert-Style Axiomatic Proof Tutor. International Journal of Artificial Intelligence in Education 31:99-133. https://doi.org/10.1007/s40593-020-00222-2

q2 · i? · design · r2

Indirect comparison of LOGAX proofs with lemmas against 24 Metamath proofs, after inlining lemmas and removing deduction-theorem applications. "Nearly two thirds (15 out of 24) proofs are equal except for the order of the lines"; LOGAX is shorter in eight cases, in seven of which it does not use the lemmas.

"The comparison consists of 24 theorems, 12 with and 12 without negation. Nearly two thirds (15 out of 24) proofs are equal except for the order of the lines. The LOGAX proof is shorter than the Metamath proof in eight cases."

Discussion¶

Related Claims¶

• Dynamically generated proof graphs let LOGAX recognize all correct student solutions and give hints on them — related
• Student mistakes in axiomatic proofs fall into three categories and can largely be covered by buggy rules — related
• Hints generated by LOGAX help students complete the exercises — related