Automatic deduction in an AI geometry book

Abstract

The pursuit of an AI Geometry Book should involve the study of how currently developing methodologies and technologies of geometry knowledge representation, management, deduction and discovery can be incorporated effectively into a computational application, a “book” of the future. In the geometry book of the future statements and proofs should be en-lighted by dynamic geometry sketches and diagrams, and the correctness of the proofs should be ensured by computer checking. The book will be intelligent, the reader should be able to ask closed or open questions, and can also ask for proof hints. The book should also provide interactive exercises with automatic correction. To fulfil such a goal the development of an open library of geometry automated theorem provers with a carefully design application interface protocol, must be considered. This would allow to link computer platforms for geometry with theorem provers, providing the automatic deduction capabilities for the AI Geometry Book.