Below is the list of talks for RWCA'04. There may be a few
changes. A provisional schedule of the talks is also available.
Dongming Wang (Beijing/Paris):
Automated Handling and Proving of Geometric Theorems
In this talk, I will first give a brief review on the history, recent
developments, and current state of automated geometric reasoning, with
emphasis on the role of computer algebra for theorem proving. I will then
discuss how geometric theorems may be specified, manipulated, and proved
automatically. The discussed aspects will be illustrated with live examples
running in my GEOTHER environment. The problem of designing and implementing
a geometric-object-oriented language for symbolic geometric computing and
reasoning will be addressed.
Henk Barendregt (Nijmegen):
The Quest for Correctness
Special Evening Presentation
Bart de Smit (Leiden):
Escher's Print Gallery and the Droste Effect
For a preview see the dedicated web site
Bruce W. Westbury (Warwick):
Finite presentations of spherical categories
The category of representations of a group or
Lie algebra has both a tensor product and a dual. These functors
satisfy relations which are then taken as defining tensor
categories with extra structure. Here we are concerned with
pivotal and spherical categories.
Our main aim is a construction of free spherical categories.
The usual approach is to use isotopy classes of planar diagrams.
Our construction is purely combinatorial. The advantage of this
approach is that we replace isotopy classes by a combinatorial
notion of equivalence. Our construction retains the features of the
diagram construction and in addition is suitable for implementation
on a computer algebra system.
Thomas Bayer (Muenchen):
Computing the stratification of actions of compact Lie groups
We provide a constructive approach to the stratification of the
representation- and the orbit space of
linear actions of compact Lie groups contained in the general linear
group over the reals and we show that our description of orbit spaces
and strata is optimal in the number of inequalities. More precisely, any
stratum, respectively its closure can be described by D sharp,
respectively, relaxed polynomial inequalities, where D is the dimension
and D is also a lower bound for both cases. Additionally we present
SINGULAR implementation of the algorithms and mention differences
between finite and infinite compact Lie groups.
Sergei Haller (Giessen):
Galois cohomology: some aspects of computation and applications
This is a joint project with Arjeh M. Cohen, Scott H. Murray and D.E. Taylor.
We design and implement algorithms for computation with groups of Lie type
in the software package Magma. The goal is to perform computations with
parametrised group elements.
The twisted groups of Lie type are implemented as fixed point subgroups of
untwisted groups of Lie type. The possible twists for a given field extension
and group type are classified by Galois cohomology. We report on current work
to make Galois cohomology effective and on using Galois cohomology to compute
all maximal tori of a given group of Lie type.
F. Botana, T. Recio (Pontevedra/Santander):
Towards Solving the Dynamic Geometry Bottleneck Via a Symbolic Approach
The goal of this short note is to give some simple examples from a
prototype of a recent program, GDI, a Spanish acronym of Intelligent
Dynamic Geometry. Apart from being a standard dynamic geometry
environment, GDI includes, via the cooperation with a symbolic program
(such as Mathematica or CoCoA), enhanced tools for loci generation and
automatic proving, plus another distinguished feature, namely, a
discovery option allowing a user to finding complementary hypotheses for
arbitrary statements to become true, or, in other words, to finding the
missing hypotheses so that a given conclusion follows from a given
(perhaps drastically) incomplete set of hypotheses. The key technique
for all these improvements is the development of an automatic "bridge"
between the graphic and the algebraic counterparts of the program.
Dan Roozemond (Eindhoven):
Automated proofs using bracket algebra with Cinderella and OpenMath
This talk is on the results of a project intended to make it possible to put forward geometrical theorems by pointing and clicking, and then obtain a verifiable proof for that theorem automatically. This goal was achieved by adding various options to the Cinderella , a computer program with which one can create geometrical configurations. In the project the functionality was added to find proofs for these theorems with the aid of the computer algebra package GAP. Communication between these two programs and the various steps in generating the proof is done by means of OpenMath. The proofs are represented by bracket calculations as proposed by Jürgen Richter Gebert in 1995.
Moreover, recently there has been work done on the incorporation of OpenMath in GDI, a geometry program developed at the University in Vigo (Spain). Eventually, Cinderella and GDI should be able to easily exchange geometrical configurations and theorems via OpenMath. In the talk a short introduction on bracket proofs and OpenMath will be given, followed by some demonstrations of Cinderella. There will be plenty of time for discussion and suggestions.
Reinier Bröker (Leiden):
How to construct an elliptic curve with a given number of points
In this talk I will consider the problem of constructing an elliptic
curve with a given number of points. A popular deterministic algorithm
to solve this problem is the `CM-approach'. Classicaly, this algorithm
proceeds via computations over the complex numbers. I will explain how
this works and I will give an CM-algorithm that works over a p-adic field
instead of the complex numbers. The theory will be illustrated with the
actual computation of an elliptic curve with a given number of points.
Sergei Abramov, Denis E. Khmelnov (Moscow):
A note on computing the regular solutions of linear differential systems
We present an approach to find all regular solutions of a system of
linear ordinary differential equations using EG'-algorithm (Abramov,
Bronstein, Khmelnov) as an auxiliary tool. A regular solution of
the differential equation Ly=0 at a fixed point z_0 in C, is a solution
of the form (z-z_0)^lambda*F(z), with F(z) in C((z-z_0))[log(z-z_0)],
where C((z-z_0)) is the field of Laurent series (here we do not consider
convergence problems; all series are formal). Our approach is
a modification of the algorithm from one of the work by M.Barkatou.
This modification does not use the transformation of a system into
a super-irreducible form. Instead, we use EG'-algorithm. Note that
sometimes the transformation into a super-irreducible form as well
as the application of EG'-algorithm is not fast. When we need to
solve a linear differential system of a large size, then it could make
a sense to try both approaches; if we are lucky, at least one (it is
possible that only one) of them will solve the problem.
E. Hubert, N. le Roux (INRIA Sophia-Antipolis/Limoges):
Newton-Hensel algorithm to compute power series solutions to non-linear
ODE of order 1
In this talk, we will present an algorithm combining a Newton method
and a Hensel lifting in order to compute power series solutions to non linear
ODE of order 1.
The basic step of the Newton method
is to double the number of known coefficients of the
power series solution using the
linearisation of the equation at the known approximation.
In a previous work, we generalized this method to systems of
partial differential equations . The method works for so called
regular differential systems and any polynomially nonlinear
differential systems can be rewritten in terms of those.
The Newton methods mentionned above lend themselves to modular
computations. Our goal now is to recover the exact power series solution
from the modular computations with a Hensel lifting. As a first stage
we explore the case of first order ordinary differential equations.
We first obtain a bound on the coefficients.
We expect that we can generalize that approach to PDE systems.
Ha Le, Ziming Li (INRIA Rocquencourt/Waterloo):
Differential rational normal forms and representations of hyperexponential
We describe differential rational normal forms
of a rational function and their properties.
Based on these normal forms, we show how to
construct a multiplicative decomposition of
a hyperexponential function, and present an
algorithm which solves the additive decomposition
problem of a hyperexponential function. This
algorithm can be used to accelerate the differential
Gosper's algorithm and to compute right factors of
Mark Giesbrecht, George Labahn, Wen-shin Lee (Waterloo/INRIA Sophia-Antipolis):
Symbolic-numeric sparse interpolation of multivariate polynomials
We consider the problem of interpolating sparse, black-box, multivariate
polynomials in an environment where all computations are done with a fixed,
finite precision. We present two interpolation methods that are sensitive to
the number of terms in the target polynomial. One is a modification of the
Ben-Or/Tiwari sparse interpolation algorithm that is designed for exact
arithemtic. The other is based on the reformulation of Prony's method as a
generalized eigenvalue problem, and our observation of the similarity between
the Ben-Or/Tiwari algorithm and Prony's method. We examine the numerical
sensitivity of these methods.
Hitoshi Yanami, Hirokazu Anai (Fujitsu-Kawasaki/CREST-Kawaguchi):
SyNRAC: A Maple package for solving real algebraic constraints
We present newly developed functions in Maple-package SyNRAC, for
solving real algebraic constraints derived from various engineering
problems. The current version of SyNRAC provides quantifier
elimination (QE) for up to the quadratic case and a new environment
dealing with first-order formulas over the reals (including new
simplifiers of formulas) on Maple.
A.N. Prokopenya (Brest):
Computation of the stability boundaries in the linear Hamiltonian systems
with periodic coefficients
We consider the hamiltonian system of linear differential
equations with periodic coefficients. Using the method based on
the existence of periodic solutions on the boundaries between the
domains of stability and instability we have developed the
algorithm for computation of the stability boundaries. The
algorithm has been realized for the fourth order hamiltonian
system arising in the restricted many-body problems. The stability
boundaries have been found in the form of powers series, accurate
to the fifth order in a small parameter. All the computations are
done with the computer algebra system Mathematica.
Systems and Packages
J. Abbott, et al (CoCoA-Genova):
Presentation of CoCoA 5
One of the products of the long running CoCoA project specialised
in Computations in Commutative Algebra is a freely available
interactive system offering good implementations of many algorithms in
that area. This program (currently CoCoA 4.3) has been, and still
is, highly successful; indeed it has grown far beyond what was
foreseen when its foundations were laid. The similarly specialized
systems Macaulay 2 and Singular have their own special strengths.
CoCoA 5 is an important new phase in the project: the program is
being completely rewritten in C++. This obviates various limitations
innate in the earlier design (written in C). CoCoA 5 will be
available in three guises: an interactive system, a C++ library, and a
server (using an OpenMath-like interface). Ease of use is a high
priority for all three forms. Currently there is an `alpha' release
of the library.
The new library already offers facilities for computing Gröbner
bases beyond those present in version 4.3: e.g. more coefficient types,
and better execution speed. Version 4.3 also boasts a range of other
skills including polynomial factorization, exact linear algebra,
Hilbert functions, and computing with zero-dimensional schemes.
CoCoA 5 will gradually grow to cover each of these skills, and
ultimately extend the repertoire.
Unlike general purpose symbolic computation systems CoCoA does not offer
facilities for calculus or any other area not closely related to commutative
polynomial algebra. The CoCoA project is closely allied to this book:
M. Kreuzer, L. Robbiano
Computational Commutative Algebra 1,
Springer (2000), ISBN 3-540-67733-X
A Magma package
The groups of Lie type are among the most important structures in
modern mathematics. Examples of such groups include reductive Lie groups,
reductive algebraic groups, and finite groups of Lie type (which include
most of the finite simple groups). Many problems in the representation theory
of groups of Lie type have been solved using computers (for example, by
the CHEVIE group). In this talk, I discuss descriptions of
these groups (via the Steinberg presentation or highest
weight representations) that are useful for computation. I also
give methods for dealing with the twisted groups using Galois cohomology
and Lang's theorem.
This talk describes joint work with Arjeh Cohen, Sergei Haller, and Don
Jos Vermaseren (NIKHEF, Amsterdam):
Symbolic Manipulation with FORM
FORM is a symbolic system for the fast manipulation of large expressions.
I will show a number of its features and properties.