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

EPTCS 352

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

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:

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

Parallel robot

Rolling Robot, Humanoid Robot, Rolling-Serial Robot

Various mathematical formulations are used to describe the motion behavior of mechanisms and robots. This mathematical formulation is the basis for kinematic analysis and synthesis, i.e., determining the motion capability of a robot, the velocities and accelerations, on the one hand, and to obtain design parameters on the other. Vector/matrix formulation containing trigonometric functions is probably the most favoured approach used in the engineering research community. A less well known but nevertheless very successful approach relies on an algebraic formulation. In this method mechanism constraints are described with algebraic (polynomial) equations as to be able to solve the sets of equations that pertain to some given mechanism or robot, with the powerful tools of algebraic and numerical algebraic geometry. It will be shown that this approach leads to a description of the global behaviour of a mechanism or robot. Therefore we have coined the notion global kinematics for this method.


Algebraic representation of singularities of a 3-UPU parallel robot

With implicit, algebraic constraint equations one can get global information on

For more than 25 years, the author and his collaborators have been applying the algebraic formulation to a wide range of kinematic analysis and synthesis problems. These instances include direct and inverse pose determination in general parallel (e.g., Stewart-Gough platform) and serial (e.g. 6R) robots, singularity distribution and workspace mapping. This has also been carried out in cases of lower degree of mobility parallel robots as well as for planar, spatial and spherical mechanisms. Fundamental to such formulations is the algebraic parametrization of the various displacement groups (planar, spherical, spatial). These parameters are usually elements of the quaternion algebra of the displacement groups.

In this talk we will focus on the global algebraic formulation, the representation of singularities of serial and parallel robots as well as other mechanical devices like closed kinematic chains.


Sharing Geometry Proofs Across Logics and Systems

Gilles Dowek (Inria and ENS Paris-Saclay, France)

The contemporary development of computerized proof systems is a major step forward in the never ending quest of mathematical rigor. But it jeopardizes the universality of mathematical truth, as each proof system: Coq, HOL Light, PVS, etc. defines its own language for mathematical statements and its own truth conditions for these statements. To restore this universality of mathematical truth, we propose to follow a path that has some similarities with that used to resolve the crisis of non-Euclidean geometries: express the theories implemented in these systems in a common logical framework, such as the framework Dedukti, with some axioms common to all these theories and others differentiating them. Then, classify the proofs according to the axioms they use. This idea applies in particular to the Coq formalization of the first book of Euclid's elements, that, as expected, uses very few of the features of Coq and can therefore be translated to the theory of several other proof systems.


New and Interesting Theorems

Pedro Quaresma (CISUC, Department of Mathematics, University of Coimbra, Portugal)

In Automated Reasoning: 33 Basic Research Problems, Larry Wos, writes about the problems that computer programs that reason face. Problem 31 it is still open and object of active research:

What properties can be identified to permit an automated reasoning program to find new and interesting theorems, as opposed to proving conjectured theorems?

Two problems in a single sentence: new and interesting problems. The automatic discovery of new problems is a goal in itself, it has been addressed in specific areas, with different methods. The separation of the “weeds”, uninteresting, trivial facts, from the “wheat”, new and interesting facts, is much harder, but is being addressed also, by different authors using different approaches.

Paraphrasing, again, Wos, “since a reasoning program can be instructed to draw some (possible large) set of conclusions” what should be the “criteria that permit the program to select from those the ones (if any) that correspond to interesting results.”

The different approaches for the automatic discovery of mathematical theorems (and properties) and the proposed metrics to find the interesting ones among all those that were generated, are presented and discussed.

References

  1. Beeson, M.: Euclid After Computer Proof-checking. arXiv e-prints arXiv:2103.09623 (Mar 2021), to appear in American Mathematical Monthly in 2022.
  2. Beeson, M., Wos, L.: Finding proofs in Tarskian geometry. Journal of Automated Reasoning 58(1), 181–207 (Out 2016). doi:10.1007/s10817-016-9392-2.
  3. Colton, S., Bundy, A., Walsh, T.: On the notion of interestingness in automated mathematical discovery. International Journal of Human-Computer Studies 53(3), 351–375 (Sep 2000). doi:10.1006/ijhc.2000.0394.
  4. Gao, H., Li, J., Cheng, J.: Measuring interestingness of theorems in automated theorem finding by forward reasoning based on strong relevant logic. In: 2019 IEEE International Conference on Energy Internet (ICEI). pp. 356–361. IEEE (may 2019). doi:10.1109/ICEI.2019.00069.
  5. Gao, H., Cheng, J.: An epistemic programming approach for automated theorem finding. In: 2015 IEEE 14th International Conference on Cognitive Informatics & Cognitive Computing (ICCIxCC). IEEE (Jul 2015). doi:10.1109/ICCI-CC.2015.7259365.
  6. Gao, H., Goto, Y., Cheng, J.: Research on automated theorem finding: Current state and future directions. In: Lecture Notes in Electrical Engineering. pp. 105–110. Springer Berlin Heidelberg (2014). doi:10.1007/978-3-642-55038-6_16.
  7. Gao, H., Li, J., Cheng, J.: Measuring interestingness of theorems in automated theorem finding by forward reasoning: A case study in Tarski's geometry. In: 2018 IEEE SmartWorld, Ubiquitous Intelligence & Computing, Advanced & Trusted Computing, Scalable Computing & Communications, Cloud & Big Data Computing, Internet of People and Smart City Innovation (SmartWorld/SCALCOM/UIC/ATC/CBDCom/IOP/SCI). IEEE (cot 2018). doi:10.1109/SmartWorld.2018.00064.
  8. Kovács, Z., Yu, J.H.: Towards automated discovery of geometrical theorems in GeoGebra. CoRR abs/2007.12447 (2020), https://arxiv.org/abs/2007.12447.
  9. Puzis, Y., Gao, Y., Sutcliffe, G.: Automated generation of interesting theorems. In: FLAIRS Conference (2006).
  10. Quaresma, P., Graziani, P.: Measuring the readability of a proof, (submitted to J. Autom. Reason.).
  11. Recio, T., Vélez, M.P.: Automatic discovery of theorems in elementary geometry. J. Autom. Reason. 23, 63–82 (July 1999). doi:10.1023/A:1006135322108, http://dl.acm.org/citation.cfm?id=594128.594243.
  12. Rimma, N.: What makes a mathematical task interesting? Educational Research and Reviews 11(16), 1509–1520 (Aug 2016). doi:10.5897/ERR2016.2919.
  13. Wos, L.: Automated Reasoning: 33 Basic Research Problems. Prentice-Hall (1988).
  14. Wos, L.: The problem of automated theorem finding. Journal of Automated Reasoning 10(1), 137–138 (1993). doi:10.1007/BF00881868.