Catálogo de publicaciones - libros

This paper proposes a system in the form of a textbook for managing geometric knowledge dynamically, effectively, and interactively. Such a system, called an , can be viewed or printed as a traditional textbook and run as dynamic software on computer. The knowledge in the textbook is being formalized by using standard formal languages and may be processed by software modules developed for geometric computing and reasoning, diagram generation, and visualization. The textbook can be generated automatically by organizing and presenting the textbook data according to some specifications. The system allows the user to manipulate (query, modify, restructure, etc.) the textbook with automated consistency checking. We present the main ideas on the design of the electronic geometry textbook, explain the features of the system, propose five phases of creating and managing the geometric knowledge in the textbook, discuss the involved tasks and some of the fundamental research problems in each phase, and report our progress and experiments on a preliminary implementation of the system.

This article describes an algorithm that decides whether a region in three dimensions, described by quadratic constraints, is equidecomposable with a collection of primitive regions. When a decomposition exists, the algorithm finds the volume of the given region. Applications to the ‘Flyspeck’ project are discussed.

We present an application of automatic theorem proving (ATP) in the verification of constructions made with dynamic geometry software (DGS). Given a specification language for geometric constructions, we can use its processor to deal with syntactic errors. The processor can also detect semantic errors — situations when, for a given concrete set of geometrical objects, a construction is not possible. However, dynamic geometry tools do not test if, for a given set of geometrical objects, a construction is geometrically sound, i.e., if it is possible in a general case. Using ATP, we can do this last step by verifying the geometric constructions deductively. We have developed a system for the automatic verification of regular constructions (made within DGSs GCLC and Eukleides), using our ATP system, GCLCprover. This gives a real-world application of ATP in dynamic geometry tools.

We propose an algorithm for automated recognition of computationally constructed curves and discuss several aspects of the recognition problem. Recognizing loci means determining a single implicit polynomial equation and geometric invariants, characterizing an algebraic curve which is given by a discrete set of sample points. Starting with these discrete samples, arising for example from a geometric ruler and compass construction, an eigenvalue analysis of a matrix derived from the data leads to proposed curve parameters. Utilizing the construction itself, with its free and dependent geometric elements, further specifications of the type of constructed curves under genericity assumptions are made. This is done by a second eigenvalue analysis of parameters of several generically generated curves.

This paper describes the recent convergence of four topics: polynomial systems, flexibility of three dimensional objects, computational chemistry, and computer algebra. We discuss a way to solve systems of polynomial equations with . Using ideas of Bricard, we find a system of polynomial equations that models a configuration of quadrilaterals that is equivalent to some three dimensional structures. These structures are of interest in computational chemistry, as they represent molecules. We then describe an algorithm that examines the resultant and determines ways that the structure can be

It is known that five points in ℝ generically determine a finite number of cylinders containing those points. We discuss ways in which it can be shown that the generic (complex) number of solutions, with multiplicity, is six, of which an even number will be real valued and hence correspond to actual cylinders in ℝ. We partially classify the case of no real solutions in terms of the geometry of the five given points. We also investigate the special case where the five given points are coplanar, as it differs from the generic case for both complex and real valued solution cardinalities.

In geometric constraints solving, the detection of dependences and the decomposition of the system into smaller subsystems are two important steps that characterize any solving process, but nowadays solvers, which are graph-based in most of the cases, fail to detect dependences due to geometric theorems and to decompose such systems. In this paper, we discuss why detecting all dependences between constraints is a hard problem and propose to use the witness method published recently to detect both structural and non structural dependences. We study various examples of constraints systems and show the promising results of the witness method in subtle dependences detection and systems decomposition.

The main proposal in this paper is the merging of two techniques that have been recently developed. On the one hand, we consider a new approach for computing some specializable Gröbner basis, the so called Minimal Canonical Comprehensive Gröbner Systems (MCCGS) that is -roughly speaking- a computational procedure yielding “good” bases for ideals of polynomials over a field, depending on several parameters, that specialize “well”, for instance, regarding the number of solutions for the given ideal, for different values of the parameters. The second ingredient is related to automatic theorem discovery in elementary geometry. Automatic discovery aims to obtain complementary (equality and inequality type) hypotheses for a (generally false) geometric statement to become true. The paper shows how to use MCCGS for automatic discovering of theorems and gives relevant examples.

This paper describes the mechanization of the proofs of the first height chapters of Schwabäuser, Szmielew and Tarski’s book: . The proofs are checked formally using the Coq proof assistant. The goal of this development is to provide foundations for other formalizations of geometry and implementations of decision procedures. We compare the mechanized proofs with the informal proofs. We also compare this piece of formalization with the previous work done about Hilbert’s . We analyze the differences between the two axiom systems from the formalization point of view.

The paper deals with a problem of finding natural geometry problem, that is, not specifically built up for the only purpose of having some concrete property, where the hypothesis is not described by a radical ideal. This problem was posed by Chou long ago. Regular polygons in the Euclidean space and their existence in spaces of various dimensions are studied by the technique of Gröbner bases. When proving that regular pentagons and heptagons span spaces of even dimension one encounters the case that the ideal describing the hypotheses is not radical. Thus, in order to prove that one needs to show that belongs to the radical of the ideal describing .