|
Published: 22nd January 2024 DOI: 10.4204/EPTCS.398 ISSN: 2075-2180 |
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.
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
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
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ć.
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.