HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

Automation of Geometry - Theorem Proving, Diagram Generation, and Knowledge Management

Dongming Wang 1
1 PolSys - Polynomial Systems
LIP6 - Laboratoire d'Informatique de Paris 6, Inria Paris-Rocquencourt
Abstract : 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.
Document type :
Conference papers
Complete list of metadata

Contributor : Dongming Wang Connect in order to contact the contributor
Submitted on : Tuesday, December 3, 2013 - 4:38:37 PM
Last modification on : Friday, January 21, 2022 - 3:22:22 AM

Links full text



Dongming Wang. Automation of Geometry - Theorem Proving, Diagram Generation, and Knowledge Management. ADG 2012 - 9th International Workshop Automated Deduction in Geometry, Sep 2012, Edinburgh, United Kingdom. pp.31-32, ⟨10.1007/978-3-642-40672-0_2⟩. ⟨hal-00913433⟩



Record views