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


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

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

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


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 (

The invited speakers at ADG 2021 were:

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

Program Committee

Additional Reviewers

Local Organization

ADG Steering Committee

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