A Rule Based Theorem Prover: an Introduction to Proofs in Secondary Schools
This work tackles the problem of making automated theorem proving accessible and engaging for secondary school students, though it is incremental in adapting existing methods to educational contexts.
The paper addresses the challenge of integrating automated theorem provers into secondary school geometry education by proposing a rule-based method using geometry deductive databases, tested on geometric conjectures suitable for 12-year-old students.
The introduction of automated deduction systems in secondary schools face several bottlenecks. Beyond the problems related with the curricula and the teachers, the dissonance between the outcomes of the geometry automated theorem provers and the normal practice of conjecturing and proving in schools is a major barrier to a wider use of such tools in an educational environment. Since the early implementations of geometry automated theorem provers, applications of artificial intelligence methods, synthetic provers based on inference rules and using forward chaining reasoning are considered to be more suited for education proposes. Choosing an appropriate set of rules and an automated method that can use those rules is a major challenge. We discuss one such rule set and its implementation using the geometry deductive databases method (GDDM). The approach is tested using some chosen geometric conjectures that could be the goal of a 7th year class (approx. 12-year-old students). A lesson plan is presented, its goal is the introduction of formal demonstration of proving geometric theorems, trying to motivate students to that goal