Dans le contexte actuel d'urgence environnementale, la communauté européenne, sensible à la qualité de l'air et à l'épuisement des ressources fossiles fixe un objectif clair et ambitieux aux constructeurs automobiles pour les émissions de gaz à effet de serre. Les rejets de gaz carbonique ne devraient ainsi pas dépasser 120g/km à l'horizon 2015 et sans doute 90g vers 2018. Le travail de thèse s'insère dans cette dynamique urgente de réduction des émissions de dioxyde de carbone. Il s'agit de réduire la traînée aérodynamique de l'ordre de 20% afin de parvenir aux normes environnementales de 2015 et également de mieux comprendre la physique de la dynamique tourbillonnaire afin d'optimiser les solutions de contrôle. Concrètement, cela consiste à coupler deux méthodes de contrôle d'écoulement : un contrôle passif par la modification de l'état de surface des carrosseries par insertion de milieux poreux et un contrôle actif par la mise en place de jets soufflant et/ou aspirant à l'arrière du véhicule. L'étude est menée en 2D pour la configuration du corps d'Ahmed avec un culot droit puis en 3D pour la configuration avec une lunette inclinée à 25° avec une résolution directe des équations de Navier-Stokes. / In the present environmental urgency, the european community which is alive to the air quality and fossil resources rarefaction determines a clear and ambitious objective to the car makers for the greenhouse gas emissions. The carbon gas discharges will not exceed 120g/km for the year 2015 and probably 90g around the year 2018. The thesis work lies within this urgent dynamics of the carbon dioxide emissions. It is question of reducing the aerodynamic drag of the order of 20% to manage to the environmental limits of the year 2015 and also to better understand the vortex dynamics in order to improve the control solutions. In practical terms, it consists in coupling two flow control methods : a passive control with a wall modification using porous media and an active control with the use of blowing and/or sucking actuators at the car back wall. The study is lead in 2D for the square back Ahmed body and next in 3D for the Ahmed body with a rear window inclined at 25° with a direct resolution of the Navier-Stokes equations.

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.

Récemment, la géomatique grand public s'est emparée de la représentation 3D des bâtiments. Le besoin d'acquérir des images et de les restituer en 3D, sous forme de maquettes parfaitement fidèles à la réalité, est ainsi devenu immense. On a donc vu depuis une décennie, se construire des véhicules capables de photographier en stéréoscopie des villes entières, et il a fallu concevoir les algorithmes capables de traiter ces énormes quantités d'images. Très naturellement, les industriels en charge de ces problèmes se sont tournés vers les outils de vision par ordinateur et de robotique, très bien adaptés aux calculs temps réel, oubliant l'essentiel de l'héritage de la photogrammétrie, orientée quant à elle vers une extrême précision, jugée ici comme une moindre priorité. Néanmoins, les algorithmes publiés en vision par ordinateur présentaient de réels défauts lorsqu'ils étaient appliqués à des surfaces planes alors que ce cas est extrêmement courant dans des scènes urbaines pour traiter les façades de bâtiments. Les recherches que nous avons menées ont porté sur la recherche de solutions nouvelles, capables d'exploiter les spécificités de telles images : tout d'abord, nos travaux ont cherché à accélérer l'orientation relative des images, en tirant bénéfice des points de fuite figurant dans celles-ci. Pour ce faire, de nouvelles méthodes d'extraction automatique de ces points ont été mises au point et évaluées plus performantes que celles disponibles jusqu'ici. Ensuite, nos recherches ont porté sur les moyens de corriger le défaut évoqué précédemment pour les surfaces planes, et de nouveaux algorithmes capables de donner en temps quasi-réel de bonnes solutions d'orientation relative pour de telles scènes ont été développés. A cette fin, de nouveaux outils mathématiques ont été utilisés : les bases de Gröbner. En rupture complète avec les solutions linéaires habituelles, ils permettent en effet une résolution directe des équations sous leur forme polynomiale. Ils évitent de passer par l'habituelle linéarisation, qui nécessitait une solution approchée parfois difficile à trouver dans les usages de photogrammétrie terrestre. Finalement, nos travaux ont porté sur les moyens d'accélérer les méthodes d'orientation relative en exploitant opportunément la connaissance de la direction verticale, obtenue par exemple à l'aide du nouvel algorithme de détection des points de fuite. Au total, la thèse présente une remise à plat générale des solutions permettant l'orientation et la localisation de tout un ensemble d'images.

Le problème de la modélisation et de la simulation des mouvements du tronc pendant la respiration est étudié dans cette thèse. L'objectif est la représentation graphiquement réaliste de ces mouvements grâce à des modèles générateurs. Le découpage de ce document propose des étapes méthodologiques pour la modélisation.<br />Dans une première partie les principes mécaniques du phénomène de la respiration sont exposés. Le problème apparaît alors comme la modélisation et la simulation comportementale sous contraintes d'un objet complexe composés de régions ayant des propriétés différentes (élasticité, motricité, rigidité). Les modèles générateurs basés sur la physique se révèlent être les outils informatiques les plus aptes à atteindre notre objectif. Un état de l'art de ces méthodes et des problématiques liées est alors dressé.<br />La deuxième partie présente la construction du modèle informatique découpée en régions de propriétés spécifiques. On présente alors une nouvelle fonction d'élasticité utilisant l'expression d'une mémoire de forme locale. Comparée à un modèle classique masse-ressort, cette fonction d'élasticité prouve son efficacité. La modélisation des régions musculaires et solides est ensuite présentée. Puis, on montre la possibilité de contraindre ces régions afin de modéliser d'autres propriétés. On développe notamment une méthode de résolution directe permettant de vérifier des contraintes locales et globales sans utiliser d'algorithme itératif. La résolution de la contrainte d'incompressibilité illustre cette méthode de résolution ; les principes généraux de cette résolution sont dégagés permettant ainsi de généraliser son application.<br />La dernière partie de ce manuscrit fournit une validation qualitative du modèle développé par l'intermédiaire de différents exemples, dont celui de la simulation des mouvements du tronc pendant la respiration.