Resúmenes - Abstracts

Maria Emilia Alonso


In the talk we give an approach to some topics of Computational Algebra as standard bases computation and canonical forms in the setting of algebraic power series.
Our main motivation to deal with these problems comes from Algebraic Geometry, where Algebraic functions appear in
describing the local structure of algebraic varieties at a point.
There is a second more abstract motivation. The henselization of a local ring A is ``unique" in an strong way, (as for instance it is the real clousure of an ordered field); it is unique up to unique A--homomorphism. So that, in a more general setting we are dealing with describing, say constructively, the henselization of a local ring.
This is the approach where we show how we can manipulate the henselization of a local ring in a dynamic way through some essentially finite $A$ algebras.

The talk present results from joint works: old results, and new ones in progress with Castro and Hauser, and, Lombardi and Pedry. Our approach to compute in the ring of algebraic power series is the representation, based in the fact that an algebraic function locally is a component of a vector of solutions to a polynomial system of equations verifiying IFT at a point.

That representation allows to compute standard bases and the initial monomial ideal or the set of leading (minimal) terms E={ in(I) of a given ideal I of the ring of algebraic power series, wr.t. a local term ordering. We identify E=in(I) with a subset of Nn. By Hironaka Henselian Division Theorem it is known that quotients and remainders of the formal division by ( an standard basis of ) I are still algebraic series, provided E verifies a finiteness condition called ``box condition".
We achieve to have an effective version of this theorem, that is to effectively compute canonical forms, in some cases including Weierstrass division theorem.

For, we introduce a new reduction process of a polynomial w.r.t. a set of polynomials whose leading monomials generate an ``escalier" which has this finitness condition. In fact this process is very general and does not required to fix any term ordering for considering the leading (maximal) monomials of polynomials: one can fix freely the ``leading monomials" with the only condition to be maximal in the partial order of semigroup. We use old ideas of Janet to make a suitable partition of the set leading terms E.

Robert Corless 


This talk outlines some new algorithms for operations on multivariate
polynomials. The point of view taken in the talk is a dual viewpoint,
namely that all polynomials considered are given by their values at known points, and that the degrees of the polynomials are known or can be deduced. The first nontrivial
algorithm considered is division; then Bezout matrices, generalized
companion matricies, GCD, and the solution of zero-dimensional
polynomial systems are investigated. A new algorithm is given for such
solution: neither Gröbner basis nor resultant-based, it shares some
characteristics with resultant algorithms.

A preprint of a paper detailing this talk can be found at This is joint
work with Laureano Gonzalez-Vega, Amir Amiraslani, and Azar Shakoori.

Michel Coste 


This talk is intended to present the work of a group including
researchers in robotics, computer algebra and geometry and studying the
possible behaviours of a simple manipulator when one varies the design
parameters (length of arms, offset). One important aspect of this
behaviour is the ability to change posture without crossing
singularities. The output of the work is a partition of the space of
parameters into cells where the behaviour remains the same.
We plan to emphasize the interplay between the algebraic modelisation
of the problem, the use of specialized computer algebra tools and the
geometric analysis of occurring phenomena.

David Cox 


The talk would discuss implicitization using A) resultants and B) moving surfaces and C) relations between the two. The talk would illustrate how concrete questions in implicitization leads naturally to concepts in commutative algebra such as syzygies, free resolutions, regularity, and local complete intersections. The talk would be down-to-earth but the moral would be that serious commutative algebra is involved. There would be lots of examples.

Peter Olver


In this talk, I will describe a new approach to the powerful Cartan theory of moving frames. The method is completely algorithmic, and applies to very general Lie group actions. I hope to discuss a wide variety of new applications, including classification of differential invariants, geometrical equivalence of curves and surfaces, symmetries of polynomials in classical invariant theory, object recognition in computer vision, invariant variational problems, and the design of symmetry-preserving numerical approximations. the emphasis will be on computer algebra aspects of the methods.

José Luis Ruiz Reina


Verificar formalmente un programa significa demostrar, usando una lógica formal, que el programa cumple con las propiedades de corrección que se esperan del mismo, expresando igualmente estas propiedades en la misma lógica. Nuestra confianza en los cálculos realizados por un programa se verá incrementada sustancialmente si éste ha sido formalmente verificado. Usualmente, esta verificación formal se lleva a cabo con la ayuda de algún sistema de demostración automática de teoremas.

En esta conferencia, pretendemos explicar técnicas que pueden ser aplicadas a la verificación formal de algoritmos implementados en sistemas de cálculo simbólico. En este caso, además del esfuerzo de verificación usual que se necesita para demostrar la corrección de cualquier proceso computacional, debemos formalizar también toda la rica y extensa teoría matemática necesaria
para poder expresar las propiedades de corrección de los programas. En particular, describiremos nuestra experiencia con el
demostrador de teoremas ACL2, usado para implementar y verificar algunos algoritmos bien conocidos presentes en la mayoría de los sistemas de cálculo simbólico.


Formal verification of a program means the act of proving, using a formal logic, that the program meets its intended correctness
properties, formally expressed in the same logic. Our confidence in the results computed by a program increases if it is formally
verified. Usually, this formal verification is carried out with the assistance of a mechanized reasoning system.

In this talk, we intend to explain how we can formally verify some algorithms typically implemented in symbolic computation systems. In
this case, in addition to the usual verification effort needed to prove correctness properties of the computation processes implemented, we must formalize also all the (usually rich) mathematical theory needed to express the properties of the program. In particular, we show our experience with the use of the ACL2 mechanized reasonig system for the implementation and verification of some well-known algorithms present in most of symbolic computation systems.

Renaud Rioboo


The talk presents the main features of the FoC programming environment
and its basic notions. Going through the example of an implementation of
distributed and recursive polynomials we introduce some FoC concepts. FoC's species
and collections allow to give a mathematical view of FoC types and values
of a type are safely interpreteds as mahematical objects.

We will present the static analysis performed in FoC and show that data
type safety can be achieved.