Published: 22nd January 2024
DOI: 10.4204/EPTCS.398
ISSN: 2075-2180


Proceedings 14th International Conference on
Automated Deduction in Geometry
Belgrade, Serbia, 20-22th September 2023

Edited by: Pedro Quaresma and Zoltán Kovács

Pedro Quaresma and Zoltán Kovács
Invited Presentation: Formalization, Arithmetization and Automatization of Geometry
Julien Narboux
Invited Presentation: Formalization, Automatization and Visualization of Hyperbolic Geometry
Filip Marić
Invited Presentation: OK Geometry
Zlatan Magajna
Towards Automatic Transformations of Coq Proof Scripts
Nicolas Magaud
Towards Automated Readable Proofs of Ruler and Compass Constructions
Vesna Marinković, Tijana Šukilović and Filip Marić
Automated Completion of Statements and Proofs in Synthetic Geometry: an Approach based on Constraint Solving
Salwa Tabet Gonzalez, Predrag Janičić and Julien Narboux
Using GXWeb for Theorem Proving and Mathematical Modelling
Philip Todd and Danny Aley
Showing Proofs, Assessing Difficulty with GeoGebra Discovery
Zoltán Kovács, Tomás Recio and M. Pilar Vélez
Open Source Prover in the Attic
Zoltán Kovács and Alexander Vujic
Automation of Triangle Ruler-and-Compass Constructions Using Constraint Solvers
Milan Banković
Towards an Independent Version of Tarski's System of Geometry
Pierre Boutry, Stéphane Kastenbaum and Clément Saintier
Considerations on Approaches and Metrics in Automated Theorem Generation/Finding in Geometry
Pedro Quaresma, Pierluigi Graziani and Stefano M. Nicoletti
Solving with GeoGebra Discovery an Austrian Mathematics Olympiad problem: Lessons Learned
Belén Ariño-Morera, Zoltán Kovács, Tomás Recio and Piedad Tolmos
Solving Some Geometry Problems of the Náboj 2023 Contest with Automated Deduction in GeoGebra Discovery
Amela Hota, Zoltán Kovács and Alexander Vujic
Using Java Geometry Expert as Guide in the Preparations for Math Contests
Ines Ganglmayr and Zoltán Kovács
The Locus Story of a Rocking Camel in a Medical Center in the City of Freistadt
Anna Käferböck and Zoltán Kovács
3D Space Trajectories and beyond: Abstract Art Creation with 3D Printing
Thierry Dana-Picard, Matias Tejera and Eva Ulbrich
Theorem Discovery Amongst Cyclic Polygons
Philip Todd
Improving Angular Speed Uniformity by Piecewise Radical Reparameterization
Hoon Hong, Dongming Wang and Jing Yang


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 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 Hagenberg 2021, postponed from 2020, and held online due to the COVID-19 pandemic, 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 14th edition, ADG 2023, was held in Belgrade, Serbia, in September 20-22, 2023 (ADG2023). This edition of ADG had an additional special focus topic: Deduction in Education.

The invited speakers at ADG 2023 were:

The quality of research articles submitted for this proceedings of ADG was very high. Out of seventeen full-papers submitted, fifteen were accepted. Each submission was carefully reviewed by, at least, three reviewers. Therefore this volume consists of fifteen 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 3 parts.

Automated and interactive theorem proving in geometry

The effort of formalise many areas of mathematics using deduction tools such as proof assistants is a huge undertaking, the area of geometry is part of that effort. The two invited talks, by Julien Narbox, Formalisation, arithmetization and automatisation of geometry and by Filip Marić, Automatization, formalization and visualization of hyperbolic geometry gave a very good account of those efforts with the second also introducing an important subject, somehow less common to see, of the non-Euclidean geometries.

The subject of readability of the proofs when automated or interactive theorem prover are used is addressed in several contributions. Nicolas Magaud addresses the problem by presenting a framework to carry out a posteriori script transformations of Coq proof scripts. Vesna Marinković et al. demonstrate how their triangle construction solver ArgoTriCS can cooperate with automated theorem provers for first order logic and coherent logic so that it generates construction correctness proofs, that are both human-readable and formal. Salwa Tabet Gonzalez et al. present a framework for completing incomplete conjectures and incomplete proofs. The proposed framework can also help in completing a proof sketch into a human-readable and machine-check-able proofs.

The systems combining dynamic geometry and automated deduction are very important, when the aim is to reach a larger audience than the automated deduction experts. A first paper by Zoltán Kovács et al. describes some on-going improvements concerning the automated reasoning tools developed in GeoGebra Discovery. A second paper by Zoltán Kovács et al. describes the efforts that are being made to resume the development of JGEX, a system that combines the dynamic geometry system with several automated theorem provers and with natural language, with links to visual animations, human-readable proofs.

Milan Banković presents an approach to automated solving of triangle ruler-and-compass construction problems using finite-domain constraint solvers. Pierre Boutry et al. present their progress towards obtaining an independent version of Tarski's System of Geometry, in the form of a variant of Gupta's system. Pedro Quaresma et al. make some considerations on Approaches and Metrics in Automated Theorem Generation/Finding in Geometry, addressing Wos' Problem 31, about the properties that can be identified to permit an automated reasoning program to find new and interesting theorems.

The special focus topic Deduction in Education

This special focus topic addresses the several difficulties, or should we say, opportunities, that must be addressed to open the field of automated deduction to a wider audience, namely to the education community. The talks were all around the tools and problems crossing dynamic geometry systems and automated deduction. In the invited talk by Zlatan Magajna, OK Geometry, he presents a tool for analysing dynamic geometric constructions, observing invariants of dynamic geometric constructions, and generating conjectures. Philip Todd and Danny Aley present GXWeb in the context of proving and mathematical modelling, Zoltán Kovács and other researchers use GeoGebra, GeoGebra Discovery and JGEX to address several problems in mathematical competitions. In two STEAM activities, Anna Käferböck and Zoltán Kovács present an activity, finding the locus of a rocking camel and Thierry Dana-Picard et al. present the visualisation of 2D and 3D curves, with various technologies to use the motivational fascination of outer space from students to connect to mathematical modelling.

Algebraic methods in automated reasoning in geometry

Philip Todd examine a class of geometric theorems on cyclic 2n-gons, proving that if n disjoint pairs of sides are taken, each pair separated by an even number of polygon sides, then there is a linear combination of the angles between those sides which is constant. Hoon Hong et al. present a piece-wise rational reparameterization of curves obtaining a more uniform angular speed obtaining a better rational parameterization of those curves.

The quality of this proceedings is 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 organisers of ADG 2023.

General Chair
Predrag Janičić (University of Belgrade, Serbia)
Program Committee
Francisco Botana (University of Vigo, Spain)
Xiaoyu Chen (Beihang University, China)
Thierry Dana-Picard (Jerusalem College of Technology, Israel)
Jacques Fleuriot (University of Edinburgh, UK)
Tetsuo Ida (University of Tsukuba, Japan)
Zoltán Kovács (The Private University College of Education of the Diocese of Linz, Austria) - Co-chair
Claudia Nalon (University of Brasília, Brazil)
Pavel Pech (University of South Bohemia, České Budějovice, Czechia)
Pedro Quaresma (University of Coimbra, Portugal) - Co-Chair
Tomás Recio (Universidad Antonio de Nebrija, Spain)
Vanda Santos (University of Aveiro, Portugal)
Steven van Vaerenbergh (University of Cantabria, Spain)
María Pilar Vélez (Universidad Antonio de Nebrija, Spain)
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
Christopher Brown (United States Naval Academy, USA)
Xiuquan Ding (University of Chinese Academy of Sciences, China)
Bo Huang (Beihang University, China)
Dongchen Jiang (Beijing Forestry University, China)
Dong Lu (Southwest Jiaotong University, China)
Weifeng Shang (Beihang University, China)
Fanghui Xiao (Hunan Normal University, China)
Local Chair
Vesna Marinković (Faculty of Mathematics, University of Belgrade,Serbia)
Track-chair for Deduction in Education
Filip Marić (University of Belgrade, Serbia)
ADG Steering Committee
Zoltán Kovács (JKU Linz School of Education, Austria), chair
Xiaoyu Chen (Beihang University, China)
Predrag Janičić (University of Belgrade, Serbia)
Hongbo Li (Chinese Academy of Sciences, China)
Vesna Marinković (University of Belgrade, Serbia)
Pedro Quaresma (University of Coimbra, Portugal)
Dongming Wang (Beihang University, China)
Jing Yang (Guangxi University for Nationalities, China)

We would like to express our gratitude to all participants at ADG 2023 and to all those that helped the organisation of ADG 2023 in some way. We would also like to thank the EPTCS staff for their support and efficiency.

January 2024
Pedro Quaresma, Zoltán Kovács
ADG 2023 Program Committee Chairs

Formalization, Arithmetization and Automatization of Geometry

Julien Narboux (University of Strasbourg, France)

In this talk we will present an overview of our work (with Michael Beeson, Pierre Boutry, Gabriel Braun and Charly Gries) about formalization and automation of geometry and the GeoCoq library. We will delve into the axiomatic systems of influential mathematicians such as Euclid, Hilbert and Tarski and present formalization issues. A special focus will be placed on the formalization of continuity axioms and parallel postulates.

We will highlight details and issues that can be seen only through the lens of a proof assistant and intuitionist logic. We will present a syntactic proof of the independence of the parallel postulate.

From axiomatic foundations to computer-assisted proofs, we will explore the intricate interplay between synthetic and analytic geometry, and different kinds of automation.

Julien Narboux, Invited Talk ADG 2023

Formalization, Automatization and Visualization of Hyperbolic Geometry

Filip Marić (University of Belgrade, Serbia)

In this talk we describe our experiences with the formalization, automation and visualization of non-Euclidean geometries.

We start with a formalization of the complex projective line CP(1) (also known as the extended complex plane), its objects (points and circlines) and transformations (Möbius transformations). An algebraic approach is used, where points are described with homogeneous coordinates, circlines are described with Hermitean matrices and Möbius transformations are described using regular matrices. We use the unit disk in CP(1) for the formalization of the Poincaré disk model of hyperbolic geometry and show that it satisfies all Tarski axioms of geometry (with the negated Euclidean axiom).

We also analyze the problem of automatic construction of triangles in absolute and hyperbolic geometry. For this purpose we adapt the software ArgoTriCS. For the visualization of the generated constructions we use ArgoDG: a lightweight JavaScript library for dynamic geometry.

Finally, we introduce the formalization of gyrogroups and gyrovector spaces introduced by Abraham Ungar, which is an alternative approach to formalize hyperbolic geometry inspired by Einstein's special theory of relativity.

ADG23 invited talk, Filip Marić.

OK Geometry

Zlatan Magajna (University of Ljubljana, Slovenia)

Automated observation of dynamic constructions is based on numerical checks of a variety of geometric properties performed on multiple instances of dynamic constructions, where all free points are continuously dragged. Unlike most dynamic geometry systems that incorporate some elements of observation, OK Geometry is a tool developed specifically for the purpose of automated observation of dynamic constructions. The goal of the observations is not to prove facts, but to generate plausible hypotheses about the properties of the observed construction.

In the presentation, we focused on two aspects of observation in addition to the very concept of automated observation. Firstly, we considered the necessary functionalities of software for automated observation. The functionalities range from the possibility of importing dynamic constructions from different dynamic systems, to the management of a database of geometric facts, objects and properties to be considered during the observation, from the possibility of creating implicitly defined geometric objects to the importance of controlling computational errors in numerical checks.

The second focus of the presentation was on the relationship between automated observation, proving and automated provers. Automated observation can be helpful in proving geometric facts as it brings to light properties of a configuration that one may not be aware of. In classroom practice, however, students have difficulty selecting the relevant facts among those automatically observed. It seems that automated observation is particularly useful in combination with automated provers when exploring geometric configurations. Automated observation generates (many) plausible hypotheses about the properties of a geometric configuration that can be proved with a prover.

ADG23 invited talk, Zlatan Magajna.