Automated Proof Planning for Instructional Design
Erica Melis⋆, Christoph Glasmacher, Carsten Ullrich, Peter H. Gerjets · eScholarship (California Digital Library) · 2001
Automated theorem proving based on proof planning is a new and promising paradigm in the field of automated deduction.The idea is to use methods and heuristics as they are used by human mathematicians and encode this knowledge into so-called methods.Naturally, the question arises whether these methods can be beneficially used in learning mathematics too.This paper investigates and compares the effect of different instruction materials (textbook-based, example-based, and method-based) on problem solving performance.The results indicate that the performance for the method-based instruction derived from automated proof planning in the ΩMEGA system is superior to that of the other instructions that were derived from a textbook and an example-based classroom lesson.These results provide a first support for introducing proof planning based on methodological knowledge into the school curriculum for mathematics.