EPTCS 352
Proceedings of the 13th International Conference on
Automated Deduction in Geometry
Hagenberg, Austria/virtual, September 1517, 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 WithoutLossofGenerality 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 
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 coordinatefree 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, specialpurpose 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 COVID19 pandemic, it was postponed for 2021, and held online
(still hosted by RISC Institute, Hagenberg, Austria), September 1517, 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 ParisSaclay, 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 stateoftheart 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 standalone 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 DanaPicard (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

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.
Wire robot