TY - GEN
T1 - Automation of geometry - Theorem proving, diagram generation, and knowledge management
AU - Wang, Dongming
PY - 2013
Y1 - 2013
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/84885191830
U2 - 10.1007/978-3-642-40672-0_2
DO - 10.1007/978-3-642-40672-0_2
M3 - 会议稿件
AN - SCOPUS:84885191830
SN - 9783642406713
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 31
EP - 32
BT - Automated Deduction in Geometry - 9th International Workshop, ADG 2012, Revised Selected Papers
PB - Springer Verlag
T2 - 9th International Workshop on Automated Deduction in Geometry, ADG 2012
Y2 - 17 September 2012 through 19 September 2012
ER -