Preface

Traditionally, the conference is held every two years. The previous editions of ADG were held in Nanning in 2018, Strasbourg in 2016, Coimbra in 2014, Edinburgh in 2012, Munich in 2010, Shanghai in 2008, Pontevedra in 2006, Gainesville in 2004, Hagenberg in 2002, Zurich in 2000, Beijing in 1998, and Toulouse in 1996.

The 13th edition of ADG was supposed to be held in 2020 in Hagenberg, Austria, but due to the COVID-19 pandemic, it was postponed for 2021, and held online (still hosted by RISC Institute, Hagenberg, Austria), September 15-17, 2021 (https://www.risc.jku.at/conferences/adg2021).

The invited speakers at ADG 2021 were:

• Manfred Husty, University Innsbruck, Austria
• Christoph Koutschan, RICAM, Austria
• Wolfgang Windsteiger, RISC, JKU, Austria
• Gilles Dowek, Inria and ENS Paris-Saclay, France
• Pedro Quaresma, CISUC, University of Coimbra, Portugal

Despite the disturbed schedule, the quality of research articles submitted for this edition of ADG was very high. Out of fifteen submitted extended abstracts, fourteen were accepted for presentation. Each submission was carefully reviewed by three reviewers and this volume consists of versions revised according to the reviews. Therefore, along with articles for five invited lectures, this volume consists of nineteen articles, bringing exciting new ideas, spanning various areas of automated deduction in geometry, and showing the current state-of-the-art research in this field. The conference programme and this volume can be roughly divided into four parts:

Geometrical constraints:

This part opens by two invited lectures. One by Husty focuses on global algebraic representations of singularities of serial and parallel robots, as well as other mechanical devices like closed kinematic chains. The contribution by Koutschan derives a recursive formula for the number of realizations of minimally rigid graphs, by using algebraic and tropical geometry. The article by Marinković, Šukilović and Marić introduces a system for automated triangle constructions in absolute and hyperbolic geometry, and points to an online compendium containing construction descriptions and illustrations. The paper by Zeng, Lu, Xu and Wang proves a geometrical inequality which states that for any four points on a hemisphere with the unit radius, the largest sum of distances between the points is $4+4\sqrt{2}$. The article by Ida and Takahashi introduces a cut along a crease on an origami sheet to significantly simplify modeling and subsequent implementation for computational origami.

Automation and illustrations:

The invited lecture by Windsteiger report on several scenarios of using automated theorem proving software, especially the Theorema system, in university education. The article by Heimrath presents an implementation of the area method for Euclidean geometry as a stand-alone Mathematica package. The article by Schreck, Magaud, and Braun presents proofs of incidence geometry theorems in dimensions three, four, and five, obtained with the help of a combinatorial prover based on matroid theory applied to geometry. Janičić and Narboux report on a new approach for automated generation of illustrations for (readable) synthetic geometry proofs. The paper by Thaller and Kovács introduces a toolset able to create proofs without words by combining the Geometric Deduction Database method and the GeoGebra framework.

Formalization and repositories:

The invited lecture by Dowek advocates for expressing the theories implemented in computer proof systems in a common logical framework, such as the framework Dedukti, with some axioms common to all these theories and others differentiating them. The article by Magaud describes a formalization of the smallest projective space PG(3,2) in the Coq proof assistant, the spreads and packings of PG(3,2), as well as some of their properties. Schmoetten, Palmer, and Fleuriot report on the continued formalisation of an axiomatic system for Minkowski spacetime (as used in the study of Special Relativity) in Isabelle/Isar. Baeta and Quaresma, in their article, present the Open Geometry Prover Community Project, that aims at the integration of different efforts for automated theorem proving in geometry, under a common framework.

Discovery in geometry:

The final part of this volume starts with Quaresma's invited talk on new and interesting theorems, highlighting different approaches and various metrics to find the interesting ones among all those that were generated by automated discovery. The article by Kovács, Recio and Vélez reflects, through a collection of selected examples, on the potential impact of the GeoGebra Discovery application on different social and educational contexts. Todd's contribution presents an approach for discovery in geometry, based on identifying matrix patterns which, with appropriate numeric values, lead to theorems about angles. Brown, Kovács and Vajda report on a system of software tools that can automatically prove or discover geometric inequalities, based on GeoGebra and Tarski/QEPCAD B. In the last paper, Kovács and Vajda extend their research by proposing a method that could replace the general real quantifier elimination approach, using a parametric root finding algorithm.

The quality of the conference was due to the invited lecturers and the authors of submitted papers, but also to the reviewers, the members of the program committee, and all the organizers of ADG 2021:

General Chair

• Zoltán Kovács (JKU Linz School of Education, Austria)

Program Committee

• Predrag Janičić (University of Belgrade, Serbia), chair
• Armin Biere (Johannes Kepler University Linz, Austria)
• Francisco Botana (University of Vigo, Spain)
• Jose Capco (University of Innsbruck, Austria)
• Xiaoyu Chen (Beihang University, China)
• Thierry Dana-Picard (Jerusalem College of Technology, Israel)
• Jacques Fleuriot (University of Edinburgh, UK)
• Georg Grasegger (Johann Radon Institute, Austria)
• Markus Hohenwarter (JKU Linz School of Education, Austria)
• Tetsuo Ida (University of Tsukuba, Japan)
• Julien Narboux (University of Strasbourg, France)
• Walther Neuper (University of Technology, Graz, Austria)
• Pavel Pech (University of South Bohemia, České Budějovice, Czechia)
• Martin Pfurner (University of Innsbruck, Austria)
• Pedro Quaresma (University of Coimbra, Portugal)
• Tomás Recio (Universidad Antonio de Nebrija, Spain)
• Pascal Schreck (University of Strasbourg, France)
• Wolfgang Schreiner (RISC, Johannes Kepler University Linz, Austria)
• Ileana Streinu (Smith College, USA)
• Dingkang Wang (Chinese Academy of Sciences, China)
• Dongming Wang (Beihang University/Guangxi University for Nationalities, China)
• Jing Yang (Guangxi University for Nationalities, China)

Additional Reviewers

• Ujué Etayo (University of Cantabria, Spain)
• Bo Huang (Beihang University, China)
• Jake Palmer (University of Edinburgh, UK)
• Bican Xia (Peking University, China)

Local Organization

• Zsolt Lavicza (JKU Linz School of Education, Austria)

ADG Steering Committee

• Julien Narboux (University of Strasbourg, France), chair
• Francisco Botana (University of Vigo, Spain)
• Xiaoyu Chen (Beihang University, China)
• Hongbo Li (Chinese Academy of Sciences, China)
• Pedro Quaresma (University of Coimbra, Portugal)
• Pascal Schreck (University of Strasbourg, France)
• Ileana Streinu (Smith College, USA)
• Dongming Wang (Beihang University/Guangxi University for Nationalities, China)
• Jing Yang (Guangxi University for Nationalities, China)

We would like to express our gratitude to others who participated at ADG 2021 or helped the organization of ADG 2021 in some way. We would also like to thank the EPTCS staff for their support and efficiency.

December 2021.

Predrag Janičić ADG 2021 Program Committee Chair Zoltán Kovács ADG 2021 General Chair

Robot Kinematics – The Algebraic Point of View

Robot mechanical devices comprise many different types such as serial or parallel robots, wire driven systems, walking, rolling or humanoid robots.

Serial robots

Wire robot