Skip to main content

Über dieses Buch

This book constitutes the thoroughly refereed post-workshop proceedings of the 8th International Workshop on Automated Deduction in Geometry, ADG 2010, held in Munich, Germany in July 2010.
The 13 revised full papers presented were carefully selected during two rounds of reviewing and improvement from the lectures given at the workshop. Topics addressed by the papers are incidence geometry using some kind of combinatoric argument; computer algebra; software implementation; as well as logic and proof assistants.



Cancellation Patterns in Automatic Geometric Theorem Proving

This article is about the equivalence of two seemingly different methods for proving incidence theorems in projective geometry. The first proving method is essentially an algebraic certificate for the non-existence of a counterexample—via biquadratic final polynomials [13]. For the second method the theorems of Ceva and Menelaus are elementary building blocks and are used as faces of an oriented topological 2-cycle, with their geometric structure on the edges identified appropriately. The fact that the cycle finally closes up translates into the proof of the theorem. We start by formalizing both methods. After this we present a bijective translation process that establishes the equivalence of the two methods. The proving methods and the translation process will be illustrated by a (quite well-natured) example. Using our methods one gains additional structural insight in the purely algebraic proofs (biquadratic final polynomials) by reconstructing an underlying topological structure of the proof.
Susanne Apel, Jürgen Richter-Gebert

Exploring the Foundations of Discrete Analytical Geometry in Isabelle/HOL

This paper gives an overview of the formalization of the Harthong-Reeb integer number system (HR ω ) in the proof-assistant Isabelle. The work builds on an existing mechanization of nonstandard analysis and describes how the basic notions underlying HR ω can be recovered and shown to have their expected properties, without the need to introduce any axioms. We also look at the formalization of the well-known Euler method over the new integers and formally prove that the algorithmic approximation produced can be made to be infinitely-close to its continuous counterpart. This enables the discretization of continuous functions and of geometric concepts such as the straight line and ellipse and acts as the starting point for the field of discrete analytical geometry.
Jacques Fleuriot

A Formalization of Grassmann-Cayley Algebra in COQ and Its Application to Theorem Proving in Projective Geometry

This paper presents a formalization of Grassmann-Cayley algebra [6] that has been done in the COQ [2] proof assistant. The formalization is based on a data structure that represents elements of the algebra as complete binary trees. This allows to define the algebra products recursively. Using this formalization, published proofs of Pappus’ and Desargues’ theorem [7,1] are interactively derived. A method that automatically proves projective geometric theorems [11] is also translated successfully into the proposed formalization.
Laurent Fuchs, Laurent Théry

Automatic Calculation of Plane Loci Using Gröbner Bases and Integration into a Dynamic Geometry System

We describe the integration of a well known algorithm for computing and displaying plane loci based on ideal elimination using Gröbner bases in the dynamic geometry software JSXGraph. With our approach it is not only possible to determine loci depending on other loci but it is also possible to extend JSXGraph to deal with loci depending on arbitrary plane algebraic curves. For Gröbner bases calculations we use CoCoa, a computer algebra system with its focus on computations in commutative algebra.
Michael Gerhäuser, Alfred Wassermann

Proof Documents for Automated Origami Theorem Proving

A proof document for origami theorem proving is a record of entire process of reasoning about origami construction and theorem proving. It is produced at the completion of origami theorem proving as a kind of proof certificate. It describes in detail how the whole process of an origami construction and the subsequent theorem proving are carried out in our computational origami system. In particular, it describes logical and algebraic transformations of the prescription of origami construction into mathematical models that in turn become amenable to computation and verification. The structure of the proof document is detailed using an illustrative example that reveals the importance of such a document in the analysis of origami construction and theorem proving.
Fadoua Ghourabi, Tetsuo Ida, Asem Kasem

The Midpoint Locus of a Triangle in a Corner

We are given an equilateral triangle with vertices constrained to lie in each of the three positive octant coordinate planes (colloquially, “a triangle in a corner”). We wish to describe the locus of points covered by the midpoint of the triangle, as the vertices range over configurations allowed by the above constraint. This locus comprises a solid region. We use numerical and graphical methods, and also computational algebra, to find the boundary surface and visualize this locus.
Daniel Lichtblau

Some Lemmas to Hopefully Enable Search Methods to Find Short and Human Readable Proofs for Incidence Theorems of Projective Geometry

Search methods provide short and human readable proofs, i.e. with few algebra, of most of the theorems of the Euclidean plane. They are less succesful and convincing for incidence theorems of projective geometry, which has received less attention up to now. This is due to the fact that basic notions, like angles and distances, which are relevant for Euclidean geometry, are no more relevant for projective geometry. This article suggests that search methods can also provide short and human readable proofs of incidence theorems of projective geometry with well chosen notions, rules or lemmas. This article proposes such lemmas, and show that they indeed permit to find by hand short proofs of some theorems of projective geometry.
Dominique Michelucci

What Is a Line ?

The playground is the projective complex plane. The article shows that usual, naive, lines are not all lines. From naive lines (level 0), Pappus geometry creates new geometric objects (circles or conics) which can also be considered as (level 1) lines, in the sense that they fulfil Pappus axioms for lines. But Pappus theory also applies to these new lines. A formalization of Pappus geometry should enable to automatize these generalizations of lines.
Dominique Michelucci

On One Method of Proving Inequalities in Automated Way

The paper describes proving geometric inequalities in automated way without cell decomposition. Firstly an overview of known methods of proving inequalities is given including the method which is based on reduction of a conclusion polynomial to the canonical form modulo a hypotheses ideal. Then a parametrization method of proving geometric inequalities is introduced. Further a method of proving geometric inequalities which introduces an auxiliary polynomial is described.
Pavel Pech

Thousands of Geometric Problems for Geometric Theorem Provers (TGTP)

Thousands of Geometric problems for geometric Theorem Provers (TGTP) is a Web-based library of problems in geometry.
The principal motivation in building TGTP is to create an appropriate context for testing and evaluating geometric automated theorem proving systems (GATP). For that purpose TGTP provides a centralised common library of geometric problems with an already significant size but aiming to became large enough to ensure meaningful system evaluations and comparisons. TGTP provides also a workbench were it is possible to test any given geometric conjecture.
TGTP is independent of any given GATP. For each problem the code for each GATP (whenever available) is kept in the library. A common format for geometric conjectures, extending the i2g format, is being developed. This common format, plus a list of converters, one for each GATP, will allow to test all the GATPs with all the problems in the library.
TGTP is well structured, documented and with a powerful querying mechanism, allowing an easy access to the information. All information in the library, and also the supporting formats and tools are freely available.
TGTP aims, in a similar spirit of TPTP and other libraries, to provide the automated reasoning in geometry community with a comprehensive and easily accessible library of GATP test problems. The development of TGTP problem library is an ongoing project.
Pedro Quaresma

An Investigation of Hilbert’s Implicit Reasoning through Proof Discovery in Idle-Time

In this paper, we describe how we captured and investigated incidence reasoning in Hilbert’s Foundations of Geometry by using a new discovery tool integrated into an interactive proof assistant. Our tool exploits concurrency, inferring facts independently of the user with the incomplete proof as a guide. It explores the proof space, contributes tedious lemmas and discovers alternative proofs. We show how this tool allowed us to write readable formalised proof-scripts that correspond very closely to Hilbert’s prose arguments.
Phil Scott, Jacques Fleuriot

A Coherent Logic Based Geometry Theorem Prover Capable of Producing Formal and Readable Proofs

We present a theorem prover ArgoCLP based on coherent logic that can be used for generating both readable and formal (machine verifiable) proofs in various theories, primarily geometry. We applied the prover to various axiomatic systems and proved tens of theorems from standard university textbooks on geometry. The generated proofs can be used in different educational purposes and can contribute to the growing body of formalized mathematics. The system can be used, for instance, in showing that modifications of some axioms do not change the power of an axiom system. The system can also be used as an assistant for proving appropriately chosen subgoals of complex conjectures.
Sana Stojanović, Vesna Pavlović, Predrag Janičić

Automated Generation of Readable Proofs for Constructive Geometry Statements with the Mass Point Method

The existing readable machine proving methods deal with geometry problems using some geometric quantities. In this paper, we focus on the mass point method which directly deals with the geometric points rather than the geometric quantities. We propose two algorithms, Mass Point Method and Complex Mass Point Method, which can deal with the Hilbert intersection point statements in affine geometry and the linear constructive geometry statements in metric geometry respectively. The two algorithms are implemented in Maple as provers. The results of hundreds of non-trivial geometry statements run by our provers show that the mass point method is efficient and the machine proofs are human-readable.
Yu Zou, Jingzhong Zhang


Weitere Informationen

Premium Partner