Catálogo de publicaciones - libros

Algorithms for solving geometric problems are widely used in many scientific disciplines. Applications range from computer vision and robotics to molecular biology and astrophysics. Proving the correctness of these algorithms is vital in order to boost confidence in them. By specifying the algorithms formally in a theorem prover such as Isabelle, it is hoped that rigorous proofs showing their correctness will be obtained. This paper outlines our current framework for reasoning about geometric algorithms in Isabelle. It focuses on our case study of the convex hull problem and shows how Hoare logic can be used to prove the correctness of such algorithms.

Construction of geometrical objects by origami, the Japanese traditional art of paper folding, is enjoyable and intriguing. It attracted the minds of artists, mathematicians and computer scientists for many centuries. Origami will become a more rigorous, effective and enjoyable art if the origami constructions can be visualized on the computer and the correctness of the constructions can be automatically proved by an algorithm. We call the methodology of visualizing and automatically proving origami constructions computational origami. As a non-trivial example, in this paper, we visualize a construction of a regular heptagon by origami and automatically prove the correctness of the construction.

The notion of partitioned-parametric Gröbner bases of a polynomial ideal under constraints is introduced and an algorithm for constructing partitioned-parametric Gröbner bases is given; the correctness and the termination of the algorithm are proved. We also present a method based on computing partitioned-parametric Gröbner bases for proving geometric theorems mechanically. By this method, besides proving the generic truth of a geometric theorem, we can give the necessary and sufficient conditions on the free parameters for the theorem to be true. An example for proving geometric theorems by the partitioned-parametric Gröbner bases method is given.

Some properties of inscribed polygons, i.e., such plane polygons whose vertices lie on a circle, are investigated. Given an inscribed polygon with the lengths of its sides, we explore the area and radius of its circumcircle. We start with a triangle and a quadrangle and then we will explore the case of a pentagon. All the computations are based on results of commutative algebra especially on Gröbner bases method and elimination of variables in a given ideal.

This paper presents a symbolic solution to a piano movers’ problem with four parameters through investigating the positive definiteness of an even polynomial of degree 8 and the feasibility of certain inequality systems.

A few years ago S-H Kim investigated some problems at the boundary of number theory, optimization, and geometry. One question regarded an optimal packing of certain “triangular oval” planar curves and another looked at some related transformations of ℝ to ℝ. These were investigated primarily using tools from calculus but it turns out that computational algebra methods may instead be employed to particular advantage. Moreover, generalizations that are beyond the reach of such methods are still amenable to hybrid approaches using numeric and symbolic methods in tandem. We introduce some of the specific problems and generalizations, and show by detailed example how such techniques may be implemented and deployed.

The goal of this paper is to report on a prototype of a new dynamic geometry software, GDI (Geometría Dinámica Inteligente). We will describe how, apart from being a standard dynamic environment for elementary geometry, GDI addresses some key problems of the dynamic geometry paradigm, by including enhanced tools for loci generation and automatic proving, plus another distinguished feature, namely, a option, allowing the user to find complementary hypotheses for arbitrary statements to become true. The key technique for all these improvements is the development of an automatic “bridge” between the graphic and the algebraic counterparts of the program (calling on an external computer algebra system).

We investigate two important problems arising in Dynamic Geometry, the and the . After presenting purely algebraic algorithms for these problems, we give an alternative approach.

This paper proposes a geometric-object-oriented language for symbolic geometric computation, reasoning, and visualization. In this language, geometric objects are constructed with indefinite parametric data. Modifications and basic operations on these objects are enabled. Degeneracy and uncertainty are handled effectively by means of imposing conditions and assumptions and geometric statements are formulated by declaring relations among different objects. A system implemented on the basis of this language will allow the user to perform geometric computation and reasoning rigorously and to prove geometric theorems and generate geometric diagrams and interactive documents automatically. We present the overall design of the language, explain the capabilities, features, main components of the proposed system, provide specifications for some of its functors, report our experiments with a preliminary implementation of the system, and discuss some encountered difficulties and research problems.

In this paper, we propose a symbolic-numerical algorithm for collision-free placement and motion of an object avoiding collisions with obstacles. The algorithm is based on the combination of configuration space and energy approaches. According to the configuration space approach, the position and orientation of the geometric object to be moved or placed is represented as an individual point in a configuration space, in which each coordinate represents a degree of freedom in the position or orientation of this object. The configurations which, due to the presence of obstacles, are forbidden to the object, can be characterized as regions in this configuration space called configuration space obstacles. As will be demonstrated, configuration space obstacles can be computed symbolically using quantifier elimination over the reals and represented by polynomial inequalities. We propose to use the functional representation of semi-algebraic point sets defined by such inequalities, so-called R-functions, to describe nonlinear geometric objects in the configuration space. The potential field defined by R-functions can be used to “move” objects in such a way as to avoid collisions. Introducing the additional function, which forces the object towards the goal position, we reduce the problem of finding collision free path to a solution of the Newton’s equations, which describes the motion of a body in the field produced by the superposition of “attractive” and “repulsive” forces. These equations can be solved iteratively in a computationally efficient manner. Furthermore, we investigate the differential properties of R-functions in order to construct a suitable superposition of attractive and repulsive potentials.