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.
Type de document :
Communication dans un congrès
Tetsuo Ida; Jacques Fleuriot. ADG 2012 - 9th International Workshop Automated Deduction in Geometry, Sep 2012, Edinburgh, United Kingdom. Springer, 7993, pp.31-32, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-40672-0_2〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00913433
Contributeur : Dongming Wang <>
Soumis le : mardi 3 décembre 2013 - 16:38:37
Dernière modification le : lundi 29 mai 2017 - 14:24:35

Identifiants

Collections

Citation

Dongming Wang. Automation of Geometry - Theorem Proving, Diagram Generation, and Knowledge Management. Tetsuo Ida; Jacques Fleuriot. ADG 2012 - 9th International Workshop Automated Deduction in Geometry, Sep 2012, Edinburgh, United Kingdom. Springer, 7993, pp.31-32, 2013, Lecture Notes in Computer Science. 〈10.1007/978-3-642-40672-0_2〉. 〈hal-00913433〉

Partager

Métriques

Consultations de la notice

221