Dans la tradition occidentale, mathématiques et musique ont été étroitement liées depuis plus de 2000 ans. Nonobstant cette longue histoire concernant les relations entre mathématiques et musique, l'intérêt professionnel des mathématiciens dans ce domaine est un phénomène assez récent. Alors que la puissance d'application des mathématiques dans la description de la musique a été reconnue depuis longtemps, c'est seulement grâce a des développements plus récents que la musique commence à occuper également une place stratégique au sein des mathématiques. Ce fait est confirmé par l'émergence d'un nombre croissant de problèmes «~mathémusicaux~». Ces problèmes sont caractérisés par le fait qu'en positionnant un problème à l'origine musical dans un contexte mathématique approprié non seulement on obtient des résultats mathématiques nouveaux mais cela ouvre la voie également à des constructions musicales nouvelles. C'est ce double mouvement, de la musique aux mathématiques et vice-versa, qui suscite l'intérêt de plus en plus de chercheurs dans les deux domaines et qui est au c\oe ur d'une croissante activité de recherche internationale accompagnée de la création de revues internationales à comité de lecture et collections d'ouvrages consacrés à la matière ainsi que d'une prolifération de conférences, séminaires d'études et projets collaboratifs dans le domaine. Dans la première partie de ce mémoire, nous présentons tout d'abord une sélection de problèmes «~mathémusicaux~» sur lesquels nous avons travaillé en montrant les résultats obtenus et les questions qui restent ouvertes. Dans la deuxième partie, nous détaillons trois types d'interactions entre recherche mathémusicale et trois autre disciplines, à savoir les sciences cognitives, l'informatique et la philosophie.

Cette thèse présente une formalisation des nombres algébriques et de leur théorie. Elle apporte deux nouvelles contributions importantes à la formalisation de résultats mathématiques dans des assistants à la preuve, ici Coq : la construction intuitionniste des nombres algébriques réels et la preuve qu'ils constituent un corps réel clos, ainsi que la programmation et la certification de procédures d'élimination des quantificateurs pour les théories des corps algébriquement clos et des corps réels clos. Pour atteindre ces résultats, nous avons apporté des contributions aux outils et aux méthodologies de preuves et de formalisation des mathématiques en Coq. En particulier, nous fournissons pour Coq/SSReflect un cadre pour travailler avec des types quotients. Nous fournissons une bibliothèque complète sur les structures algébriques de nombres ordonnés et normés. Nous avons réalisé une courte implémentation des réels de Cauchy accompagnée de tactiques pour effectuer facilement des raisonnements comportant des affirmations de la forme "soit n un entier suffisamment grand", couramment utilisés dans les preuves mathématiques sur papier. Nous avons également développé une petite bibliothèque d'analyse de base sur les polynômes à coefficients dans un corps réel clos. Une grande partie de nos résultats s'intègrent dans la formalisation de la preuve du théorème de Feit-Thompson et ont aussi pour objectif d'aider à certifier des procédures plus efficace d'élimination des quantificateurs sur les réels.

Les erreurs dimensionnelles des pièces d'une famille de pièces provoquent un mauvais placement initial de la pièce sur le montage affectant la qualité du produit final. Même si la pièce est positionnée correctement, la pièce s'écarte de cette position initiale à cause des forces externe d'usinage et de bridage et de la rigidité du montage. Dans cette thèse, un modèle analytique complet, composé d'un modèle cinématique et un modèle mécanique, ayant une configuration de type 3-2-1 des appuis est proposé. Le modèle cinématique remet la pièce, initialement mal placée dans la référence machine, sur la bonne position par les avancements axiales des six appuis en tenant compte de tout les éléments du montage considérés rigides. Cette pièce repositionnée se déplace à nouveau à partir de la position corrigée sous les forces de bridage et d'usinage. Le modèle mécanique calcule ce déplacement de la pièce en considérant les appuis et des brides élastiques. Le plateau cuboïde rigide, utilisé pour repositionner la pièce précisément, est également considéré élastique au niveau des contacts avec les appuis. Le comportement non-linéaire de la déformation des contacts est linéarisé en convergeant la déformation des appuis jusqu'à ce que la précision requise est atteinte. En utilisant l'hypothèse des petits déplacements et en considérant le frottement nul au niveau des contacts, On calcule le déplacement de la pièce, la déformation de chaque appui suivant l'énergie minimale, la matrice de rigidité et le comportement mécanique du système du montage grâce à la formalisation Lagrangienne. Le déplacement de la pièce est à nouveau compensé par l'avancement axial des six appuis calculés par le modèle cinématique.

Le laminage transversal, procédé de mise en forme des métaux essentiellement développé " à chaud ", permet d'obtenir des bruts de haut niveau de qualité en réalisant un gain notoire sur l'engagement matière face à d'autres procédés. Les travaux de thèse dressent l'état de l'art de cette technologie complexe et mal connue en France ; ils s'appuient sur une bibliographie dense et diversifiée pour synthétiser les lois qui régissent ce procédé et identifier les paramètres significatifs. Les conditions du contact pièce/outil étant prépondérantes, la mesure de la pression de contact est développée sur des matrices instrumentées afin de caractériser la sévérité des efforts. Des préformes en acier, titane et alliage base cuivre-aluminium avec simple réduction de diamètre sont fabriquées pour mettre en évidence les spécificités du contact pièce-matrice au niveau tribologique et rhéologique. En vue de démontrer que la condition d'entrainement en rotation des pièces est un facteur clé de pilotage du procédé, de nombreux essais expérimentaux pointent le rôle de la texture de surface pour l'obtention de pièces sans défaut, ainsi que son influence sur l'histoire thermomécanique interne. Les nombreuses difficultés liées à la mise au point d'outillages sont identifiées sur la base d'observations expérimentales et ensuite intégrées dans une démarche de conception d'outillage. Une procédure de conception d'outillage est ainsi proposée en s'appuyant sur une synthèse de règles issues de la bibliographie ainsi que de règles déterminées par les travaux expérimentaux. Une étude de cas sur une préforme " balustre " est traitée ; elle intègre la conception des matrices, la simulation numérique avec le logiciel FORGE© ainsi que les essais de mise au point d'outillage sur un banc développé à l'ENSAM. Une vision d'ensemble sur le procédé et les paramètres qui le gouvernent est finalement proposée.

L'objet de cette thèse est la formalisation et l'automatisation du raisonnement géométrique au sein de l'assistant de preuve Coq.<br />Dans une première partie, nous réalisons un tour d'horizon des principales axiomatiques de la géométrie puis nous présentons une formalisation des huit premiers chapitres du livre de Schwabäuser, Szmielew et Tarski: Metamathematische Methoden in der Geometrie.<br />Dans la seconde partie, nous présentons l'implantation en Coq d'une procédure de décision pour la géométrie affine plane : la méthode des aires de Chou, Gao et Zhang. Cette méthode produit des preuves courtes et lisibles.<br />Dans la troisième partie, nous nous intéressons à la conception d'une interface graphique pour la preuve formelle en géométrie : Geoproof. GeoProof combine un logiciel de géométrie dynamique avec l'assistant de preuve Coq.<br />Enfin, nous proposons un système formel diagrammatique qui permet de formaliser des raisonnements dans le domaine de la réécriture abstraite. Il est par exemple possible de formaliser dans ce système la preuve diagrammatique du lemme de Newman. La correction et la complétude du système sont prouvées vis-à-vis d'une classe de formules appelée logique cohérente.

Le logiciel Coq est un assistant à la preuve basé sur le Calcul des<br />Constructions Inductives.<br /> Dans cette thèse nous proposons d'améliorer l'automatisation de ce<br /> système en le dotant d'une procédure de décision réflexive et complète<br />pour la théorie du premier ordre de l'arithmétique réelle.<br /> La théorie des types implémentée par le système Coq comprend un<br />langage fonctionnel typé dans lequel nous avons programmé un<br />algorithme de Décomposition Algébrique Cylindrique (CAD). Cet<br />algorithme calcule une partition de l'espace en cellules<br />semi-algébriques sur lesquelles tous les polynômes d'une famille donnée <br />ont un signe constant et permet ainsi de décider les formules de cette théorie.<br /> Il s'agit ensuite de prouver la correction de l'algorithme et de la<br />procédure de décision associée avec l'assistant à la preuve Coq.<br /> Ce travail comprend en particulier une librairie d'arithmétique polynomiale<br />certifiée et une partie significative de la preuve formelle de correction de<br />l'algorithme des sous-résultants. Ce dernier algorithme permet de calculer<br />efficacement le plus grand commun diviseur de polynômes à coefficients dans un<br />anneau, en particulier à plusieurs variables.<br /> Nous proposons également une tactique réflexive de décision des égalités dans les<br />structures d'anneau et de semi-anneaux qui améliore les performances de l'outil<br />déjà disponible et augmente son spectre d'action en exploitant les possibilités de<br />calcul du système.<br /> Dans une dernière partie, nous étudions le contenu calculatoire d'une preuve<br />constructive d'un lemme élémentaire d'analyse réelle, le principe d'induction<br />ouverte.

This thesis presents an approach to design, specify, validate, verify, implement, and evaluate composed web/grid services. Web and grid services can be composed to create new services with complex behaviours. The BPEL (Business Process Execution Language) standard was created to enable the orchestration of web services, but there have also been investigation of its use for grid services. BPEL specifies the implementation of service composition but has no formal semantics; implementations are in practice checked by testing. Formal methods are used in general to define an abstract model of system behaviour that allows simulation and reasoning about properties. The approach can detect and reduce potentially costly errors at design time. CRESS (Communication Representation Employing Systematic Specification) is a domainindependent, graphical, abstract notation, and integrated toolset for developing composite web service. The original version of CRESS had automated support for formal specification in LOTOS (Language Of Temporal Ordering Specification), executing formal validation with MUSTARD (Multiple-Use Scenario Testing and Refusal Description), and implementing in BPEL4WS as the early version of BPEL standard. This thesis work has extended CRESS and its integrated tools to design, specify, validate, verify, implement, and evaluate composed web/grid services. The work has extended the CRESS notation to support a wider range of service compositions, and has applied it to grid services as a new domain. The thesis presents two new tools, CLOVE (CRESS Language-Oriented Verification Environment) and MINT (MUSTARD Interpreter), to respectively support formal verification and implementation testing. New work has also extended CRESS to automate implementation of composed services using the more recent BPEL standard WS-BPEL 2.0.

Cette étude porte sur les différentes formalisations du sens linguistique dans le cadre de la théorie Sens-Texte (TST) ; elle s’intéresse notamment à la représentation sémantique, la représentation la plus importante dans la modélisation du sens d’énoncés et d’unités lexicales de la langue. Cette étude a trois objectifs : premièrement, décrire trois formalisations de la représentation sémantique existant dans la TST – les réseaux sémantiques, les définitions lexicographiques et les définitions de la BDéf (des définitions très formalisées) ; deuxièmement, identifier les disparités et les décalages entre les formalisations choisies ; troisièmement, proposer des modifications aux formalisations existantes pour réduire au maximum ces disparités. / This study explores the different formalisations of linguistic meaning as encountered in the Meaning-Text Theory (MST) framework. Its main interest is semantic representation, which is the most important representation in the modeling of the meaning of utterances and lexical units. This study has three objectives: first, describing three existing formalisations of semantic representation in the MST – semantic networks, lexicographical definitions, and BDéf definitions (definitions that are extremely formalized); second, identifying the discrepancies between these formalisations; finally, proposing modifications to these formalisations in order to reduce the disparities as much as possible.

Pour demeurer compétitives, de plus en plus d'entreprises sont amenées à collaborer dans le cadre des entreprises étendues ou des réseaux d'entreprises. Ce type d'organisation nécessite l'interconnexion d'une multitude de systèmes d'entreprises, hétérogènes que ce soit par les fonctions qu'ils assurent ou par leurs conceptions (modèles, architectures, ...). Typiquement, ceci renvoie au concept de l'interopérabilité, définie par la capacité des systèmes ou des organisations à fournir ou à accepter des services et à utiliser ces services pour opérer efficacement ensemble. L'échange de l'information et le partage des connaissances (interopérabilité technique) entre les différents systèmes d'information sont désormais des atouts majeurs pour favoriser l'activité collaborative de création de valeur. Le développement de nouvelles technologies et la mise en place de standards a contribué à résoudre (partiellement au moins) ce problème d'interopérabilité technique. Cependant, ce n'est pas suffisant pour garantir l'interopérabilité à un niveau conceptuel : c'est-à-dire garantir que les modèles issus d'une ingénierie peuvent être partagés et compris par rapport à une sémantique commune, et utilisés par les différents systèmes d'entreprise pour réaliser une mission globale. L'approche de gestion du cycle de vie du produit (PLM) est considérée comme une solution essentielle pour faciliter le partage de modèles relatifs à des produits fabriqués. Elle vise à fournir une plate-forme commune qui rassemble les différents systèmes de l'entreprise à chaque étape du cycle de vie du produit dans ou à travers les entreprises. Bien que les principaux éditeurs de logiciels fassent des efforts pour créer des outils offrant un ensemble complet et intégré de modèles, la plupart d'entre eux n'intègrent pas une gestion cohérente des connaissances formalisées dans ces modèles spécifiques à chaque métier. L'hétérogénéité tant syntaxique que sémantique de ces modèles est souvent source d'une interprétation erronée des spécifications produites par chaque environnement de modélisation. L'objectif de cette thèse est ainsi de proposer une méthode, une formalisation et des outils pour prendre en compte, tout au long du cycle de vie d'un produit, l'ensemble des connaissances tacites et explicites sous la forme d'annotations sémantiques formelles qui peuvent favoriser la compréhension partagée ainsi qu'une vérification de cohérence des modèles produits, dans un contexte PLM.

Like many industries, the nuclear power industry in Sweden is currently facing the challenges of a major generational change. To meet these challenges, alongside the demands for a high level of security, the industry has attempted to standardise its mode of operations as far as possible. Apart from various technological fixes and safety devices, manuals and instructions have been modelled for every conceivable situation, or course of events; documentations and formal systems of co-ordination that become larger and larger, and more and more detailed. In high-risk industries there is a tendency to equate learning with changes in external patterns of behaviour, as against fixed standards, typically among operating staff. The acquisition  of professional skill, on the other hand, is the result of participation in practice. From this point of view, rather, learning is the outcome of reflection, upon actual events and experiences. Recurrent training can be used to promote formalisation, but also to explore and reinforce the experience based knowledge of skilled operators; between these approaches, the former prevails. Accidents and incidents incessantly put in question what is commonly referred to as the safety culture of various power plants, and subsequent to the misfortunes at Forsmark 1 in 2006, the accident was described as the culmination of a longterm decline in safety culture. The strong requirement for security and control is a cause of formalisation, whereas the need to support reflection as formation of professional skill tends to be omitted. Even so, experience based skill and knowledge remains a substantial consituent of what could be regarded as a dependable safety culture. Codified knowledge must be interpreted and applied in practice. Furthermore, experienced professionals, from encountering a great variety of situations, seem to develop what can be described as the skill of anticipation, and, as shown in connection with the incident at Forsmark 1, an ability to handle the unexpected. The urge for formalisation raises certain concerns: that of the primacy of defining the containments of professional skill, the impact and resilience of local knowledge and diversity, and the hollowing out of ability and skill within work-life organisations. The “human factor”, that is the operating staff, is commonly made responsible for established accidents and incidents. Even so, experienced personnel are able to manage a variety of unforeseen events and disturbances, that sometimes occur in high-risk technology industries. At times, on the contrary, the human factor saves technology, instead of the other way around. This study explores the concept of safety culture within the nuclear power industry from an epistemological perspective. It discusses the use of recurrent training, and the role of experience based skill and knowledge in the operating of Swedish power plants. What methods can be employed to support experience based knowledge as an essential complement to standardised work processes, codified knowledge, or benchmark strategies? Principles of formalisation need to be supplemented with a more thorough exploration of professional skill, in which a distinction between behaviour and responsibility can be made. / QC 20110906