Séminaires de l'année


Lien ical.

Boris Kolev, Université de Provence. 2:00:00 2 février 2012 15:30 labo
Un principe universel de la mécanique d'après Jean-Marie Souriau
Abstract

« div(T) = 0, c'est la mécanique ! » . À partir de cette expression attribuée à Einstein, Jean-Marie Souriau a formulé une équation universelle de la mécanique, dont dérive la plupart des modèles de la mécanique des milieux continus. Cet exposé propose de présenter cette formulation géométrique, élégante et encore mal connue.

Afaf Bouharguane, LJK, Uuniversité Joseph Fourier. 2:00:00 2 février 2012 14:00 edp
Analyse et simulation numérique de modèles non-locaux en morphodynamique littorale
Abstract

Au cours de cet exposé, j'introduirai deux approches qui aboutissent à la résolution de modèles non-locaux pour l'analyse de la dynamique sédimentaire. La première portera sur l'équation d' A.-C. Fowler qui correspond à l'équation de Burgers visqueuse modifiée par un terme non-local qui peut être identifié à un Laplacien fractionnaire anti-diffusif. Dans la seconde approche, nous utilisons les principes de minimisation pour décrire l'évolution d'un lit érodable sous l'action de l'eau. Il sera intéressant de constater que cette seconde méthode peut être liée à la première.

Zakaria Belhachmi, Université de Mulhouse. 2:00:00 27 janvier 2012 15:15 edp
Débruitage et régularisation par variation totale : modèles de décomposition en vision par ordinateur.
Abstract

Dans cette exposé, nous proposons une nouvelle formulation des problèmes d'estimation de flot optique et de stéréo-vision qui repose sur une analogie avec les problèmes de débruitage. Le caractère mal posé de ces problème nous conduit à la régularisation par variation totale que nous controllons grâce a des modèles de décomposition.

Ilia Itenberg, Jussieu. 2:00:00 27 janvier 2012 10:15 geo
Homologie tropicale
Abstract

L'exposé est consacré aux groupes d'homologie dans le cadre tropical. Sous certaines conditions, une variété tropicale peut être approximée par une famille à un paramètre de variétés complexes, et des caractéristiques importantes des variétés de cette famille peuvent être exprimées en termes des groupes d'homologie tropicaux de la variété tropicale considérée. (Travail en commun avec L. Katzarkov, G. Mikhalkin et I. Zharkov.)

Filippo Gazzola, Politecnico di Milano. 2:00:00 20 janvier 2012 14:00 edp
Tamara Servi, Univ. Lisbonne. 2:00:00 20 janvier 2012 10:15 geo
Théorème de rectilinéarisation pour algèbres quasi-analytiques
Abstract

Un résultat central de géométrie analytique réelle est le théorème de rectilinéarisation d'Hironaka, qui affirme que tout ensemble sous-analytique borné peut être décrit par un nombre fini d'égalités et inégalités satisfaites par des compositions de fonctions analytiques et de la fonction 1/x. Nous étendons cet énoncé à des algèbres quasi-analytiques, en donnant des exemples d'applications. Nous expliquons en particulier comment des arguments de théorie des modèles permettent de se passer du traditionnel théorème de préparation de Weierstrass, qui fait défaut dans les classes quasi-analytiques. (travail en commun avec J.-P. Rolin).

Gilles Lebeau, Laboratoire Dieudonné de Nice. 2:00:00 19 janvier 2012 14:00 labo
Algorithme de Metropolis
Abstract

L'algorithme de Metropolis est un algorithme permettant de tirer un point au hasard pour une probabilité donnée. Il a été introduit en 1953 par N. Metropolis, A.-W. Rosenbluth, M.-N. Rosenbluth, A.-H. Teller, E. Teller, dans l'article '' Equations of State Calculations by Fast Computing Machines, Journal of Chemical Physics 21 (6) 1087--1092. Il a ensuite été généralisé en 1970 par W.-K. Hastings dans Monte Carlo Sampling Methods Using Markov Chains and Their Applications'', Biometrika 57 (1) 97?109. Cet algorithme, et ses variantes, est un des plus utilisés du calcul scientifique, voir par exempletop ten algorithms of the century'' sur google. Son étude mathématique est par contre très loin d'être achevée et pose des problèmes fort intéressants de géométrie, de théorie spectrale, d'analyse, et bien sur de probabilités. Dans cet exposé, je commencerai par introduire l'algorithme sous sa forme historique : Comment choisir N disques de rayon r (sans recouvrement ) au hasard dans un carré? et j'indiquerai quelques résultats et problèmes ouverts sur ce modèle. Dans une deuxième partie, je montrerai comment les plus simples des algorithmes de Metropolis, associés à des marches aléatoires à ``petits pas'', conduisent à l'étude d'opérateurs qui généralisent les opérateurs du calcul pseudodifférentiel semiclassique usuel.

Etienne Duchesne, LIPN - Paris-Nord. 2:00:00 19 janvier 2012 10:00 limd
MELL in a free compact closure
Abstract

The categorical presentation of the standard model of the geometry of interaction –namely the free compact closure of sets and partial injections Int(PInj)– fails to be a denotational semantics of MELL. The work of Melliès, Tabareau & Tasson on the formula for a free exponential modality gives us insights into the reasons of this failure: absence of free pointed objects, absence of equalizers of some groups of permutations... We will present generic constructions which successively add the algebraic structure needed to compute this formula, and show that the usual model of GoI wrapped in these successive layers defines a denotational semantics of MELL.

Muhammad Humayoun, LAMA, LIMD. 2:00:00 18 janvier 2012 15:00 labo
Developing the System MathNat for Automatic Formalization of Mathematical texts
Abstract

There is a wide gap between the language of mathematics and its formalized versions. The term language of mathematics'' ormathematical language'' refers to prose that the mathematician uses in authoring textbooks and publications. It mainly consists of natural language, symbolic expressions and notations. It is flexible, structured and semantically well-understood by mathematicians. However, it is very difficult to formalize it automatically. Some of the main reasons are: complex and rich linguistic features of natural language and its inherent ambiguity; intermixing of natural language with symbolic mathematics causing problems which are unique of its kind, and therefore, posing more ambiguity; and the possibility of containing reasoning gaps, which are hard to fill using the current state of art theorem provers (both automated and interactive). One way to work around this problem is to abandon the use of the language of mathematics. Therefore in current state of art of theorem proving, mathematics is formalized manually in very precise, specific and well-defined logical systems. The languages supported by these systems impose strong restrictions. For instance, these languages have non-ambiguous syntax with a limited number of possible syntactic constructions. This enterprise divides the world of mathematics in two groups. The first group consists of a vast majority of mathematicians whose rely on the language of mathematics only. In contrast, the second group consists of a minority of mathematicians. They use formal systems such as theorem provers (interactive ones mostly) in addition to the language of mathematics. To bridge the gap between the language of mathematics and its formalized versions, we may ask the following gigantic question: Can we build a program that understands the language of mathematics used by mathematicians and can we mechanically verify its correctness? This problem can naturally be divided in two sub-problems, both very hard: 1. Parsing mathematical texts (mainly proofs) and translating those parse trees to a formal language after resolving linguistic issues. 2. Validation of this formal version of mathematics. The project MathNat (Mathematics in controlled Natural language) aims at being the first step towards solving this problem, focusing mainly on the first question. For that, first, we develop a Controlled Language for Mathematics (CLM) which is a precisely defined subset of English with restricted grammar and lexicon. To make CLM natural and expressive, we support important linguistic features such as anaphoric pronouns and references, rephrasing of a sentence in multiple ways, the proper handling of distributive and collective readings and so on. The coverage of CLM at the moment is yet rather small and to be improved as the project keeps evolving in future. Second, we develop MathAbs (Mathematical Abstract language). It is a prover independent formal language to represent the semantics of CLM texts preserving its logical and reasoning structure. MathAbs is designed as an intermediate language between CLM and the formal languages of theorem provers, allowing proof checking. Third, we propose a system that can automatically translate CLM to MathAbs, giving a precise semantics to CLM. We consider that formalizing mathematics automatically in such a formal language that has a precise semantics is an important progress even if it can't always be proof-checked. This brings us to the second question for which we report a very limited work. We only translate MathAbs to the first-order formulas. If we feed these formulas to the automated theorem provers (ATPs), then fundamentally the ATPs should be able to validate them sometimes. In other words, the resulting MathAbs document is not completely verifiable for the moment, but it represents an opportunity for the mathematician to write mathematical text (mainly proofs) without becoming expert of any theorem prover. Keywords: Computational linguistics, Controlled languages, Formalization, Formal systems, Verification, Proof checking.

Juan-Carlos Alvarez Paiva, Université de Lille. 2:00:00 13 janvier 2012 10:15 geo
Amuse-gueules finslériens
Abstract

Quelle est la loi de réfraction de la lumière quand celle-ci traverse des espaces normés ? Quel est le volume de la boule unitaire d'un espace normé ? Quelle est l'aire de la sphère unitaire ? Y-a-t'il une généralisation naturelle du théorème de Gauss-Bonnet pour les surfaces finslériennes ? Pour résumer le résumé: une introduction irresponsable et amusante à la géométrie finslérienne.

Eric Leichtnam, Jussieu. 2:00:00 6 janvier 2012 10:15 geo
Opérateur de la signature pour les espaces stratifiés
Abstract

Nous présenterons une nouvelle preuve du théorème (du à Cheeger) que l'opérateur de la signature est Fredholm sur un espace de Witt compact orientable. Les arguments de cette preuve permettent d'aborder le cas où l'espace n'est plus de Witt mais admet des conditions dites idéales au sens de Cheeger.

Assia Mahboubi, LIX. 2:00:00 5 janvier 2012 10:00 limd
Vers une vérification formelle de la preuve du théorème de Feit-Thompson
Abstract

Le théorème de Feit-Thompson (1963) est un résultat historique de théorie des groupes finis. En effet, il permet de comprendre la structure de tous les groupes finis simples d'ordre impair et constitue ainsi une étape importante dans la classification des groupes finis simples qui est considérée comme achevée depuis les années 80. Néanmoins cette classification a un statut controversé car elle résulte de la compilation d'un nombre considérable de publications hétérogènes et parfois encore mal comprises. La preuve du théorème de Feit-Thompson est elle-même imposante, par sa taille et par la variété des résultats sur lesquels elle repose (théorie des groupes, algèbre linéaire, théorie de Galois, caractères,...). Elle est un défi pour les assistants à la preuves, logiciels permettant de représenter énoncés et preuves mathématiques sous la forme de termes logiques, vérifiables mécaniquement par un ordinateur. Dans cet exposé, qui ne présuppose aucune connaissance préalable en théorie des groupes, nous essaierons de montrer quels problèmes sont posés par une telle formalisation, par la représentation des objets mathématiques mis en jeu en théorie des types et en particuliers les solutions qui ont été trouvées pour faire vérifier (une partie conséquente de) cette preuve par l'assistant à la preuve Coq.

Sergey Gavrilyuk, Aix-Marseille University, UMR CNRS 6595 IUSTI. 2:00:00 15 décembre 2011 14:00 edp
Modèles d'interfaces diffuses ``solide élasto-plastique-fluide compressible``
Abstract

On dérive un modele Eulerien d'interfaces di ffuses pour l'interaction ``solide élasto-plastique - fluide compressible'' dans le cas de grandes déformations. Les applications du modèle aux problèmes d'impact seront présentées. Références 1. Favrie, N. and Gavrilyuk, S. (2011a) Mathematical and numerical model for nonlinear viscoplas- ticity, Phil. Trans. R. Soc. A, 369, 2864-2880. 2. Favrie, N. and Gavrilyuk, S. (2011b) Di use interface model for compressible fluid-compressible elastic-plastic solid interaction, J. Computational Physics (soumis).

Annette Casagrande, LAMA, LIMD. 2:00:00 15 décembre 2011 10:00 limd
Proposition d'une mesure de voisinage entre textes Application à la veille stratégique
Abstract

Nous proposons une méthode de calcul de proximité entre textes, appelée mesure de voisinage. Cette mesure est basée sur la présence de mots communs, de synonymes et de mots cooccurrents. Nous comparons cette mesure à la similarité cosinus, utilisée en Recherche d'Informations, au travers de trois bases de données différentes. Nous avons développé un prototype, nommé ALHENA, utilisé dans le domaine de la veille stratégique anticipative (VAS). L'expérimentation menée sur la valorisation du CO2 a montré l'utilité du prototype dans le processus de VAS, face au problème de la surcharge d'information notamment occasionnée par l'usage de l'Internet.

F. Bihan, LAMA. 2:00:00 9 décembre 2011 14:30 geo
F. Bihan, LAMA. 2:00:00 9 décembre 2011 14:30 labo
E.-N. Dancer, Universite de Sydney. 2:00:00 2 décembre 2011 14:00 edp
Finite Morse index solutions and Applications
Abstract

We discuss linearized stable and finite Morse Index solutions of weakly nonlinear elliptic equations on all of R(N) or half spaces and discuss their application to bounded domain problems where either the diffusion is small or the solutions are large.

Karim Nour, LAMA, LIMD. 2:00:00 1 décembre 2011 10:00 limd
About the range property for H
Abstract

Recently, A. Polonsky has shown that the range property fails for H. We give here some conditions on a term F that imply that its range has cardinality either 1 or infinity. L'exposé sera accessible à tous les membres de l'équipe.

JERAA, Rhone Alpes. 2:00:00 18 novembre 2011 09:00 edp
A préciser
Abstract
Krzysztof Worytkiewicz, LAMA. 2:00:00 17 novembre 2011 10:00 limd
Simulations as homotopies
Abstract

We exhibit a model structure on 2-Cat. A certain class of homotopies in this model structure turns out to be in 1-to-1 correspondence with strong simulations among labeled transitions systems, formalising the geometric intuition of simulations as deformations. The correspondence still holds in the cubical setting, characterising simulations of higher-dimensional transition systems (HDTS).