Automation of geometry - Theorem proving, diagram generation, and knowledge management

Abstract of Talk: The process of theorem proving in geometry is sophisticated and intelligence-demanding. Mechanizing this process has been the objective of many great scientists, from ancient times to the information era. Scientific breakthroughs and technological advances have been made in the last three decades, which allows us now to automate the process (almost) fully on modern computing devices. The remarkable success of automated theorem proving has been a major source of stimulation for investigations on the automation of other processes of geometric deduction such as diagram generation and knowledge management. This talk provides an account of historical developments on the mechanization and the automation of theorem proving in geometry, highlighting representative methodologies and approaches. Automated generation of dynamic diagrams involving both equality and inequality constraints is discussed as another typical task of geometric deduction. The presentation is then centered around the concept and the management of geometric knowledge.We view geometric theorems, proofs, and diagrams as well as methods as knowledge objects and thus as part of the geometric knowledge.We are interested in creating reliable software environments in which different kinds of geometric knowledge are integrated, effective algorithms and techniques for managing the knowledge are implemented, and the user can use the built-in knowledge data and functions to develop new tools and to explore geometry visually, interactively, and dynamically. We have considered and studied several foundational and engineering issues of geometric knowledge management and adopted some key strategies to deal with the issues. We explain and discuss such issues and strategies and demonstrate the effectiveness of the strategies by some pieces of software that have implemented preliminary and experimental versions of our geometric knowledge base, geometric-object-oriented language, and geometric textbook system.