Maria Emilia Alonso
|ALGEBRAIC POWER SERIES: REPRESENTATION AND EFFECTIVENESS OF DIVISION
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.
|POLYNOMIAL ALGEBRA BY VALUES
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
http://www.orcca.on.ca/TechReports/2004/TR-04-01.html. This is joint
work with Laureano Gonzalez-Vega, Amir Amiraslani, and Azar Shakoori.
|CLASSIFYING SERIAL MANIPULATORS:
COMPUTER ALGEBRA AND GEOMETRIC INSIGHT.
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.
|IMPLICITATION AND COMMUTATIVE ALGEBRA
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.
|COMPUTATIONAL ASPECTS OF MOVING FRAMES
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
|VERIFICACION FORMAL Y SISTEMAS DE CALCULO SIMBOLICO
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 AND SYMBOLIC COMPUTATION SYSTEMS
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.
|CERTIFYING COMPUTER ALGEBRA PROGRAMS,
DATA SAFETYIN THE FoC LANGUAGE
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.