Title: Rule Based Geometry Automated Theorem Provers
Nuno Baeta CISUC, University of Coimbra, Portugal
Pedro Teixeira, Department of Mathematics, University of Coimbra, Portugal
Pedro Quaresma, CISUC / Department of Mathematics, University of Coimbra, Portugal
Geometry Automated Theorem Provers have now what may be considered a
long story. Since the early attempts, linked to Artificial
Intelligence, synthetic provers based on inference rules and using
forward chaining reasoning are considered the more suited for
education. Using an appropriated set of rules and using forward
chaining they can more easily mimic the expected behaviour of a
student when developing a proof. We describe an implementation of the
geometry deductive database method, discussing its merits, and
demerits when an application in education is concerned.