Thèse numérisée par la Direction des bibliothèques de l'Université de Montréal.

Thèse numérisée par la Division de la gestion de documents et des archives de l'Université de Montréal.

Mémoire numérisé par la Direction des bibliothèques de l'Université de Montréal.

Les logiques hybrides accroissent les logiques modales avec des éléments pour décrire et raisonner à propos de l'identité, ce qui est crucial dans certaines situations. Les logiques modales que l'on connaît comme ``hybrides'' aujourd'hui remontent au travaux de Prior dans les années 1960, mais leur étude systématique n'a commencé qu'au bout des années 1990. Elles sont intéressantes en grande partie car elles comblent un manque en matière d'expressivité dans les logiques modales. D'ailleurs, elles sont connues parfois comme des ``logiques modales avec égalité''. L'un des thèmes centraux de cette thèse est le problème de la satisfiabilité pour celle qui est probablement la mieux connue des logiques hybrides: le système H(@,dwn), et pour certaines de ses sous-logiques. La satisfiabilité est le problème fondamental en raisonnement automatique. Dans le cas des logiques hybrides, elle a été étudiée essentiellement par la méthode des tableaux. Dans cette thèse, nous essayons de compléter le panorama en explorant la satisfiabilité des logiques hybrides par d'autres méthodes: la résolution du premier ordre et des variantes de calcul de résolution qui manipulent directement des formules hybrides. Nous présentons un certain nombre de traductions en temps linéaire de H(@,dwn) à la logique de premier ordre qui préservent la satisfiabilité. Elles sont conçues de façon telle qu'elles réduisent l'espace de recherche. Ensuite nous dirigeons notre attention vers les calculs qui manipulent directement des formules hybrides. En particulier, nous considérons le calcul de résolution directe. Inspirés par la résolution du premier ordre, nous transformons ce calcul en un calcul de résolution ordonnée avec des fonctions de sélection, et nous prouvons qu'il a la propriété de réduction des contre-exemples. Nous concluons ainsi qu'il est réfutationnellement complet et qu'il est compatible avec le fameux critère standard de redondance. Nous montrons également qu'une version raffinée de ce calcul constitue un procédure de décision pour H(@), un fragment décidable de H(@,dwn). Dans la dernière partie de cette thèse, nous explorons certaines formes normales des logiques hybrides et d'autres logiques modales étendues. Nous nous intéressons aux formes normales où certaines modalités ne sont jamais présentes dans la portée d'autres opérateurs modaux. Nous montrons qu'il est possible de profiter de ce type de transformations sous la forme d'un prétraitement, dans le but de réduire le nombre d'inférences nécessaires pour un prouveur modal. En nous efforçant de formuler ces résultats en tenant compte d'autres logiques modales étendues, nous arrivons à une formulation de la sémantique modale par un nouveau type de modèles définis de façon coinductif. Plusieurs logiques modales étendues (dont les logiques hybrides) peuvent être définies par des classes de modèles coinductifs. Ainsi, des résultats qui étaient habituellement prouvés séparément pour chaque langage (mais dont la preuve n'était souvent que de routine) peuvent être démontrés d'une façon générale. / Hybrid logics augment classical modal logics with machinery for describing and reasoning about identity, which is crucial in many settings. Although modal logics we would today call ``hybrid'' can be traced back to the work of Prior in the 1960's, their systematic study only began in the late 1990's. Part of their interest comes from the fact they fill an important expressivity gap in modal logics. In fact, they are sometimes referred to as ``modal logics with equality''. One of the unifying themes of this thesis is the satisfiability problem for the arguably best-known hybrid logic, H(@,dwn), and some of its sublogics. Satisfiability is the basic problem in automated reasoning. In the case of hybrid logics it has been studied fundamentally using the tableaux method. In this thesis we attempt to complete the picture by investigating satisfiability for hybrid logics using first-order resolution (via translations) and variations of a resolution calculus that operates directly on hybrid formulas. We present firstly several satisfiability-preserving, linear-time translations from H(@,dwn) to first-order logic. These are conceived in a way such that they tend to reduce the search space of a resolution-based theorem prover for first-order logic. We then move our attention to resolution-based calculi that work directly on hybrid formulas. In particular, we will consider the so-called direct resolution calculus. Inspired by first-order logic resolution, we turn this calculus into a calculus of ordered resolution with selection functions and prove that it possesses the reduction property for counterexamples from which it follows its completeness and that it is compatible with the well-known standard redundancy criterion. We also show that certain refinement of this calculus constitutes a decision procedure for H(@), a decidable fragment of H(@,dwn). In the last part of this thesis we investigate certain normal forms for hybrid logics and other extended modal logics. We are interested in normal forms where certain modalities can be guaranteed not to occur under the scope of other modal operators. We will see that these kind of transformations can be exploited in a pre-processing step in order to reduce the number of inferences required by a modal prover. In an attempt to formulate these results in a way that encompasses also other extended modal logics, we arrived at a formulation of modal semantics in terms of a novel type of models that are coinductively defined. Many extended modal logics (such as hybrid logics) can be defined in terms of classes of coinductive models. This way, results that had to be proved separately for each different language (but whose proofs were known to be mere routine) now can be proved in a general way.

Les objets électromagnétiques sont conçus en considérant des matériaux aux propriétés radio-électriques (permittivité, perméabilité) homogènes. Néanmoins, lors de leur réalisation les matériaux réels peuvent présenter des fluctuations de ces propriétés. Ce travail porte sur la mise au point d'outils capables d'estimer le champ diffusé produit par les fluctuations. Trois méthodes ont été mises au point : EMFORS, ABE et RECY pour la détermination du champ diffusé par des fluctuations de permittivité et de perméabilité. La modélisation de la contribution des fluctuations de perméabilité est une avancée significative. En effet, il n'existait pas d'outil traitant ce problème dans toute sa généralité pour estimer le champ diffusé par cette fluctuation. L'absence de magnétisme aux fréquences des ondes optiques en est la principale raison.La méthode RECY est une méthode qui permet d'estimer à l'aide du principe de réciprocité le champ diffusé dans un objet quelconque à partir de la simple connaissance du champ dans l'objet sans défaut et de la fluctuation. Cette méthode permet une fois le calcul du champ idéal effectué par une méthode quelconque (analytique ou numérique) de calculer le champ diffusé de n'importe quelle forme de fluctuation. Nous avons appliqué RECY à des structures comme un réseau simple, une structure industrielle et aux cristaux photoniques. / Electromagnetic objects are designed by considering homogeneous materials properties (permittivity, permeability). However, during their realization real materials may present fluctuations of their properties. This work focuses on the development of tools able to estimate scattered fields produced by fluctuations. Three methods have been developed: EMFORS, ABE and RECY for the determination of the scattered field by fluctuations of permittivity and permeability. Taking into account permeability fluctuations is a significant advance. Indeed, there was no tool to estimate the scattered field by such a fluctuation, due to the absence of magnetic properties at optical frequencies.The RECY method is a method which allows to estimate the field in an object using the principle of reciprocity from the knowledge of the field in the object without defect and of the fluctuation function. This method allows, once the ideal field calculated by any method (analytic or digital), to obtain the scattered field from any structure.We applied RECY for structures such as elementary gratings, an industrial structure and photonic crystals.

Deux groupes sont dits élémentairement équivalents s'ils satisfont les mêmes énoncés du premier ordre dans le langage des groupes. Aux environs de l'année 1945, Tarski posa la question suivante, connue désormais comme le problème de Tarski : les groupes libres non abéliens sont-ils élémentairement équivalents ? Une réponse positive à cette fameuse question fut apportée plus d'un demi-siècle plus tard par Sela, et en parallèle par Kharlampovich et Myasnikov, comme le point d'orgue de deux volumineuses séries de travaux. Dans la foulée, Sela généralisa aux groupes hyperboliques sans torsion, dont les groupes libres sont des représentants emblématiques, les méthodes de nature géométrique qu'il avait précédemment introduites à l'occasion de son travail sur le problème de Tarski. Les résultats rassemblés ici s'inscrivent dans cette lignée, en s'en démarquant toutefois dans la mesure où ils traitent des théories du premier ordre des groupes hyperboliques en présence de torsion. Dans un premier chapitre, on démontre, entre autres, que tout groupe de type fini qui est élémentairement équivalent à un groupe hyperbolique est lui-même hyperbolique. On démontre ensuite que les groupes virtuellement libres sont presque homogènes, ce qui signifie que deux éléments qui sont indiscernables du point de vue de la logique du premier ordre sont dans la même orbite sous l'action du groupes des automorphismes du groupe ambiant, à une indétermination finie près. Enfin, on donne une classification complète des groupes virtuellement libres de type fini du point de l'équivalence élémentaire à deux quantificateurs. / Two groups are said to be elementarily equivalent if they satisfy the same first-order sentences in the language of groups, that is the same mathematical statements whose variables are only interpreted as elements of a group. Around 1945, Tarski asked the following question : are non-abelian free groups elementarily equivalent? An affirmative answer to this famous Tarski's problem was given in 2006 by Sela and independently by Kharlampovich and Myasnikov, as the culmination of two voluminous series of papers. Then, Sela gave a classification of all finitely generated groups that are elementarily equivalent to a given torsion-free hyperbolic group. The results contained in the present thesis fall into this context and deal with first-order theories of hyperbolic groups with torsion. In the first chapter, we prove that any finitely generated group that is elementarily equivalent to a hyperbolic group is itself a hyperbolic group. Then, we prove that virtually free groups are almost homogeneous, meaning that elements are almost determined up to automorphism by their type, i.e. the first-order formulas they satisfy. In the last chapter, we give a complete classification of finitely generated virtually free groups up to elementary equivalence with two quantifiers.

Cette thèse s'inscrit dans le champ de la mesure et de l'explication de la santé dans un contexte d'analyse des inégalités de santé.<br /><br />Un premier chapitre considère les indicateurs de santé couramment utilisés dans les travaux empiriques et revient sur le débat de l'utilisation de la santé auto-évaluée. Il souligne la pertinence des raffinements méthodologiques de la mesure de la santé proposés dans la littérature internationale jusqu'ici non appliqués à la France.<br /><br />Un second chapitre propose une méthodologie originale de mesure de la santé. La construction s'appuie sur une donnée d'état de santé individuel jugée moins subjective, à savoir le nombre de maladies et leur degré de sévérité et considère des variables collectées classiquement dans les enquêtes sur la santé.<br /><br />Un troisième chapitre décrit les outils de la dominance stochastique et les indices couramment utilisés dans l'analyse des inégalités dans un cadre appliqué à la santé.<br /><br />Le quatrième chapitre procède à l'analyse des inégalités sociales de santé en France en 2004, puis au cours de la période 1998-2004. Il met en évidence des inégalités sociales de santé en faveur des groupes sociaux les plus élevés. Ces inégalités ont cependant diminué entre 1998 et 2004, du fait d'une plus faible élasticité de la santé avec le revenu et d'une diminution de l'inégale répartition du revenu au sein des groupes sociaux. De plus, l'analyse menée sur différentes mesures de santé met en évidence une influence sur l'amplitude des inégalités, du nombre de catégories de la variable discrète de santé et de la distribution de santé choisie pour la cardinaliser.<br /><br />Le cinquième chapitre s'intéresse à l'influence sur l'état de santé à l'âge adulte, du milieu social d'origine et de la longévité relative des parents par rapport à leur cohorte de naissance en empruntant trois approches. La première approche met en évidence le fait que les distributions d'état de santé des personnes nées d'un père ou d'une mère appartenant aux catégories sociales supérieures dominent significativement celles des personnes ayant des parents issus de catégories sociales inférieures. L'approche paramétrique confirme un effet de la profession de chacun des parents sur l'état de santé à l'âge adulte. Elle montre, de plus, que l'état de santé dépend significativement de la longévité de chacun des parents. Enfin, l'approche par indices de concentration met en évidence une inégalité des chances de santé en faveur des individus dont les parents ont connu une forte longévité puis une inégalité de santé en faveur des individus issus de milieux plus favorisés. Le chapitre conclut alors qu'il existe des inégalités des chances en santé, en France..

Le travail présenté dans ce mémoire est divisé en deux parties. La première partie est consacrée aux calculs des fonctions d'appui de la Jacobienne généralisée de Clarke et de son enveloppe plénière, associées à une fonction localement lipschtizienne à valeurs vectorielles. Clarke avait établi en 1975 que la fonction d'appui du sous-différentiel généralisé était une dérivée directionnelle généralisée. Il est donc satisfaisant de constater que la fonction d'appui de la Jacobienne généralisée est une sorte de "divergence directionnelle généralisée". Dans la seconde partie, nous présentons un certain nombre d'applications de techniques issues de l'Analyse non lisse à la résolution d'équations de Hamilton-Jacobi du premier ordre. Ainsi nous utilisons la dualité convexe et le calcul sous-différentiel pour prouver que les formules dites de Hopf-Lax définissent des solutions explicites des équations de Hamilton-Jacobi associées (avec données initiales semicontinues inférieurement). Nous n'utilisons ni le fameux principe de comparaison de la théorie des solutions de viscosité ni régularisation. Nous traitons successivement le cas de la dimension finie et de la dimension infinie. Ces résultats nous permettent de trouver des estimations des solutions d'équations dont l'hamiltonien est la différence de deux fonctions convexes. Enfin, nous nous attachons à l'étude des solutions sci dans des espaces de Banach dits ``lisses''. Le théorème de la valeur moyenne de Clarke et Ledyaev nous permet de montrer un résultat d'``enveloppe'' : nous construisons une solution sci pour une équation dont l'hamiltonien est le supremum d'une famille d'hamiltoniens. Nous appliquons enfin les mêmes techniques pour prouver l'existence d'une solution sci minimale sous des hypothèses plus faibles que celles que l'on recontre généralement dans la littérature.

Le but de ce travail est de proposer un système formel pour prouver que l'ensemble des succès d'un programme logique est inclus dans l'ensemble correspondant d'un autre programme. Cela permet de prouver que deux programmes logiques, un qui représente la spécification et un représentant l'implantation sont équivalents. Le langage logique considéré est CLPforall qui est le langage le langage de programmation logique avec contraintes (CLP) auquel est ajouté le quantificateur universel. Nous présentons les sémantiques des succès finis et infinis et montrons qu'elles sont données par le plus petit et le plus grand point fixe du même opérateur. Un système de preuve pour l'inclusion des succès finis est présenté. Le système utilise pour les opérateurs et les quantificateurs logiques les mêmes règles que la logique du premier ordre. Pour raisonner sur les prédicats récursifs le système contient une règle d'induction. Nous prouvons la correction du système sous certains conditions. Un système analogue pour l'inclusion des succès infinis est présenté. La règle d'induction est remplacée par une règle de coinduction. La correction est démontrée sous conditions analogues. Les deux systèmes sont équivalents sous certains conditions. Une implantation a été réalisée sous la forme d'assistant de preuve écrit en Prolog. Le programme a environ 4000 lignes et contient des procédures simples mais efficaces de recherche de preuves. Nous présentons des exemples de preuves réalises avec ce programme parmi lesquels la preuve de correction de quicksort.

Thèse numérisée par la Division de la gestion de documents et des archives de l'Université de Montréal