Title: A Rule Based Theorem Prover: an Introduction to Proofs in 7th Year
Joana Teles, CMUC / Department of Mathematics, University of Coimbra, Portugal
Vanda Santos, CIDTFF, University of Aveiro and CISUC, Portugal
Pedro Quaresma, CISUC / Department of Mathematics, University of Coimbra, Portugal
Abstract
The introduction of automated deduction systems in secondary schools
face several bottlenecks, apart 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. The approach is tested using
a set of geometric conjectures that can be the goal of a 7th year
class.