Published: 30th December 2021 DOI: 10.4204/EPTCS.352 ISSN: 2075-2180

# Proceedings of the 13th International Conference onAutomated Deduction in Geometry Hagenberg, Austria/virtual, September 15-17, 2021

Edited by: Predrag Janičić and Zoltán Kovács

 Preface Predrag Janičić and Zoltán Kovács Invited Lecture: Robot Kinematics – The Algebraic Point of View Manfred L. Husty 1 Invited Lecture: Realizations of Rigid Graphs Christoph Koutschan 4 On Automating Triangle Constructions in Absolute and Hyperbolic Geometry Vesna Marinković, Tijana Šukilović and Filip Marić 14 Maximizing the Sum of the Distances between Four Points on the Unit Hemisphere Zhenbing Zeng, Jian Lu, Yaochen Xu and Yuzheng Wang 27 A New Modeling of Classical Folds in Computational Origami Tetsuo Ida and Hidekazu Takahashi 41 Invited Lecture: Automated Theorem Proving in the Classroom Wolfgang Windsteiger 54 The Area Method in the Wolfram Language Jack Heimrath 64 Mechanization of Incidence Projective Geometry in Higher Dimensions, a Combinatorial Approach Pascal Schreck, Nicolas Magaud and David Braun 77 Automated Generation of Illustrations for Synthetic Geometry Proofs Predrag Janičić and Julien Narboux 91 Online Generation of Proofs Without Words Alexander Thaller and Zoltán Kovács 103 Invited Lecture: Sharing Geometry Proofs Across Logics and Systems Gilles Dowek 106 Spreads and Packings of PG(3,2), Formally! Nicolas Magaud 107 Formalising Geometric Axioms for Minkowski Spacetime and Without-Loss-of-Generality Theorems Richard Schmoetten, Jake Palmer and Jacques Fleuriot 116 Open Geometry Prover Community Project Nuno Baeta and Pedro Quaresma 129 Invited Lecture: New and Interesting Theorems Pedro Quaresma 139 GeoGebra Discovery in Context Zoltán Kovács, Tomás Recio and M. Pilar Vélez 141 A Method for the Automated Discovery of Angle Theorems Philip Todd 148 Supporting Proving and Discovering Geometric Inequalities in GeoGebra by using Tarski Christopher W. Brown, Zoltán Kovács and Róbert Vajda 156 Parametric Root Finding for Supporting Proving and Discovering Geometric Inequalities in GeoGebra Zoltán Kovács and Róbert Vajda 167

# Preface

Automated Deduction in Geometry (ADG) is a forum to exchange ideas and views, to present research results and progress, and to demonstrate software tools at the intersection between geometry and automated deduction. Relevant topics include (but are not limited to): polynomial algebra, invariant and coordinate-free methods; probabilistic, synthetic, and logic approaches, techniques for automated geometric reasoning from discrete mathematics, combinatorics, and numerics; interactive theorem proving in geometry; symbolic and numeric methods for geometric computation, geometric constraint solving, automated generation/reasoning and manipulation with diagrams; design and implementation of geometry software, automated theorem provers, special-purpose tools, experimental studies; applications of ADG in mechanics, geometric modelling, CAGD/CAD, computer vision, robotics and education.

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)

• 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)

• 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

Manfred L. Husty (University Innsbruck, Joanneum Research Klagenfurt, Austria)

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