Overview
The focus of this workshop is on algorithms for polynomials, and their certification,
having in mind the geometric study of algebraic and semi-agebraic sets and
their applications..
Algebraic Algorithms for Polynomials Solving systems of polynomial
equations is a fundamental problem in computer algebra, with applications
in many areas. In recent years, algorithms for polynomial system solving
have been applied in domainsas diverse as cryptology (through attacks on
several multivariate cryptosystems, computations of discrete logarithms
in finite elds or on elliptic curves), statistics, the formal verification
of programs and many other areas. Popular approaches include of course Grobner
bases computations, but also triangular decomposition algorithms, or methods
based on toric geometry for sparse systems.Recently there have been a series
of improvements in both algorithms and implementation, resulting in orders
of magnitude faster performance, systems which were out of far reach a few
years ago being now routinely solved.
Computations in Real Algebraic Geometry Real algebraic geometry
mainly concerns the study of semi-algebraic sets. Computational aspects
in real algebraic geometry are renewed by connections with other areas of
mathematics and computer science, such as optimization, control theory robotics,
computer aided geometric design, incidence theory and game theory. Recently,
there has been significant progress in many problems, such as the quadratic
and symmetric case, road map computation and constructive aspects in Hilbert's
17th problem. Much attention is given to certificates of positivity using
Bernstein bases, or sums of squares, with connections to semi-definite programming.
Certified Algorithms, Computer Algebra and Proofs Formalization
of mathematics is currently a very active topic. There is progress on the
foundational aspect as well as on the formalization of significant mathematical
results. The impact on computer algebra is both theoretical, since constructive
mathematics can help clarifying delicate algorithmic issues in computer
algebra, and practical with the integration of computer algebra software
and proof assistants. The impact of proof assistantson closely related areas
such as computer-assisted manipulations and proofs of combinatorial identities,
simplification of hypergeometric sums and more general special function
expressions as well as computations in algebraic topology will be also discussed.
Schedule
| Monday,
December 7 |
|
8:15-8:45
|
On site registration and morning coffee |
|
8:45-9:00
|
Welcoming remarks |
|
9:00-9:50
|
Frank Sottile, Texas A&M University
Numerical Schubert Calculus |
|
9:55-10:45
|
Martin Helmer, University of California,
Berkeley (SLIDES)
Algorithms to Compute Characteristic Classes
of Subschemes of Certain Toric Varieties |
|
10:45-11:10
|
Coffee break |
|
11:10-12:00
|
Robert Krone, Queen's University
(SLIDES)
Equivariant Gröbner bases |
|
12:00-14:40
|
Lunch break |
|
14:40-15:30
|
Jose Rodriguez, University of Chicago
Numerically computing Galois groups
|
|
15:30-15:55
|
Coffee break |
|
15:55-16:45
|
Carlos d'Andrea,Universitat de Barcelona
(SLIDES)
Sparse Eliminants vs Sparse Resultants |
|
17:00
|
Reception at Fields |
| Tuesday, December
8 |
|
9:00-9:50
|
Pierre-Jean Spaenlehauer,
Inria (SLIDES)
Sparse polynomial systems with many positive
solutions from bipartite simplicial complexes |
|
9:55-10:45
|
Elias Tsigaridas,
INRIA Paris
Separation bounds for polynomial systems
|
|
10:45-11:10
|
Coffee Break
|
|
11:10-12:00
|
Jean-Charles Faugere,
Inria
Sparse-FGLM and Linear Recursive Multidimensional
Sequences
|
|
12:00-14:40
|
Lunch |
|
14:40-15:30
|
Marc Moreno Maza,
The University of Western Ontario
Limit Points of Constructible Sets |
|
15:30-15:55
|
Coffee Break
|
|
15:55-16:45
|
Mari Emi Alonso,
Complutense University (SLIDES)
Abstract local Bezout theorems and other constructive
aspects of Henselian rings |
| Wednesday,
December 9 |
|
9:00-9:50
|
Fabrice Rouillier,
INRIA Paris
Computing intersections of two algebraic plane
curves : the price of the certification |
|
9:55-10:45
|
Marie-Francoise Roy,
Université de Rennes 1 (SLIDES)
Quantifier elimination for real closed fields :
a purely algebraic variant of CAD |
|
10:45-11:10
|
Coffee Break |
|
11:10-12:00
|
Guillaume Moroz,
INRIA Nancy-Grand Est
On the computation of the silhouette of an analytic
surface |
|
12:00-13:40
|
Lunch break |
|
13:40-14:30
|
Mehdi Ghasemi,University
of Saskatchewan (SLIDES)
Application of geometric programming in polynomial
optimization |
|
14:40-15:30
|
Michel Coste, Université
de Rennes 1
Geometry and Symbolic Computation for Analyzing
the Singularities of Parallel Robots |
|
15:30-15:55
|
Coffee Break
|
|
15:55-16:45
|
Mohab Safey El Din,
University Pierre et Marie Curie
On nearly optimal algorithms for computing
roadmaps |
|
16:55-17:45
|
Eric Schost, University
of Waterloo
Using linearly recursive sequences to solve polynomial
systems |
| Thursday,
December 10 |
|
9:00-9:50
|
Greg Blekherman,
Georgia Institute of Technology
Degree bounds in sums of squares representations
|
|
10:00 -
|
Free time making it possible
to attend the Grothendieck Memorial Day for those who wish: https://www.fields.utoronto.ca/programs/scientific/15-16/grothendieck/ |
| Friday,
December 11 |
|
9:00-9:50
|
Michael Sagraloff,
Max Planck Institute for Informatics
On the Complexity of Solving Polynomial Systems
via Projection |
|
9:55-10:45
|
Gabriela Jeronimo,
Universidad de Buenos Aires (SLIDES)
A zero counting symbolic procedure for a class
of univariate Pfaffian functions |
|
10:45-11:10
|
Coffee Break |
|
11:10-12:00
|
Rainer Sinn, Georgia
Institute of Technology
Sums of squares on projective varieties |
|
12:00-13:45
|
Lunch |
|
14:40-15:30
|
Saugata Basu, Purdue
University (SLIDES)
Complexity of constructible sheaves |
|
15:30-15:55
|
Coffee Break |
|
15:55-16:45
|
Cynthia Vinzant,
North Carolina State University (SLIDES)
Numerical methods for computing real and complex
tropical curves |
|
16:55-17:45
|
Cordian Riener,
Aalto University
Topological complexity of symmetric semi-algebraic
sets |
| Saturday,
December 12 |
|
9:00-9:50
|
Lihong Zhi,
Chinese Academy of Sciences
A certificate for semidefinite relaxations in computing
positive-dimensional real radical ideals |
|
9:55-10:45
|
Michael Burr, Clemson
University
Continuous Amortization: Intrinsic Geometric Complexity
for Subdivision-based Algorithms |
|
10:45-11:10
|
Coffee Break |
|
11:10-12:00
|
Jonathan Hauenstein,
University of Notre Dame
Local decomposition and local methods for
analyzing real solutions |
| Monday,
December 14 |
|
9:00-9:50
|
Tom Hales, University
of Pittsburgh
The formal proof of the Kepler Conjecture |
|
9:55-10:45
|
James Davenport,
University of Bath (SLIDES)
Cylindrical Algebraic Decomposition with logical
structure |
|
10:45-11:10
|
Coffee Break |
|
11:10-12:00
|
Francis Sergeraert,
l'Institut Fourier (SLIDES)
Functional Programming and Complexity |
|
12:00-13:45
|
Lunch |
|
13:45-14:35
|
Doron Zeilberger,
Rutgers University
The Babylonian vs. the Greek Approaches to
Computer Proofs |
|
14:40-15:30
|
Bruno Buchberger,
Johannes Kepler University Linz
Meta-mathics |
|
15:30-15:55
|
Coffee Break |
|
15:55-16:45
|
Georges Gonthier,
Microsoft Research
Hidden gems of formal combinatorial proofs |
| Tuesday,
December 15 |
|
9:00-9:50
|
Henri Lombardi,
Université de Franche-Comté
Geometric theories for constructive algebra
|
|
9:55-10:45
|
Carsten Schneider,
Johannes Kepler University Linz (SLIDES)
Symbolic summation for particle physics: difference
ring theory, stable software and proof certificates |
|
10:45-11:10
|
Coffee Break |
|
11:10-12:00
|
Assia Mahboubi,
INRIA
An exercise in formal proofs for bijective
combinatorics |
|
12:00-13:45
|
Lunch |
|
13:45-14:35
|
Christoph Koutschan,
Österreichische Akademie der Wissenschaften (SLIDES)
Symbolic Determinant Evaluation |
|
14:40-15:30
|
Nicolas Brisebarre,
CNRS, LIP, ENS Lyon (SLIDES)
Table Maker's Dilemma for Transcendental
Functions |
|
15:30-15:55
|
Coffee Break |
|
15:55-16:45
|
Wolfgang Windsteiger,
Johannes Kepler University Linz
Theorema 2.0: A Brief Introduction and a
Case Study in Auction Theory |
| Wednesday,
December 16 |
|
9:00-9:50
|
Jesús Aransay,
Universidad de La Rioja (SLIDES)
Rendering useful formalized mathematics |
|
9:55-10:45
|
Yves Bertot, INRIA
Formalized mathematics: proofs of transcendence,
especially pi |
|
10:45-11:10
|
Coffee Break |
|
11:10-12:00
|
Jacques Carette,
McMaster University (SLIDES)
Leveraging the structure of theory libraries
|
|
12:00-13:45
|
Lunch |
|
13:45-14:35
|
Cyril Cohen, INRIA
A Coq formalization of a sign determination algorithm
in real algebraic geometry |
|
14:40-15:30
|
William Farmer,
McMaster University (SLIDES)
A Comparison of Approaches for Incorporating
Syntax-Based Mathematical Algorithms into Proof Assistants |
|
15:30-15:55
|
Coffee Break |
Registrants
as of October 22, 2015
|
Full Name
|
Institution
|
Arrival Date
|
Departure Date
|
Second Arrival Date
|
Second Departure Date
|
| Alonso, Mariemi |
Complutense University |
06-Dec-15 |
16-Dec-15 |
|
|
| Aransay Azofra, Jesús María |
Universidad de La Rioja |
05-Dec-15 |
18-Dec-15 |
|
|
| Arnold, Andrew |
University of Waterloo |
01-Sep-15 |
31-Dec-15 |
|
|
| Barhoumi, Sami |
Faculty of sciences of Yanbu |
06-Dec-15 |
17-Dec-15 |
|
|
| Basu, Saugata |
Purdue University |
06-Dec-15 |
12-Dec-15 |
|
|
| Bertot, Yves |
Inria |
06-Dec-15 |
17-Dec-15 |
|
|
| Blekherman, Grigoriy |
Georgia Tech |
06-Dec-15 |
12-Dec-15 |
|
|
| Brisebarre, Nicolas |
CNRS, LIP, ENS Lyon |
06-Dec-15 |
17-Dec-15 |
|
|
| Buchberger, Bruno |
Johannes Kepler University Linz |
|
|
|
|
| Carette, Jacques |
McMaster University |
06-Dec-15 |
16-Dec-15 |
|
|
| Chen, Shaoshi |
University of Waterloo |
02-Oct-15 |
18-Dec-15 |
|
|
| Cohen, Cyril |
Inria |
07-Dec-15 |
20-Dec-15 |
|
|
| Coste, Michel |
Universite Rennes 1 |
01-Dec-15 |
18-Dec-15 |
|
|
| D'Andrea, Carlos |
Universitat de Barcelona |
06-Dec-15 |
16-Dec-15 |
|
|
| Davenport, James |
University of Bath |
07-Dec-15 |
16-Dec-15 |
|
|
| Diatta, Seny |
University Assane Seck of Ziguinchor |
10-Sep-15 |
18-Dec-15 |
|
|
| Emiris, Ioannis |
University of Athens |
27-Oct-15 |
31-Oct-15 |
07-Dec-15 |
11-Dec-15 |
| Farmer, William |
McMaster University |
13-Dec-15 |
15-Dec-15 |
|
|
| Faugere, Jean-Charles |
INRIA |
06-Dec-15 |
16-Dec-15 |
|
|
| FRANCIS, MARIA |
Indian Institute of Science |
06-Dec-15 |
16-Dec-15 |
|
|
| Goktas, Unal |
Turgut Ozal University |
13-Sep-15 |
20-Sep-15 |
06-Dec-15 |
16-Dec-15 |
| Gonthier, Georges |
Microsoft Research |
06-Dec-15 |
17-Dec-15 |
|
|
| Guo, Feng |
Dalian University of Technology |
07-Sep-15 |
31-Dec-15 |
|
|
| Hales, Thomas |
University of Pittsburgh |
13-Dec-15 |
15-Dec-15 |
|
|
| Hao, Zhiwei |
Academy of Mathematics & System Sciences, Chinese Academy
of Sciences |
15-Sep-15 |
27-Dec-15 |
|
|
| Hauenstein, Jonathan |
University of Notre Dame |
06-Dec-15 |
11-Dec-15 |
|
|
| Helmer, Martin |
U.C. Berkeley |
06-Dec-15 |
17-Dec-15 |
|
|
| Hessami Pilehrood, Khodabakhsh |
Fields Institute |
14-Sep-15 |
17-Dec-15 |
|
|
| Hessami Pilehrood, Tatiana |
Fields Institute |
14-Sep-15 |
17-Dec-15 |
|
|
| Hubert, Evelyne |
INRIA Méditerranée |
01-Sep-15 |
17-Dec-15 |
|
|
| Hugounenq, Cyril |
Université de Versailles Saint-Quentin-en-Yvelines |
06-Dec-15 |
16-Dec-15 |
|
|
| Ivan, Daniel |
University of Waterloo |
14-Sep-15 |
20-Sep-15 |
26-Oct-15 |
31-Oct-15 |
| Jaroschek, Maximilian |
Max-Planck-Institute for Informatics |
04-Dec-15 |
20-Dec-15 |
|
|
| Jeronimo, Gabriela |
Universidad de Buenos Aires |
06-Dec-15 |
17-Dec-15 |
|
|
| KARTOUE MADY, DEMDAH |
University of N'Djamena |
04-Dec-15 |
18-Dec-15 |
|
|
| Kolpakov, Alexander |
University of Toronto |
07-Dec-15 |
16-Dec-15 |
|
|
| Koutschan, Christoph |
OEAW |
06-Dec-15 |
16-Dec-15 |
|
|
| Krone, Robert |
Queen's University |
25-Oct-15 |
01-Nov-15 |
06-Dec-15 |
17-Dec-15 |
| Labahn, George |
University of Waterloo |
01-Sep-15 |
18-Dec-15 |
|
|
| Li, Nan |
Tianjin University |
|
|
|
|
| Lombardi, Henri |
Université de Franche-Comté |
09-Dec-15 |
19-Dec-15 |
|
|
| Maddah, Sumayya Suzy |
XLIM |
|
|
|
|
| Magron, Victor |
Imperial College |
|
|
|
|
| Mahboubi, Assia |
Inria |
|
|
|
|
| Margulies, Susan |
United States Naval Academy |
06-Dec-15 |
16-Dec-15 |
|
|
| Melczer, Stephen |
University of Waterloo & ENS Lyon |
06-Dec-15 |
20-Dec-15 |
|
|
| Moreno Maza, Marc |
The University of Western Ontario |
|
|
|
|
| Naldi, Simone |
CNRS |
01-Oct-15 |
23-Dec-15 |
|
|
| Neiger, Vincent |
LIP - ENS de Lyon |
13-Sep-15 |
20-Sep-15 |
25-Oct-15 |
31-Oct-15 |
| Niemerg, Matthew |
|
13-Aug-15 |
21-Aug-15 |
29-Aug-15 |
31-Dec-15 |
| Paule, Peter |
Johannes Kepler University |
10-Sep-15 |
20-Sep-15 |
11-Dec-15 |
17-Dec-15 |
| Pillwein, Veronika |
JKU Linz |
09-Dec-15 |
16-Dec-15 |
|
|
| Rideau, Laurence |
INRIA |
13-Dec-15 |
16-Dec-15 |
|
|
| Riener, Cordian |
Aalto University |
05-Sep-15 |
20-Dec-15 |
|
|
| Rodriguez, Jose |
University of Chicago |
06-Dec-15 |
13-Dec-15 |
|
|
| Roy, Marie-Francoise |
Université de Rennes 1 |
26-Oct-15 |
31-Oct-15 |
07-Dec-15 |
16-Dec-15 |
| Safey El Din, Mohab |
Univ. Pierre & Marie Curie |
24-Oct-15 |
31-Oct-15 |
07-Dec-15 |
16-Dec-15 |
| Sagraloff, Michael |
Max Planck Institute for Informatics |
25-Oct-15 |
01-Nov-15 |
06-Dec-15 |
17-Dec-15 |
| Schneider, Carsten |
Johannes Kepler University Linz |
12-Dec-15 |
16-Dec-15 |
|
|
| Schost, Eric |
University of Waterloo |
06-Dec-15 |
16-Dec-15 |
|
|
| Sergeraert, Francis |
Institut Fourier |
05-Dec-15 |
17-Dec-15 |
|
|
| Sottile, Frank |
Texas A&M University |
06-Dec-15 |
13-Dec-15 |
|
|
| Spaenlehauer, Pierre-Jean |
Inria |
06-Dec-15 |
12-Dec-15 |
|
|
| Tsigaridas, Elias |
INRIA Paris |
06-Dec-15 |
17-Dec-15 |
|
|
| Vinzant, Cynthia |
North Carolina State |
|
|
|
|
| Wang, Chu |
Chinese Academy of Sciences |
15-Sep-15 |
27-Sep-15 |
|
|
| Windsteiger, Wolfgang |
Johannes Kepler University |
12-Dec-15 |
16-Dec-15 |
|
|
| Yang, Zhihong |
Academy of Mathematics and System Sciences, Chinese
Academy of Sciences |
15-Sep-15 |
27-Dec-15 |
|
|
| Zeilberger, Doron |
Rutgers University |
15-Sep-15 |
19-Sep-15 |
12-Dec-15 |
16-Dec-15 |
| Zhi, Lihong |
Chinese Academy of Sciences |
16-Sep-15 |
22-Dec-15 |
|
|
Abstracts
Part I Algebraic Algorithms for Polynomials
Monday
Frank Sottile, Texas A&M University
Numerical Schubert Calculus
The Schubert calculus is a well-understood and fundamental class of geometric
problems that are formulated as intersections of Schubert varieties on a Grassmannian.
The importance of these problems lies in their use as a testing ground for
new ideas and that they are universal for certain classes of problems expressed
as degeneracy loci of maps between bundles. While highly structured, they
are far from being complete intersections and standard numerical methods do
not perform well when solving Schubert problems.
Numerical Schubert calculus consists of algorithms tailored to the geometry
of these Schubert problems, including specialized homotopy algorithms, reformulation
as square systems of equations, and notions of witness sets and regeneration.
This talk will survey the developments just sketched that comprise this numerical
Schubert calculus.
Martin Helmer, University of California, Berkeley
Algorithms to Compute Characteristic Classes of Subschemes of Certain Toric
Varieties
Topological invariants such as characteristic classes are an important tool
to aid in understanding and categorizing the structure and properties of algebraic
varieties. Besides being of interest for problems in mathematics such invariants
have also been applied to problems from string theory in physics and to problems
of maximum likelihood estimation in statistics.
In this talk we discuss methods to compute several common topological invariant
of some toric varieties. More specifically, let X be a complete smooth toric
variety where all Cartier divisors in Pic(X) are nef and let V be a subscheme
of X. We give a new expression for the Segre class of the subscheme V, s(V,X),
in terms of the projective degrees of a rational map associated to V. Additionally
we give a concrete and computable expression for these projective degrees.
Combining these results we develop effective algorithms for the computation
of the Chern-Schwartz-MacPherson class, Segre class and the Euler characteristic
of V. In the case of smooth subschemes V this will also allow us to compute
the total Chern class of V. The algorithms will, in particular, be applicable
to any subscheme of a product of projective spaces.
The algorithms may be implemented symbolically using Groebner basis or numerically
using homotopy continuation via a package such as Bertini or PHCPack. The
algorithms have been implemented in Macaulay2 and an M2 package is available.
Our algorithms perform favourably on a wide selection of examples in comparison
to other known algorithms. Theoretical running time bounds for several of
the algorithms are also given.
Robert Krone, Queen's University
Equivariant Gröbner bases
Given a polynomial ring with an action of the infinite symmetric group on
its set of variables, an equivariant Gröbner basis of an ideal is a set
of polynomials whose orbits under the action form a Gröbner basis. Equivariant
Gröbner bases offer a concise way to describe ideals in high dimension
with symmetry and (under some conditions) can be effectively computed. Buchberger's
algorithm can be adapted straight-forwardly to the equivariant setting, but
only in some cases can termination be guaranteed. We present a way to repair
this in the case that a finite Gröbner basis exists. We prove that certain
toric ideals have finite equivariant Gröbner bases for certain monomial
orders and that we can use the above algorithm to compute them. Additionally
we look to adapt more efficient Gröbner basis algorithms such as signature-based
algorithms to the equivariant setting. This includes work with Jan Draisma,
Rob Eggermont, Chris Hillar and Anton Leykin.
Jose Rodriguez, University of Chicago
Numerically computing Galois groups
Galois groups are an important part of number theory and algebraic geometry.
To a parameterized system of polynomial equations one can associate a Galois
group whenever the system has k (finitely many) nonsingular solutions generically.
The Galois group of a parameterized system is a subgroup of the symmetric
group on k elements. Using monodromy loops, it has been shown how to certifiably
compute the Galois group when it is the full symmetric group. In this talk,
we are interested in Galois groups that are not of maximal cardinality. We
explore both a branch point and a fiber product approach using numerical algebraic
geometry to compute the generators of the Galois group and determine its transitivity.
An implementation using Bertini.m2 will also be discussed. (joint work with
Jon Hauenstein and Frank Sottile)
Carlos d'Andrea, Universitat de Barcelona
Sparse Eliminants vs Sparse Resultants
Sparse resultants are widely used in polynomial equation solving, a fact that
has sparked a lot of interest in their computational and applied aspects.
They have also been studied from a more theoretical point of view because
of their connections with combinatorics, toric geometry, residue theory, and
hypergeometric functions.
Sparse elimination theory focuses on ideals and varieties defined by Laurent
polynomials with given supports, in the sense that the exponents in their
monomial expansion are a priori determined. The classical approach to this
theory consists in regarding such Laurent polynomials as global sections of
line bundles on a suitable projective toric variety. Using this interpretation,
sparse elimination theory can be reduced to projective elimination theory.
In particular, sparse resultants can be studied via the Chow form of this
projective toric variety as it was done classically.
This approach works correctly when all considered line bundles are very ample,
but need to be properly defined in general. In this talk, we will report on
recent progress made in collaboration with Gabriela Jeronimo and Martin Sombra
on elimination theory from both an algebraic and geometric point of view,
which allow us to understand, extend and simplify some classical formulations
for sparse resultants in a more general context.
________________________________________________________________________________________
Tuesday, December 8
Pierre-Jean Spaenlehauer, INRIA
Sparse polynomial systems with many positive solutions from bipartite simplicial
complexes
We consider the problem of constructing multivariate polynomial systems with
prescribed monomial support and having many non-degenerate positive solutions.
We use a version of Viro's method to identify families of monomial supports
admitting polynomial systems all complex solutions of which are real and positive.
This provides some evidence in favor of a conjecture by Bihan which describes
a necessary condition on such supports. Finally, this construction is applied
to a family of fewnomial systems by considering a simplicial complex contained
in a regular triangulation of the cyclic polytope. We describe relations with
computational problems such as a positive variant of matrix completion and
the problem of deciding the realizability of oriented matroids. (joint work
with Frédéric Bihan)
Eric Schost, University of Waterloo
Using linearly recursive sequences to solve polynomial systems
Wiedemann's algorithm is a cornerstone of sparse linear algebra: roughly speaking,
it allows one to compute the minimal polynomial of a matrix by computing the
minimal polynomial of a linearly recursive sequence.
This principle has been used as well in the context of polynomial system solving
to answer the following kind of question: given a Groebner basis of a zero-dimensional
ideal, say for a degree order, compute a description of the solutions as in
the Shape Lemma. Algorithms by Becker and Wormann, Alonso et al., and Rouillier,
use trace computations in order to compute a description by means of univariate
polynomials. More recently, Bostan et al. and Faugère and Mou have
used computations with random linear forms in order to obtain similar results.
I will give an overview of these ideas, and present ongoing work with Jeannerod,
Neiger and Villard that aims at using these techniques to compute the local
structure at the solutions of the system.
Jean-Charles Faugere, INRIA
Sparse-FGLM and Linear Recursive Multidimensional Sequences
Given a zero-dimensional ideal I ? K[x1, . . . , xn] of degree D, the transformation
of the ordering of its Gröbner basis from DRL to LEX is a key step in
polynomial system solving and turns out to be the bottleneck of the whole
solving process. Thus it is of crucial importance to design efficient algorithms
to perform the change of ordering. With Chenqi we have proposed several efficient
algorithms for the change of ordering which take advantage of the sparsity
of multiplication matrices in the classical FGLM algorithm.
For the general case, the designed method is characterized by the Berlekamp–Massey–Sakata
algorithm from Coding Theory to handle the multidimensional linearly recurring
relations. Sakata extended the Berlekamp~-- Massey algorithm from 1 dimension
to n dimensions.
We design several algorithms for computing a Gr\"obner basis of the
ideal of relations. A FGLM-like algorithm allows us to compute the relations
of the table by extracting a full rank submatrix of a multi-Hankel matrix
(a multivariate generalization of Hankel matrices). Under some additional
assumptions, we make this algorithm adaptive and reduce further the number
of table probes.
The number of probes of Scalar-FGLM can be estimated by counting precisely
the number of distinct elements in a multi-Hankel matrix; we can relate this
quantity with the geometry of the final staircase. Hence, in favorable cases
such as convex ones, the complexity is essentially linear in the size of the
output.
As a by-product, we have a fast implementation that is able to handle ideals
of degree over 300000.
Marc Moreno Maza, The University of Western Ontario
Limit Points of Constructible Sets
Given a regular chain, we are interested in computing the (non-trivial) limit
points of its quasi-component in the Zariski topology, or equivalently, computing
the variety of its saturated ideal. The generalization of this problem from
regular chains to constructible sets is natural.
We propose techniques which avoid the computation of Groebner bases. A first
approach relies on linear changes of coordinates; such changes can be either
generic or guided by the input. When the polynomial coefficients are real
or complex, a second approach borrows tools from functional analysis, like
Puiseux series.
Applications of the proposed techniques include computations of tangent cones
(free of standard bases) and limits of multivariate algebraic functions. This
talk is based on a series of papers and new results co-authored with Parisa
Alvandi, Changbo Chen and Amir Hashemi.
Mari Emi Alonso, Complutense University
Abstract local Bezout theorems and other constructive aspects of Henselian
rings
Henselian rings are limits of Henselian systems, which allow us to make dynamical
computations. In this talk we survey some constructions in this class of rings,
in particular an abstract local Bezout theorem. As a technical tool, Border
Bases and multivariate Hensel lemma translate the problem of isolating multiple
zeroes of a system of equations into the problem of lifting residually simple
zeroes. This is a joint work with H. Lombardi.
________________________________________________________________________________________
Part II Computations in Real Algebraic
Geometry
Wednesday, December 9
Fabrice Rouillier, INRIA Paris
Computing intersections of two algebraic plane curves : the price of the certification
Computing the intersection of algebraic plane curves is a central problem
: topology and certified drawing of plane curves, solving polynomial systems
depending on two parameters, etc. I will present some recent algorithms for
solving systems of two bivariate polynomials by means of rational parameterizations.
These algorithms and their complexity essentially differ by the way the certification
of the algorithm is ensured (Deterministic, Las Vegas or Monte-Carlo algorithms),
by the assumptions made on the input (radical ideal, generic position, possible
asymptotes, etc..), the price for checking them … when possible and also
by their behavior in practice. For each of these algorithms, I will give complexity
results (size end computation time) as well as quantitative informations on
the practical behavior (class of problems to be solved).
Elias Tsigaridas, INRIA Paris
Separation bounds for polynomial systems
Separation bounds are bounds on the minimum distance between two different
isolated roots of a polynomial system. Zero bounds, that is estimations on
the distance of a root from zero, are special cases of separation bounds.
They appear in various disciplines, like real algebraic geometry, computational
topology and geometry, game theory, polynomial and combinatorial optimization,
quantifier elimination, algebraic number theory.
We present a priori worst case separation bounds for the isolated roots of
zero-dimensional, as well as positive-dimensional and overdetermined polynomial
systems. We also present polynomial systems whose root separation is asymptotically
not far from our bounds.
Almost always, we estimate separation bounds without solving the corresponding
polynomial system. A natural question to ask is, if we allow ourselves to
perform some operations, say quasi-linear in the size of the input, can we
obtain better bounds? We present recent progress in this direction. (joint
work with Ioannis Emiris, Aaron Herman, Hoon Hong, and Bernard Mourrain).
Guillaume Moroz, INRIA Nancy-Grand Est
On the computation of the silhouette of an analytic surface
A classical problem in real algebraic and computational geometry is the description
of a surface's silhouette. The silhouette of a regular surface S is formally
defined as the critical values of a projection map from S to the plane. The
silhouette is generally a curve in the plane, which is not necessarily regular.
Many algorithms were designed over the last decades to compute efficiently
the description of the silhouette of an algebraic surface. On the other hand,
no state-of-the-art algorithm can handle the case of analytic surfaces. An
analytic variety is defined as the zeroes of a set of real analytic functions.
Under some assumptions, we will present in this talk a first algorithm to
compute the silhouette of a regular analytic surface. This is a common work
with Marc Pouget and Rémi Imbach.
Mehdi Ghasemi, University of Saskatchewan
Application of geometric programming in polynomial optimization
We deal with the general problem of computing a lower bound for a multivariate
polynomial on a basic closed semi-algebraic. We show that there is an algorithm
for computing such a lower bound, based on geometric programming, which
applies in a large number of cases. The bound obtained is typically not
as good as the bound obtained using semidefinite programming, but it
has the advantage that it is computable rapidly, even in cases where
the optimizers based on semidefinite programming fail to provide a result.
Michel Coste, Université de Rennes 1
Geometry and Symbolic Computation for Analyzing the Singularities of Parallel
Robots
I shall present some problems in robot kinematics and review some tools from
geometry and from symbolic computations which are used to address these problems.
I shall mainly focus on the study of the singularities of parallel robots :
avoiding singular configurations is an important issue for these robots. A
famous example of parallel robots is the Gough-Stewart platform, and I plan
to discuss the existence of a rational parametrization of the singularities
of a Gough-Stewart platform. This problem is related to the classical study
of cubic surfaces.
Mohab Safey El Din, University Pierre et Marie
Curie
On nearly optimal algorithms for computing roadmaps
Roadmaps have been introduced by Canny as a tool for deciding connectivity
queries in semi-algebraic sets: these are curves which have a non-empty and
connected intersection with the semi-algebraic set under consideration.
This talk will review recent progress in the computation of roadmaps in the
case of algebraic sets. These have led to nearly optimal algorithms; we will
focus on those dealing with real algebraic sets under some regularity assumptions.
These algorithms are subquadratic in the output size which is essentially
quadratic in (nD) to the power n.log(n), where n is the dimension of
the ambient space and D bounds the degree of the input polynomials.
(Joint work with E. Schost)
Marie-Francoise Roy, Université de Rennes 1
Quantifier elimination for real closed fields : a purely algebraic variant
of CAD
We design a purely algebraic variant of CAD which is not using the notion
of semi-algebraic connectedness. This was already the case of Tarski's original
proof of quantifier elimination but its complexity was primitive recursive.
The method is based on Thom encodings and sign determination, as well as subresultants.
One of our motivations is to have a quantifier elimination with elementary
recursive complexity proved in a proof assistant (e.g. Coq). The eliminating
family we define plays a key role in our recent elementary recursive degree
bounds for Hilbert 17 th problem and the Positivstellensatz. (joint work with
Daniel Perrucci)
________________________________________________________________________________________
Thursday, December 10
Greg Blekherman, Georgia Institute of Technology
Degree bounds in sums of squares representations
I will discuss degree bounds for rational sums of squares representations
of nonnegative polynomials on curves and surfaces focusing on the interplay
between geometry of the variety and existence of good bounds.
________________________________________________________________________________________
Friday, December 11
Michael Sagraloff, Max Planck Institute for
Informatics
On the Complexity of Solving Polynomial Systems via Projection
Given a zero-dimensional polynomial system in d variables, a common approach
for computing the solutions of this system is to first project the solutions
into one dimension (e.g. using resultant or Groebner Basis computation)
in the first step and to recover the solutions from the projections in the
second step. If the projection direction is known to be separating for the
solutions, one possible solution for the recovering step is the computation
of a rational univariate representation (RUR).
However, despite the fact that a separating direction can be chosen at random
with high probability, it is difficult to verify that a given direction is
separating. In fact, this turns out to be a critical step with respect to
the worst-case complexity of a deterministic approach. In this talk, we propose
a simple deterministic and certified algorithm for solving zero-dimensional
polynomial systems, which only needs to compute projections of the solutions
but no further algebraic manipulations. It computes a separating direction
as well as isolating boxes for all solutions for the cost of d+1 projections
of the solutions. It is worthwhile to remark that, for d=2, the worst case
bit complexity of our method matches the current record bound as achieved
by much more involved algorithms.
Gabriela Jeronimo, Universidad de Buenos Aires
A zero counting symbolic procedure for a class of univariate Pfaffian functions
We will present a symbolic procedure to count the exact number of zeros in
a real interval of univariate Pfaffian functions of order 1. The procedure
is based on the construction of a family of Sturm sequences associated to
the given function, which is done by means of polynomial subresultant techniques,
and relies on an oracle for sign determination. In the particular case of
exponential polynomials, we will show an effective symbolic algorithm solving
the problem with no calls to oracles, and we will present an explicit upper
bound on the absolute value of the real roots. (joint work with María
Laura Barbagallo and Juan Sabia (Universidad de Buenos Aires, Argentina))
Rainer Sinn, Georgia Institute of Technology
Sums of squares on projective varieties
The object of interest in this talk will be nonnegative quadratics in the
graded coordinate ring of an embedded projective variety. Blekherman, Smith,
and Velasco showed that all of them are sums of squares of linear forms if
and only if the variety is of minimal degree. We will extend this result to
reducible varieties and discuss connections to spectrahedral questions arising
in algebraic statistics.
Saugata Basu, Purdue University
Complexity of constructible sheaves
Constructible sheaves play an important role in several areas of mathematics,
most notably in the theory of D-modules. It was proved by Kashiwara and Schapira
that the category of constructible sheaves is closed under the standard six
operations of Grothendieck. This result can be viewed as a far reaching generalization
of the Tarski-Seidenberg principle in real algebraic geometry. In this talk
I will describe some quantitative/effectivity results related to the Kashiwara-Schapira
theorem -- mirroring similar results for ordinary semi-algebraic sets which
are now well known. For this purpose, I will introduce a measure of complexity
of constructible sheaves, and bound the complexity of some of the standard
sheaf operations in terms of this measure of complexity. I will also discuss
quantitative bounds on the dimensions of cohomology groups of constructible
sheaves in terms of their complexity, again extending similar results on bounding
the the ordinary Betti numbers of semi-algebraic sets.
Cynthia Vinzant, North Carolina State University
Numerical methods for computing real and complex tropical curves
Tropical varieties capture combinatorial information about how coordinates
in a classical varieties approach zero or infinity. I will introduce
the notion of tropical varieties over the real and complex numbers and describe
a numerical algorithm for computing the rays of a tropical curve. These algorithms
rely on homotopy continuation, monodromy loops, and Cauchy integrals and are
implemented in the numerical algebraic geometry software Bertini. (joint work
with Daniel Brake and Jon Hauenstein)
Cordian Riener, Aalto University
Topological complexity of symmetric semi-algebraic sets
This talk will present results on the structure of cohomology modules of symmetric
(as well as multi-symmetric) real varieties and semi-algebraic sets. More
precisely, we will show bounds on the number of irreducible representations
of the symmetric group occurring in the isotypic decomposition of the
cohomology modules of the sets in question, which are polynomial in
the number of variables, as well as polynomial bounds on the corresponding
multiplicities. As an application we will give some improvements on bounds
for the Betti numbers of images under projections of (not necessarily symmetric)
bounded real algebraic sets. (based on joint works with Saugata Basu)
________________________________________________________________________________________
Saturday, December 12
Lihong Zhi, Chinese Academy of Sciences
A certificate for semidefinite relaxations in computing positive-dimensional
real radical ideals
For an ideal with a positive-dimensional real variety,
based on moment relaxations, we study how to compute a Pommaret
basis of an ideal generated by the kernel of a truncated moment
matrix and included in the real radical ideal. We provide a certificate
consisting of a condition on coranks of moment matrices for terminating the
algorithm. For a generic Delta-regular coordinate system, we prove that
the condition can be satisfied in a large enough order
of moment relaxations. (joint work with Yue Ma and Chu Wang)
Michael Burr, Clemson University
Continuous Amortization: Intrinsic Geometric Complexity for Subdivision-based
Algorithms
Continuous amortization was recently introduced as a technique to compute
the complexity of subdivision-based algorithms. This technique has been
successfully applied uniformly to algorithms in symbolic computation for isolating
solutions of polynomials. Continuous amortization can be used to compute many
complexity-based quantities of subdivision-based algorithms, such as the number
of subdivisions, the bit complexity, or the expected time. Moreover,
the complexity resulting from continuous amortization is based on the intrinsic
geometric complexity of the input instance. In practice, continuous
amortization can be applied uniformly to a variety of algorithms and provides
state-of-the-art results which are adaptive to the input data. In this
talk, I will provide an introduction to the continuous amortization technique
and illustrate the details for its application to several subdivision-based
algorithms for isolating the solutions of polynomials.
Jonathan Hauenstein, University of Notre
Dame
Local decomposition and local methods for analyzing real solutions
Real solutions to systems of polynomial equations are often the solutions
of interest in applications. This talk will describe using computational
algebraic geometry to study the real solution set of two systems. In
kinematics, a real solution is often given and the task is to determine the
local motion characteristics. Computing the local irreducible components
through the given solution provides insight into to the local behavior of
the solution set. This local decomposition will be used to show that
the "home" position of a cubic-centered 12-bar mechanism is rigid
(i.e., isolated over the real numbers), but is a point on a complex curve.
In chemistry, local methods are often used to locate local minimal energy
states. By combining numerical algebraic geometry and convex algebraic
geometry, we will describe a test for showing that all real solutions, including
positive-dimensional components, have been identified. This approach
will be applied to the analysis of energy landscapes arising from nearest-neighbor
interactions.
________________________________________________________________________________________
Part III Certified Algorithms, Computer Algebra and Proofs
Monday, December 14
Tom Hales, University of Pittsburgh
The formal proof of the Kepler Conjecture
The Kepler conjecture asserts that no packing of congruent balls in space
can have density greater than the familiar cannonball arrangement, called
the face-centered cubic packing.
In 1998, Sam Ferguson and I announced a proof of the conjecture, which was
published several years later.
In the meantime, I started a long-term project to give a formal proof of the
theorem. A proof is formally verified if every step of the proof has been
checked, at the level of the primitive inference rules of logic and the foundational
axioms of mathematics. In a collaborative effort, the Kepler conjecture has
now been formally verified. This is one of the largest formal proof projects
ever completed.
James Davenport, University of Bath
Cylindrical Algebraic Decomposition with logical structure
The original Collins CAD, and early improvements (McCallum etc.), applied
to a formula F, took as input the set of polynomials appearing in F, ignoring
the logical structure of F. Collins noted, and McCallum implemented, that
we could do better if F were of the form p=0 and G (an equational constraint).
This has been extended to two equational constraints.
In this talk we look at (DNF) formulae where the clauses contain different
equational constraints, and indeed where some may not contain equational constraints.
We show a smooth transition of complexity from no equational constraints to
every clause having an equational constraint. We also re-consider the question
of multiple equational constraints. (joint work with Bradford, England, McCallum,
Wilson)
Francis Sergeraert, l'Institut Fourier
Functional Programming and Complexity
The algorithms coming from "Effective Homology" require a high level
of Functional Programming. The concrete implementation is conveniently done
thanks to the powerful notion of Lexical Closure. Studying the complexity
of such a program is a little particular and needs a lucid knowledge of the
concrete implementation and dynamic generation of these closures. The talk
explains why the closures are generated essentially without any cost. The
notion of polynomial size for functional objects of arbitrary level is defined.
As a consequence, the computation of a n-th homotopy group can be done polynomially
with respect to the space X. Proving a polynomial complexity with respect
to n is known as difficult as P=NP (David Anick, 1989).
Doron Zeilberger, Rutgers University
The Babylonian vs. the Greek Approaches to Computer Proofs
Euclid, Aristotle, Plato and their friends gave us the wonderful formal logic
and the axiomatic method that dominated Western mathematics for the last 2300
years. Automated Theorem Proving is a wonderful incarnation of this methodology
for the computer age.
However, we should also, in parallel, pursue the more naive, empirical and
practical, Babylonian approach to mathematical knowledge, since being less
"rigorous" (I am tempted to say "pedantic") , has the
potential to go beyond the Greek straitjacket.
Bruno Buchberger, Johannes Kepler University
Linz
Meta-mathics
In this talk I argue that mathematics is evolving more and more into “meta-mathics”,
i.e. mathematics on the object level (traditionally called “mathematics”)
executed in parallel with mathematics on the meta-level (traditionally called
“meta-mathematics”).
We draw conclusions for the future capabilities of comprehensive mathematical
software systems in which, when developing a theory, the system should give
support to the work on the object level and, at the same time, on the meta-level.
We illustrate this observation by some details about various phases of developing
Gröbner bases theory, which essentially meanders through at least three
layers of object / meta.
As another example, we consider the manuscript by A.J. Stam on “Binominal
identities with old-fashioned proofs” from the year 2000 (1300 pages!)
as a benchmark challenge for the capabilities of current mathematical software
systems: The paper contains portions that, today, could be handled by combinatorial
identities algorithms (of the D. Zeilberger, P. Paule, C. Schneider et al.
type) whereas others need traditional proof methods.
We will discuss all this also in the frame of the recent “Global Math
Digital Library” initiative of the International Mathematical Union.
Georges Gonthier, Microsoft Research
Hidden gems of formal combinatorial proofs
Combinatorial proofs are the ugly ducklings of traditional mathematics, so
much so that purely combinatorial proofs, e.g., the 4-color theorem, aren’t
considered “real proofs”. Formal proofs can be even worse, reducing
combinatorial argument to either pages of mindless drivel or miraculous runs
of obscure algorithms. I will however argue that formal proofs can also offer
redemption, because they allow the mathematical description and analysis of
the algorithms used to crunch combinatorial cases, and the in vivo study of
their interplay with classical arguments. In the best cases, this study can
uncover little gems hidden under the combinatorial quagmire – as I’ve
been lucky to observe a few times starting with the 4-color theorem.
________________________________________________________________________________________
Tuesday, December 15
Henri Lombardi, Université de Franche-Comté
Geometric theories for constructive algebra
I discuss the following question: when constructivizing abstract modern algebra,
very often, a good way of doing the job is to find a geometric theory which
has in a classical context the same strength as the piece of mathematics we
aim to understand constructively. Are there exceptions to this observation,
and how can we interpret the divergence that happens between classical and
constructive points of view?
Carsten Schneider, Johannes Kepler University
Linz
Symbolic summation for particle physics: difference ring theory, stable
software and proof certificates
In the last years the difference ring theory for symbolic summation has been
pushed forward extensively to perform challenging calculations within the
field of particle physics. In a long term project with DESY (Deutsches Elektronen-Synchrotron)
the underlying algorithms have been playing a central role to evaluate several
hundred thousands 2-loop and 3-loop massive Feynman integrals.
A central requirement for these large scale calculations is the very stable
and efficient software package Sigma. Its stability relies heavily on a strict
separation between the object representation used in the computer algebra
world and the sequence representation of the analysis world. In particular,
proof certificates are used as an appropriate link between these two worlds
- they can be utilized to design correct and stable summation algorithms.
In this talk we will elaborate by concrete examples these different aspects:
how the advanced difference ring theory is used to attack highly complicated
Feynman integrals and how the concept of proof certificates can be exploited
to gain stable software packages.
Assia Mahboubi, INRIA
An exercise in formal proofs for bijective combinatorics
This talk is devoted to an exercise, posed by Alin Bostan, which consists
in showing that two families of plane lattice n-walks with (small) steps in
{N, SE, W} have the same cardinal. We provide an elementary bijective proof,
which can be seen as a simplified instance of the bijections described in
the literature. We hope to illustrate on this example how functional programming
and formal proofs can help provide reasonably concise and convincing evidences
for this kind of argument.
Christoph Koutschan, Österreichische Akademie
der Wissenschaften
Symbolic Determinant Evaluation
We consider the problem of evaluating (or proving, if known) the determinant
of a matrix whose dimension is a symbolic parameter.
Inspired by the "holonomic ansatz" that was proposed by Zeilberger
a few years ago, we discuss several methods to solve this problem. Depending
on the type of input matrix one can choose which method is best suited.
We demonstrate the wide range of applicability by a selection of "real-world"
examples. A key ingredient in these proofs is our software package HolonomicFunctions.
Nicolas Brisebarre, CNRS, LIP, ENS Lyon
Table Maker's Dilemma for Transcendental Functions
On a computer, real numbers are usually represented by a finite set of numbers
called floating-point numbers. When one performs an operation on these numbers,
such as an evaluation by a function, one returns a floating-point number,
hopefully close to the mathematical result of the operation. Ideally, the
returned result should be the exact rounding of this mathematical value. One
knows how to guarantee such a quality of results for arithmetical operations
like +, -, x, / and square root but, as of today, it is still an issue when
it comes to evaluate an elementary function such as cos, exp, cube root for
instance. This problem, called Table Maker's Dilemma, is actually a diophantine
approximation problem. It was tackled, over the last fifteen years, by V.
Lefèvre, J.M. Muller, D. Stehlé, A. Tisserand and P. Zimmermann
(LIP, ÉNS Lyon and LORIA, Nancy), using tools from algorithmic number
theory. Their work made it possible to partially solve this question but it
remains an open problem. In this talk, I will present an ongoing joint work
with Guillaume Hanrot (ÉNS Lyon, LIP, AriC) that improve on the existing
results.
Wolfgang Windsteiger, Johannes Kepler University
Linz
Theorema 2.0: A Brief Introduction and a Case Study in Auction Theory
Mathematical assistant systems are general purpose systems that should be
able to support the mathematician during all phases of mathematical activities,
regardless of the special domain in which she is working, they are the ``pencil
and paper of the 21st century''.
Automated and interactive theorem proving are traditionally in the focus of
mathematical assistant systems, but also mathematical syntax and notation,
organization and reuse of knowledge, the integration of proving and computation,
or presentation of mathematics are central topics for any mathematical assistant
system.
In this talk, we want to present Theorema 2.0, a mathematical assistant system
invented, developed, and implemented at the RISC institute at JKU Linz. We
discuss the current status of the system and an application in the formalization
of a central theorem in theoretical economics, the Vickrey's Theorem in auction
theory.
________________________________________________________________________________________
Wednesday, December 16
Jesús Aransay, Universidad de La Rioja
Rendering useful formalized mathematics
In this talk we present a project of formalisation of Linear Algebra in Isabelle/HOL
that has led us to obtain verified programs computing canonical and normal
forms of matrices, such as Gauss-Jordan and Hermite normal forms, and decompositions
such as QR. The formalisation of these algorithms is accompanied also by the
formal proofs of their particular applications (e.g., range of linear forms,
solution of systems of linear equations, orthogonal matrices, least squares
approximations of systems of linear equations, determinants over principal
ideal domains). The verified programs are also compared in terms of efficiency
to imperative implementations, yielding remarkable results. The formalisation
has also given place to side-products, such as code refinements for matrices,
an implementation of division structures in Isabelle/HOL or generalisations
of well-established Isabelle libraries.
Yves Bertot, INRIA
Formalized mathematics: proofs of transcendence, especially pi
Proofs of transcendence are interesting to study because they lie at the
interface between algebra and real and complex analysis. A formal verification
of the proof of transcendence for the number e was published in 2011. This
proof was performed using Hol-Light by J. Bingham.
In 2014, we decided to understand what was needed for a proof that pi is transcendental.
The extra ingredient is multivariate polynomials, especially symmetric polynomials
and the theorem known as the fundamental theorem of symmetric polynomials,
which is actually an algorithm.
We completed the development, just achieving the first formalized proof of
transcendence for pi.
In this talk, I will describe this proof of transcendence for pi and the hurdles
encountered when attempting to make a proof that can be mechanically checked
in the context of Coq, Coquelicot (for analysis), and Mathematical Components
(for algebra). My opinion is that this also gives some insights about the
future of formalized mathematics. (joint work with Sophie Bernard, Laurence
Rideau, and Pierre-Yves Strub)
Jacques Carette, McMaster University
Leveraging the structure of theory libraries
While it is well-known that networks of theories have a lot of structure,
very little is actually done with this structure. Our claim is that using
this structure can be an incredible time-saver for the development of large
libraries.
After showing some tools that allow this structure to become much more apparent,
we will show a large set of examples of this structure in mathematics. In
particular, some ``stories'' from the structure in algebra, logic and category
theory will be told. We will then turn to some ongoing work focused on finding
similar structure in computer science. Finally, we will demonstrate how this
work can be leveraged in a code generation setting.
The overall philosophy is, through careful engineering, to extract as much
information from structure as possible, to free mathematicians and computer
scientists from drudgery so as to allow them more time to work on the aspects
which require insight and creativity.
Cyril Cohen, INRIA
A Coq formalization of a sign determination algorithm in real algebraic
geometry
One of the problems in real algebraic geometry is root counting. Given a polynomial,
we want to count the number of roots that satisfies constraints expressed
as polynomial inequalities. A naive way is to compute an exponential number
of time consuming quantities, called Tarski Queries. In this paper, we formalize
a sign determination algorithm from "Algorithms in Real Algebraic Geometry"
(Basu, Pollack, Roy) which allows to compute them in O(s d), where s is the
number of polynomials and d the degree. We formally build a linear system,
and we prove in Coq that the system is of small size. The formal proof that
the solutions of this system are the numbers of roots satisfying the constraints
is unfinished. (joint work with Mathieu Kohli)
William Farmer, McMaster University
A Comparison of Approaches for Incorporating Syntax-Based Mathematical
Algorithms into Proof Assistants
A syntax-based mathematical algorithm (SBMA) is an algorithm that manipulates
the syntax of mathematical expressions in a mathematically meaningful way.
Examples include algorithms for processing polynomials and for differentiating
functional expressions. This presentation addresses the following problem:
How can an implementation of an SBMA in a computer algebra system be incorporated
into a proof assistant? We compare a variety of approaches to solving this
problem according to criteria such as ease of implementation, execution efficiency,
mathematical clarity, trustworthiness, and proof efficiency.
Back to top
