|
|
 |
|
Mardi 17 Novembre
| Heure: |
12:30 - 13:30 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
Identités de Gallai chromatiques opérant sur la fonction Theta Lovasz |
| Description: |
Denis Cornaz Un paramètre de graphe (une fonction qui associe un entier à tout graphe) est dit sandwich si, pour tout graphe, il est compris entre la taille de la clique maximum et le nombre chromatique.
Nous définissons à l'aide d'un graphe auxiliaire (un sous-graphe partiel du line-graphe) un opérateur PHI qui transforme tout paramètre sandwich en un autre paramètre sandwich.
Nous montrons que PHI améliore la qualité des bornes polynomiales pour la coloration (bornes obtenues par la programmation semie-définie), de plus, expérimentalement, l'amélioration est significative. Par ailleurs, PHI détériore la qualité de la borne obtenue par la programmation linéaire. |
| Heure: |
14:00 - 17:00 |
| Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
| Résumé: |
A computer-algebra-based formal proof of the irrationality of ?(3) |
| Description: |
Frédéric Chyzak We report on the formal verification of an irrationality proof of theevaluation at 3 of the Riemann zeta function. This verification usesthe Coq proof assistant in conjunction with algorithmic calculationsin Maple. This irrationality result was first proved by Apéry in1978, and our formalization follows the proof path of his originalpresentation. The crux of it is to establish that some sequencessatisfy a common recurrence. We formally prove this by an aposteriori verification of calculations performed by a Maplesession. This bases on computer-algebra algorithms implementingZeilberger's approach of creative telescoping. This experienceillustrates the limits of the belief that creative telescoping candiscover recurrences for holonomic sequences that are easily checked aposteriori. We discuss this observation and describe the protocol wedevised in order to produce complete formal proofs of the recurrences.Beside establishing the recurrences, our proof combines theformalization of arithmetical ingredients and of some asymptoticanalysis.Joint work with Assia Mahboubi, Thomas Sibut-Pinote, and Enrico Tassi. |
|
|
