Dongming Wang

Dongming Wang
Beihang University and Guangxi University for Nationalities, China and CNRS, France

Title: Discovering Geometric Theorems from Images of Diagrams

Abstract:

In this talk, I present an algorithmic approach for automated discovery of geometric theorems from images of diagrams. The approach consists of the following main steps.

  1. Specify formally basic and derived concepts in chosen geometry with semantic representation.
  2. Retrieve and generate meaningful, understandable, and characteristic geometric information using techniques of shape recognition, numeric verification, and rewriting under semantic representations of geometric concepts.
  3. Introduce specialized strategies to eliminate trivial and redundant information and generate candidate geometric propositions according to the induction principle.
  4. Invoke a geometric theorem prover to prove or disprove each candidate proposition; those proved propositions are returned as theorems discovered.

Taking plane Euclidean geometry as an example, we have designed and implemented concrete algorithms for the four steps described above and tested the feasibility of the approach we proposed using images of diagrams produced by means of tool or hand drawing, scanning, and photographing. Experimental results show that our approach is feasible and efficient and can be used to discover hundreds of non-trivial geometric theorems automatically.

The content of this talk is based on joint work with Xiaoyu Chen and Dan Song.

Short Bio

Dongming Wang is Research Director at French National Center for Scientific Research (CNRS) and Professor at Beihang University and Guangxi University for Nationalities, China. He received the B.Sc. degree in 1983 from University of Science and Technology of China, the Ph.D. degree in 1987 from Academia Sinica, China, and Diplôme d’Habilitation à Diriger des Recherches in 1999 from Institut National Polytechnique de Grenoble, France. He was appointed Assistant Professor at Institute of Systems Science, Academia Sinica, China (1987-1988), Assistant Professor at Research Institute for Symbolic Computation, Johannes Kepler University, Austria (1988-1992), Chargé de Recherche at CNRS, France (1992-2005), Cheung Kong Professor of Computer Mathematics at Beihang University, China (2005-2008), and Deputy Director of Beihang Sino-French Engineer School, China/France (2005-2008). He was elected Member of the Academia Europaea in 2017.

Wang has worked on algorithmic elimination theory, geometric reasoning and knowledge management, and applications of symbolic computation to qualitative analysis of differential and biological systems. Author of three monographs, co-author of three textbooks, and (co-)editor/translator of over 20 books and special volumes, he has published more than 100 papers in international journals and conference proceedings. He served as General Chair of AISC 2006 and ISSAC 2007 and on the program committees of more than 50 conferences and workshops. He is founding Editor-in-Chief and Managing Editor of Mathematics in Computer Science and Executive Associate Editor-in-Chief of SCIENCE CHINA Information Sciences.