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.
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.
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.
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.
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.
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).
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.
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.
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.
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).
Les théories homotopiques de champs quantiques (HQFTs) ont été introduites par V. Turaev. Ils sont une forme de QFT dans lesquelles les variétés ont des structures supplémentaires. Dans cet exposé, je vais passer rapidement en revue quelques bases de la théorie des modules croisés utile plus tard, et introduire les TQFTs et HQFTs avec un espace de but, B. Après classification des cas simples, nous allons examiner le cas dans lequel B est l'espace classifiant d'un module croisé. S'il y a assez de temps, nous aborderons quelques interprétations en forme de gerbes etc. Plan : 1. Motivation 2. Rappels et exemples (simples) des modules croisés. 3. Théories topologiques de champs quantiques (TTCQs = TQFTs); 4. Théories homotopiques de champs quantiques (THCQs = HQFTs); 5. Résultats de Classification: (i) B = K(pi; 1), (ii) B = K(A; 2); 6. Applications formelles et HQFTs formelles : résultats généraux; 7. C-algebras croisées; 8. Complexes croisés, groupes simpliciaux et espaces classifiants; 9. C-fonctions formelles simpliciales et FHCobord(d; C); 10. C-fibrés combinatoires : allant vers les Gerbes.
Le gradient horizontal est défini comme la projection du gradient (riemannien) sur une certaine distribution par rapport à une métrique donnée. Puisque l'inégalité de Lojasiewicz n'est plus forcément valable, gradient horizontal est plus difficile à étudier que gradient. Dans cet exposé, on essaye d'expliquer quelle est la difficulté quand on passe du cas de distributions de codimension 1 au cas de distributions de codimension 2. Au passage, on montre quelques propriétés génériques du gradient horizontal dans le cas le plus simple qui est le cas de structure d'Engel standard.
Finiteness spaces were introduced by Ehrhard as a model of linear logic, which relied on a finitess property of the standard relational interpretation and allowed to reformulate Girard's quantitative semantics in a simple, linear algebraic setting. I will review recent results obtained in a joint work with Christine Tasson, providing a very simple and generic construction of finiteness spaces: basically, one can ``transport'' a finiteness structure along any relation mapping finite sets to finite sets. Moreover, this construction is functorial under mild hypotheses, satisfied by the interpretations of all the positive connectives of linear logic. Recalling that the definition of finiteness spaces follows a standard orthogonality technique, fitting in the categorical framework established by Hyland and Schalk, I will show that the features of transport do not stand on the same level as the orthogonality category construction; rather, they provide a simpler and more direct characterization of the obtained structure, in a webbed setting. PS: Although I have slides (in english) ready for this presentation, it is best enjoyed in its chalk and blackboard version so I will stick to the latter.
On expliquera comment construire un anneau de Grothendieck pour les formules semi-algébriques réelles, dans lequel s'injecte l'anneau de Grothendieck des variétés algébriques K_0(A_R), et qui se réalise dans K_0(A_R) otimes Z[1/2]. On montre ensuite la formule de Denef-Loeser pour des fonctions zêta de nature semi-algébriques puis que les fibres de Milnor semi-algébriques motiviques induites par la rationalité des fonctions zêta se réalisent via la caractéristique d'Euler à supports compacts sur la caractéristique d'Euler des objets semi-algébriques sous-jacents.