Le langage mathématique courant et les langages mathématiques formelssont très éloignés. Par <> nousentendons la prose que le mathématicien utilise tous les jours dansses articles et ses livres. C'est une langue naturelle avec desexpressions symboliques et des notations spécifiques. Cette langue està la fois flexible et structurée mais reste sémantiquementintelligible par tous les mathématiciens.Cependant, il est très difficile de formaliser automatiquement cettelangue. Les raisons principales sont: la complexité et l'ambiguïté deslangues naturelles en général, le mélange inhabituel entre languenaturelle et notations symboliques tout aussi ambiguë et les sautsdans le raisonnement qui sont pour l'instant bien au-delà descapacités des prouveurs de théorèmes automatiques ou interactifs.Pour contourner ce problème, les assistants de preuves actuelsutilisent des langages formels précis dans un système logique biendéterminé, imposant ainsi de fortes restrictions par rapport auxlangues naturelles. En général ces langages ressemblent à des langagesde programmation avec un nombre limité de constructions possibles etune absence d'ambiguïté.Ainsi, le monde des mathématiques est séparé en deux, la vastemajorité qui utilise la langue naturelle et un petit nombre utilisantaussi des méthodes formelles. Cette seconde communauté est elle-mêmesubdivisée en autant de groupes qu'il y a d'assistants de preuves. Onperd alors l'intelligibilité des preuves pour tous les mathématiciens.Pour résoudre ce problème, on peut se demander:est-il possible d'écrire un programme qui comprend la langue naturellemathématique et qui la traduit vers un langage formel afin depermettre sa validation?Ce problème se subdivise naturellement en deux sous-problèmes tous lesdeux très difficiles:1. l'analyse grammaticale des textes mathématiques et leur traductiondans un langage formel,2. la validation des preuves écrites dans ce langage formel.Le but du projet MathNat (Mathematics in controlled Natural languages)est de faire un premier pas pour répondre à cette question trèsdifficile, en se concentrant essentiellement sur la première question.Pour cela, nous développons CLM (Controlled Language for Mathematics)qui est un sous-ensemble de l'anglais avec une grammaire et un lexiquerestreint, mais qui inclut tout de même quelques ingrédientsimportants des langues naturelles comme les pronoms anaphoriques, lesréférences, la possibilité d'écrire la même chose de plusieursmanières, des adjectifs distributifs ou non, ...Le second composant de MathNath est MathAbs (Mathematical Abstractlanguage). C'est un langage formel, indépendant du choix d'un systèmelogique permettant de représenter la sémantique des textes enpréservant leur structure et le fil du raisonnement. MathAbs est conçucomme un langage intermédiaire entre CLM et un système logique formelpermettant la vérification des preuves.Nous proposons un système qui permet de traduire CLM vers MathAbsdonnant ainsi une sémantique précise à CLM. Nous considèrons que cetravail est déjà un progrès notable, même si pour l'instant on estloin de pouvoir vérifier formellement toutes les preuves en MathAbsainsi générées.Pour le second problème, nous avons réalisé une petite expérience entraduisant MathAbs vers une liste de formules en logique du premierordre dont la validité garantit la correction de la preuve. Nous avonsensuite essayé de vérifier ces formules avec des prouveurs dethéorèmes automatiques validant ainsi quelques exemples.

Le langage mathématique courant et les langages mathématiques formelssont très éloignés. Par <<langage mathématique courant>> nousentendons la prose que le mathématicien utilise tous les jours dansses articles et ses livres. C'est une langue naturelle avec desexpressions symboliques et des notations spécifiques. Cette langue està la fois flexible et structurée mais reste sémantiquementintelligible par tous les mathématiciens.Cependant, il est très difficile de formaliser automatiquement cettelangue. Les raisons principales sont: la complexité et l'ambiguïté deslangues naturelles en général, le mélange inhabituel entre languenaturelle et notations symboliques tout aussi ambiguë et les sautsdans le raisonnement qui sont pour l'instant bien au-delà descapacités des prouveurs de théorèmes automatiques ou interactifs.Pour contourner ce problème, les assistants de preuves actuelsutilisent des langages formels précis dans un système logique biendéterminé, imposant ainsi de fortes restrictions par rapport auxlangues naturelles. En général ces langages ressemblent à des langagesde programmation avec un nombre limité de constructions possibles etune absence d'ambiguïté.Ainsi, le monde des mathématiques est séparé en deux, la vastemajorité qui utilise la langue naturelle et un petit nombre utilisantaussi des méthodes formelles. Cette seconde communauté est elle-mêmesubdivisée en autant de groupes qu'il y a d'assistants de preuves. Onperd alors l'intelligibilité des preuves pour tous les mathématiciens.Pour résoudre ce problème, on peut se demander:est-il possible d'écrire un programme qui comprend la langue naturellemathématique et qui la traduit vers un langage formel afin depermettre sa validation?Ce problème se subdivise naturellement en deux sous-problèmes tous lesdeux très difficiles:1. l'analyse grammaticale des textes mathématiques et leur traductiondans un langage formel,2. la validation des preuves écrites dans ce langage formel.Le but du projet MathNat (Mathematics in controlled Natural languages)est de faire un premier pas pour répondre à cette question trèsdifficile, en se concentrant essentiellement sur la première question.Pour cela, nous développons CLM (Controlled Language for Mathematics)qui est un sous-ensemble de l'anglais avec une grammaire et un lexiquerestreint, mais qui inclut tout de même quelques ingrédientsimportants des langues naturelles comme les pronoms anaphoriques, lesréférences, la possibilité d'écrire la même chose de plusieursmanières, des adjectifs distributifs ou non, ...Le second composant de MathNath est MathAbs (Mathematical Abstractlanguage). C'est un langage formel, indépendant du choix d'un systèmelogique permettant de représenter la sémantique des textes enpréservant leur structure et le fil du raisonnement. MathAbs est conçucomme un langage intermédiaire entre CLM et un système logique formelpermettant la vérification des preuves.Nous proposons un système qui permet de traduire CLM vers MathAbsdonnant ainsi une sémantique précise à CLM. Nous considèrons que cetravail est déjà un progrès notable, même si pour l'instant on estloin de pouvoir vérifier formellement toutes les preuves en MathAbsainsi générées.Pour le second problème, nous avons réalisé une petite expérience entraduisant MathAbs vers une liste de formules en logique du premierordre dont la validité garantit la correction de la preuve. Nous avonsensuite essayé de vérifier ces formules avec des prouveurs dethéorèmes automatiques validant ainsi quelques exemples. / There is a wide gap between the language of mathematics and itsformalized versions. The term "language of mathematics" or"mathematical language" refers to prose that the mathematician uses inauthoring textbooks and publications. It mainly consists of naturallanguage, symbolic expressions and notations. It is flexible,structured and semantically well-understood by mathematicians.However, it is very difficult to formalize it automatically. Some ofthe main reasons are: complex and rich linguistic features of naturallanguage and its inherent ambiguity; intermixing of natural languagewith symbolic mathematics causing problems which are unique of itskind, and therefore, posing more ambiguity; and the possibility ofcontaining reasoning gaps, which are hard to fill using the currentstate of art theorem provers (both automated and interactive).One way to work around this problem is to abandon the use of thelanguage of mathematics. Therefore in current state of art of theoremproving, mathematics is formalized manually in very precise, specificand well-defined logical systems. The languages supported by thesesystems impose strong restrictions. For instance, these languages havenon-ambiguous syntax with a limited number of possible syntacticconstructions.This enterprise divides the world of mathematics in two groups. Thefirst group consists of a vast majority of mathematicians whose relyon the language of mathematics only. In contrast, the second groupconsists of a minority of mathematicians. They use formal systems suchas theorem provers (interactive ones mostly) in addition to thelanguage of mathematics.To bridge the gap between the language of mathematics and itsformalized versions, we may ask the following gigantic question:Can we build a program that understands the language of mathematicsused 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 thoseparse trees to a formal language after resolving linguistic issues.2. Verification of this formal version of mathematics.The project MathNat (Mathematics in controlled Natural language) aimsat being the first step towards solving this problem, focusing mainlyon the first question.First, we develop a Controlled Language for Mathematics (CLM) which isa precisely defined subset of English with restricted grammar anddictionary. To make CLM natural and expressive, we support some richlinguistic features such as anaphoric pronouns and references,rephrasing of a sentence in multiple ways and the proper handling ofdistributive and collective readings.Second, we automatically translate CLM to a system independent formaldescription language (MathAbs), with a hope to make MathNat accessibleto any proof checking system. Currently, we translate MathAbs intoequivalent first order formulas for verification.

Notre thèse s’inscrit dans le cadre des langages contrôlés pour le génie logiciel. Elle a pour but de faciliter l’adoption de l’approche par règles métier (ARM) par les entreprises en créant un langage contrôlé en vue d’aider à la spécification des règles métier par les experts métier. Notre solution va permettre de réduire la distance sémantique entre les experts métier et les experts système afin de répondre non seulement au besoin d’intercompréhension entre ces derniers mais aussi pour réaliser un transfert automatique de la description des règles métier vers les systèmes d’information (SI). Ce langage contrôlé que nous avons créé permettra d’assurer en plus la consistance et la traçabilité de ces règles avec leur implantation / Our thesis focuses on controlled natural languages (CNL) for software engineering. It aims at facilitating the adoption of the business rule approach (BRA) by companies by creating a CNL in order to help business experts in the specification of their business rules. Our solution will allow reducing the semantic gap between business experts and system experts to meet not only the need for mutual understanding between them but also to achieve an automatic transfer of the description of business rules to information systems (IS). The CNL that we have created will also ensure the consistency and the traceability of these rules together with their implementation

Les langages contrôlés sont des langages artificiellement définis utilisant un sous-ensemble du vocabulaire, des formes morphologiques, des constructions syntaxiques d'une langue naturelle tout en en éliminant la polysémie. En quelque sorte, ils constituent le pont entre les langages formels et les langues naturelles. De ce fait, ils remplissent la fonction de communication du médium texte tout en étant rigoureux et analysables par la machine sans ambiguïté. En particulier, ils peuvent être utilisés pour faciliter l'alimentation de bases de connaissances, dans le cadre d'une interface homme-machine.Le Service Hydrographique et Océanographique de la Marine (SHOM) publie depuis 1971 les Instructions nautiques, des recueils de renseignements généraux, nautiques et réglementaires, destinés aux navigateurs. Ces ouvrages complètent les cartes marines. Elles sont obligatoires à bord des navires de commerce et de pêche. D'autre part, l'Organisation Hydrographique Internationale (OHI) a publié des normes spécifiant l'échange de données liées à la navigation et notamment un modèle universel de données hydrographiques (norme S-100, janvier 2010). Cette thèse se propose d'étudier l'utilisation d'un langage contrôlé pour représenter des connaissances contenues dans les Instructions nautiques, dans le but de servir de pivot entre la rédaction du texte par l'opérateur dédié, la production de l'ouvrage imprimé ou en ligne, et l'interaction avec des bases de connaissances et des outils d'aide à la navigation. En particulier on étudiera l'interaction entre le langage contrôlé des Instructions nautiques et les cartes électroniques correspondantes. Plus généralement, cette thèse se pose la question de l'évolution d'un langage contrôlé et des ontologies sous-jacentes dans le cadre d'une application comme les Instructions nautiques, qui ont la particularité d'avoir des aspects rigides (données numériques, cartes électroniques, législation) et des aspects nécessitant une certaine flexibilité (rédaction du texte par des opérateurs humains, imprévisibilité du type de connaissance à inclure par l'évolution des usages et des besoins des navigants). De manière similaire aux ontologies dynamiques que l'on rencontre dans certains domaines de connaissance, on définit ici un langage contrôlé dynamique. Le langage contrôlé décrit dans cette thèse constitue une contribution intéressante pour la communauté concernée puisqu'il touche au domaine maritime, domaine encore inexploité dans l'étude des langages contrôlés, mais aussi parce qu'il présente un aspect hybride, prenant en compte les multiples modes (textuel et visuel) présents dans le corpus constitué par les Instructions nautiques et les documents qu'elles accompagnent. Bien que créé pour le domaine de la navigation maritime, les mécanismes du langage contrôlé présentés dans cette thèse ont le potentiel pour être adaptés à d'autres domaines utilisant des corpus multimodaux. Enfin, les perspectives d'évolution pour un langage contrôlé hybride sont importantes puisqu'elles peuvent exploiter les différents avantages des modes en présence (par exemple, une exploitation de l'aspect visuel pour une extension 3D). / Controlled Natural Languages (CNL) are artificial languages that use a subset of the vocabulary, morphological forms and syntactical constructions of a natural language while eliminating its polysemy. In a way, they constitute the bridge between formal languages and natural languages. Therefore, they perform the communicative function of the textual mode while being precise and computable by the machine without any ambiguity. In particular, they can be used to facilitate the population or update of knowledge bases within the framework of a human-machine interface.Since 1971, the French Marine Hydrographic and Oceanographic Service (SHOM) issues the French Coast Pilot Books Instructions nautiques , collections of general, nautical and statutory information, intended for use by sailors. These publications aim to supplement charts, in the sense that they provide the mariner with supplemental information not in the chart. They are mandatory for fishing and commercial ships. On the other hand, the International Hydrographic Organization (IHO) issued standards providing information about navigational data exchange. Among these standards, one of a particular interest is the universal model of hydrographic data (S-100 standard, January, 2010).This thesis analyses the use of a CNL to represent knowledge contained in the Instructions nautiques. This CNL purpose is to act as a pivot between the writing of the text by the dedicated operator, the production of the printed or online publication, and the interaction with knowledge bases and navigational aid tools. We will focus especially on the interaction between the Instructions nautiques Controlled Natural Language and the corresponding Electronic Navigational Charts (ENC).More generally, this thesis asks the question of the evolution of a CNL and the underlying ontologies involved in the Instructions nautiques project. Instructions nautiques have the particularity of combining both strictness (numerical data, electronic charts, legislation) and a certain amount of flexibility (text writing by human operators, unpredictability of the knowledge to be included due to the evolution of sailors¿ practices and needs). We define in this thesis a dynamic CNL in the same way that dynamic ontologies are defined in particular domains. The language described in this thesis is intended as an interesting contribution for the community involved in CNL. Indeed, it addresses the creation of a CNL for the unexploited domain of maritime navigation, but its hybrid aspects as well through the exploration of the multiple modalities (textual and visual) coexisting in a corpus comprising ENC and their companion texts. The mechanisms of the CNL presented in this thesis, although developed for the domain of the maritime navigation, have the potential to be adapted to other domains using multimodal corpuses. Finally, the benefits in the future of a controlled hybrid language are undeniable: the use of the different modalities in their full potential can be used in many different applications (for example, the exploitation of the visual modality for a 3D extension).