In Memory of Wen-tsün Wu,Founder of the Chinese School of Mathematics Mechanization
|
ADG is a forum dedicated to the exchange of ideas and views, to the presentation of research results and progress, and to the demonstration of software tools on the intersection between geometry, computation, and automated reasoning. ADG organized a workshop every two years. The previous editions were held in Strasbourg (France) 2016, Coimbra (Portugal) 2014, Edinburgh (UK) 2012, Munich (Germany) 2010, Shanghai (China) 2008, Pontevedra (Spain) 2006, Gainesville (USA) 2004, Linz (Austria) 2002, Zurich (Switzerland) 2000, Beijing (China) 1998, and Toulouse (France) 1996.
The twelfth conference ADG 2018 will take place in Nanning, China, from September 11 to September 14, 2018, in memory of Wen-tsün Wu, founder of the Chinese school of mathematics mechanization.
Aim and Scope
ADG 2018 aims at gathering researchers, engineers, and others interested in exploring methods for automated reasoning and symbolic computation in geometry, to discuss theoretical and practical challenges, and to present recent research progress and results dedicated (not exhausted) in
- polynomial algebra, invariant and coordinate-free methods, probabilistic, synthetic, and logic approaches, techniques for automated geometric reasoning from discrete mathematics, combinatorics, and numerics;
- symbolic and numeric methods for geometric computation, geometric constraint solving, automated generation/reasoning and manipulation with diagrams;
- design and implementation of geometry software, special-purpose tools, automated theorem provers, experimental studies;
- applications of ADG to mechanics, geometric modeling, CAGD/CAD, computer vision, robotics, and education.
- Problem: what is the problem/question/objective?
- Motivation: why do we work on the problem and what is the importance?
- State of the art: what has been done already on the problem?
- Contribution: what is the main original contribution?
- Main idea: what is the main idea underlying the contribution?
Invited Speakers
Jacques Fleuriot (University of Edinburgh, UK)Interactive Theorem Proving in Geometry: From Foundations to Applications
In this talk, I乫ll argue that interactive theorem proving is an effective tool for the systematic investigation of geometric problems, ranging from axiomatic foundations to formal verification. This type of mechanization is usually carried out within the settings of proof-assistants such as Isabelle, which provide both a rich language for formalizing non-trivial concepts, e.g. higher-order geometric axioms or even inductive definitions, and an array of powerful automated tools, e.g. first order theorem provers and decision procedures, that can help the user in their quest for a (readable) proof.
I will illustrate the above by discussing some of the achievements from the past twenty years, a number of which were originally presented at Automated Deduction in Geometry. Time permitting, I乫ll also talk about some potential mechanization challenges and avenues for collaborative proof efforts in geometry.
Xiao-Shan Gao (Chinese Academy of Sciences, China) Wen-tsün Wu and Mathematics Mechanization
In this talk, I will give a review of some of the major advances in the field of mathematics mechanization coined by Wen-tsün Wu. These include the Ritt-Wu characteristic set method for symbolic solution of algebraic, differential, and difference polynomial equation systems; methods for automated proving and discovering geometry theorems; and applications in computer aided geometric design, computer vision, robotics, etc.
Ilias S. Kotsireas (Wilfrid Laurier University, Canada) Hard Combinatorial Problems via SAT
The area of boolean satisfiability and SAT solvers has seen dramatic advances in the past two decades. A recent trend in SAT solving is an attempt to combine the strengths of symbolic computation tools with the power of SAT solvers, in order to improve their effectiveness and to build custom-tailored SAT solvers for hard combinatorial problems. We will describe our work in this context, with a focus on some particularly hard combinatorial problems, described via autocorrelation of finite sequences.
Based on joint work with Vijay Ganesh (University of Waterloo) and Curtis Bright (University of Waterloo) in the context of the Horizon 2020 EU project "Satisfiability Checking and Symbolic Computation" (SC^2).
Pascal Schreck (University of Strasbourg, France)Around Dandelin-Gallucci Theorem
This talk is about mechanization of projective incidence geometry. I present some parts of a work which began in 2004 with a proposal of Dominique Michelucci about the so-called hexamys and a study around combinatorial proofs in incidence geometry. Most of this presentation relates to joint works with other members of the Strasbourg team and especially David Braun and Nicolas Magaud. After a brief description of projective incidence geometry, and after recalling the importance of both Desargues and Pappus theorems, I explain how projective incidence geometries correspond to a certain class of matroids. Then, I present Dandelin-Gallucci theorem with several proofs using very different approaches: combinatoric algebra, synthetic geometry, matroids, ...
Dingkang Wang (Chinese Academy of Sciences, China)Comprehensive Gröbner Systems and Discovering Geometric Theorems Mechanically
For many geometric theorems, the hypotheses can be represented by a system of parametric polynomial equations and the conclusion can be represented by a parametric polynomial equation. An important problem concerning proving geometric theorems is to determine whether a geometric statement is valid under a specialization of parameters. Comprehensive Gröbner system is an important tool to solve the problem related to parametric polynomial system. We will review the progresses in comprehensive Gröbner systems and then use it to discover geometric theorems mechanically, i.e., we can find out complementary conditions on the parameters such that the geometric statement becomes true or true on components.
Chuanming Zong (Tianjin University, China)Can You Pave the Plane Nicely with Identical Tiles
Everybody knows that identical regular triangles or squares can tile the whole plane. Many people know that identical regular hexagons can tile the plane properly as well. In fact, even the bees know and use this fact! Is there any other convex domain which can tile the Euclidean plane? Of course, there is a long list of them! To find the list and to show the completeness of the list is a unique drama in mathematics, which has lasted for more than one century and the completeness of the list has been mistakenly announced not only once! Up to now, the list consists of triangles, quadrilaterals, fifteen types of pentagons, and three types of hexagons. In 2017, Michael Rao announced a computer proof for the completeness of the list. Meanwhile, Qi Yang and Chuanming Zong made a series of unexpected discoveries in multiple tilings in the Euclidean plane. For examples, besides parallelograms and centrally symmetric hexagons, there is no other convex domain which can form any two-, three- or four-fold translative tiling in the plane. However, there are two types of octagons and one type of decagons which can form nontrivial five-fold translative tilings. Furthermore, a convex domain can form a five-fold translative tiling of the plane if and only if it can form a five-fold lattice tiling. In this talk we will report these progresses.
Important Dates
| Deadline for extended abstract/full paper submission | |
| Notification on all papers | July 15, 2018 |
| Camera-ready submission | July 31, 2018 |
| Early registration deadline | August 1, 2018 |
| Conference taking place | September 11-14, 2018 |
Submission
Original research papers in English, including experimental work and work in progress, are welcome. The following two types of submissions are invited.
(1) Full paper: maximum 20 pages
(2) Extended abstract addressing the following aspects explicitly:
Submissions should follow the standard Springer LNCS Proceedings format. Electronic submission as PDF is required via EasyChair at
http://www.easychair.org/conferences/?conf=adg2018.
If you have any problems with the submission of your paper, or questions concerning ADG 2018 or EasyChair, please contact adg2018@easychair.org. At least one author of each accepted submission must register at ADG 2018.
Publication
The submitted contributions will be subject to a summary review by the Program Committee, bearing in mind that this first review is mainly for presentation, NOT for publication. Digital publication of the full papers/extended abstracts accepted for presentation will be available at the conference. The authors of the full papers/extended abstracts accepted for presentation at the conference will be invited to submit their full and/or revised papers for publication in a formal proceedings of ADG 2018 after the conference. The full papers (submitted after the conference) will be formally reviewed by PC members and external referees. All participants are encouraged to bring along posters on their work (irrespective of whether it was presented at the conference or not) for display during ADG 2018.
The accepted full papers will be published as a special issue of some journal or in the Springer Lecture Notes in Artificial Intelligence (LNAI) series or Lecture Notes in Computer Science (LNCS) series. The proceedings of ADG 1996, ADG 1998, ADG 2000, ADG 2002, ADG 2004, ADG 2006, ADG 2010, ADG 2012, and ADG 2014 appeared as LNAI 1360, LNAI 1669, LNAI 2061, LNAI 2930, LNAI 3763, LNAI 4869, LNCS 6877, LNAI 7993, and LNAI 9201, respectively.
General Chair
Dongming Wang (Beihang University and Guangxi University for Nationalities, China)
Program Committee Chair
Hongbo Li (Chinese Academy of Sciences, China)
Program Committee
Francisco Botana (University of Vigo, Spain)
Falai Chen (University of Science and Technology of China, China)
Xiaoyu Chen (Beihang University, China)
Yong Feng (Chinese Academy of Sciences, China)
Lei Huang (Chinese Academy of Sciences, China)
Hoon Hong (North Carolina State University, USA)
Tetsuo Ida (University of Tsukuba, Japan)
Predrag Janičić (University of Belgrade, Serbia)
Na Lei (Dalian University of Technology, China)
ZhuoJun Liu (Chinese Academy of Sciences, China)
Julien Narboux (University of Strasbourg, France)
Pedro Quaresma (University of Coimbra, Portugal)
Tomás Recio (University of Cantabria, Spain)
Ileana Streinu (Smith College, USA)
Thomas Sturm (CNRS, France)
Dingkang Wang (Chinese Academy of Sciences, China)
Chee K. Yap (New York University, USA)
Local Arrangements
Xiaoyu Chen (Beihang University, China)
Jing Yang (Guangxi University for Nationalities, China)
Webmaster & Publicity Chair
Fadoua Ghourabi (Ochanomizu University, Japan)