Cette thèse est une étude de la géométrie de l'interaction dans le facteur hyperfini (GdI5), introduite par Jean-Yves Girard, et de ses liens avec les constructions plus anciennes. Nous commençons par montrer comment obtenir des adjonctions purement géométriques comme une identité entre des ensembles de cycles apparaissant entre des graphes. Il est alors possible, en choisis- sant une fonction qui mesure les cycles, d'obtenir une adjonction numérique. Nous montrons ensuite comment construire, sur la base d'une adjonction numérique, une géométrie de l'interaction pour la logique linéaire multiplicative additive où les preuves sont interprétées par des graphes. Nous expliquons également comment cette construction permet de définir une sémantique dénotationnelle de MALL, et une notion de vérité. Nous étudions finalement une généralisation de ce cadre utilisant des outils de théorie de la mesure afin d'interpréter les exponentielles et le second ordre. Les constructions sur les graphes étant paramétrées par une fonction de mesure des cycles, nous entreprenons ensuite l'étude de deux cas particuliers. Le premier s'avère être une version combinatoire de la GdI5, et nous obtenons donc une interprétation géométrique de l'orthogonalité basée sur le déterminant de Fuglede-Kadison. Le second cas particulier est une version combinatoire des constructions plus anciennes de la géométrie de l'interaction, où l'orthogonalité est basée sur la nilpotence. Ceci permet donc de comprendre le lien entre les différentes versions de la géométrie de l'interaction, et d'en déduire que les deux adjonctions -- qui semblent à première vue si différentes -- sont des conséquences d'une même identité géométrique. Nous étudions ensuite la notion de vérité subjective. Nous commençons par considérer une version légè- rement modifiée de la GdI5 avec une notion de vérité dépendant du choix d'une sous-algèbre maximale commutative (masa). Nous montrons qu'il existe une correspondance entre la classification des masas introduite par Dixmier (regulière, semi-régulière, singulière) et les fragments de la logique linéaire que l'on peut interpréter dans cette géométrie de l'interaction. Nous étudions alors la vérité subjective de la GdI5, qui dépends du choix d'une représentation du facteur hyperfini de type II1, à la lumière de ce résultat. Finalement, nous détaillerons une proposition de Girard pour étudier les classes de complexité et dé- taillons la caractérisation obtenue par ce dernier de la classe de complexité co-NL, en montrant comment coder un problème complet pour cette classe à l'aide d'opérateurs.

Le but de la thèse est l'étude de certains "petits" groupes de rang de Morley fini. La conjecture de Cherlin-Zilber affirme que les groupes simples infinis de rang de Morley fini sont algébriques. Dans le cadre d'une approche inductive, "petit" doit signifier simple et minimal, dans le sens où le groupe ambiant est simple mais que toute section propre connexe en est résoluble. Le seul tel groupe algébrique est PSL2 ; la thèse est vouée à reconnaître ce groupe sous certaines hypothèses supplémentaires, et à limiter les pathologies sinon. On s'est placé en type impair, ce qui revient à attendre un corps (algébriquement clos) de caractéristique impaire ou nulle. L'identification de PSL2 (chapitre 3) ainsi que l'étude des éventuelles configurations non-algébriques (chapitre 5) repose essentiellement sur une notion d'unipotence en caractéristique nulle introduite par Burdges. Celle-ci permet dans le contexte simple connexe minimal de nombreux lemmes de rigidité, offrant ainsi une théorie complexe mais puissante des intersections de sous-groupes de Borel.

The doctoral dissertation introduces independence-friendly (IF) modal logic as an extension of standard modal logic. Making use of the notion of uniform strategy, a game-theoretical interpretation of IF modal logic is formulated. It is shown that under this interpretation, IF modal logic has greater expressive power than standard modal logic, and can be translated into first-order logic. However, when restricted to a simple tense-logical setting (evaluation over strict linear orders), its expressive power coincides with standard tense logic. The syntax of IF modal logic can be modified to allow independence of modal operators from conjunctions and disjunctions. It is shown that the resulting modal logic can no longer be translated into first-order logic. Two further interpretations of the language of IF modal logic are given, one in terms of backwards-looking operators, the other algebraic. The dissertation contains an extensive discussion of tenses in linguis- tics, and explains how the 'backwards-looking operators' interpretation of IF tense logic makes it possible to formally distinguish between two types of independence appearing in connection with tense evaluation. It is argued that the linguistic critique against scope theories of tense becomes less appealing when this distinction is made.

Dans cette thèse, nous présentons les relations entre le principe de réflexion MRP introduit par Moore, les propriétés d'arbres généralisées ITP et ISP introduites par Weiß, ainsi que les propriétés square introduites par Jensen et développées par Schimmerling. Le résultat principal de cette thèse est que MRP+MA entraine ITP(λ, ω2) pour tout cardinal λ ≥ ω2. Ce résultat implique par conséquent que les méthodes actuelles pour prouver la consistance de MRP+MA nécessitent au moins l'existence d'un cardinal supercompact. Il s'avère que MRP seul ne suffit pas à démontrer ce résultat, et nous donnons la démonstration que MRP n'entraine pas la propriété d'arbre plus faible, à savoir TP(ω2, ω2). De plus MRP+MA n'entraine pas le principe d'arbre plus fort ISP(ω2, ω2). Enfin nous étudions les relations entre MRP et des versions faibles de square. Nous montrons que MRP implique la négation de square(λ, ω) et MRP+MA implique la négation de square(λ, ω1) pour tout λ ≥ ω2.

Dans ce document, nous montrons comment la notion de calculabilité introduite par W. W. Tait et étendue par Girard aux types polymorphes peut être utilisée et facilement étendue pour montrer la terminaison de différents types de relations de réécriture, y compris avec filtrage sur des symboles définis, filtrage d'ordre supérieur ou réécriture de classe modulo certaines théories équationnelles. Nous montrons également que la notion de clôture de calculabilité donne lieu a une relation bien fondée incluant l'extension à l'ordre supérieur par J.-P. Jouannaud et A. Rubio de l'ordre récursif sur les chemins de N. Dershowitz.

La première étude systématique de la théorie des modèles positive était faite par Ben Yaacov qui a proposé une approche uniforme aux travaux précurseurs accomplis indépendamment par Robinson, Shelah, Hrushovski et Pillay avec un souci croissant d'incorporer les techniques modernes de la théorie des modèles dans le contexte des logiques réduites. Ben Yaacov et Poizat dans leur travail intitulé fondements de la logique positive ont défini un nouveau cadre pour la théorie des modèles positive, qui détermine le contexte de cette thèse. Dans le premier chapitre nous rappelons les outils de la théorie des modèle positive et nous développons des notions et des outils qui nous seront utiles dans le reste des chapitres. Parmi ceux-ci, il convient de souligner les extensions universelles. Elles caractérisent les bases d'amalgamation dans le deuxième chapitre, et sont cruciales dans la construction des domaines universels positifs. Dans le deuxième chapitre nous étudions la notion d'amalgamation qui s'avère centrale dans la théorie des modèles positive. Elle nous permettra d'étudier la conservation de la séparation topologique entre les extensions élémentaires positives, et de caractériser les théories de Robinson et l'élimination des quanteurs dans certaines classes des structures. Dans le troisième chapitre, nous continuons l'étude de la stabilité positive déjà entamée par Ben Yaacov, et nous en proposons une nouvelle caractérisation par une notion d'ordre propre à la théorie des modèles positive.

Cette thèse traite le développement d'un modèle mathématique d'optimisation acoustique des trajectoires de vol de deux avions commerciaux en approche sous contrainte énergétique, aérodynamique et opérationnelle. C'est un modèle analytique de contrôle optimal non-linéaire et non-convexe régi par un système d'équations différentielles ordinaires issues de la dynamique de vol et des contraintes associées. Notre contribution porte sur la modélisation mathématique des équations, l'optimisation et la programmation algorithmique d'un modèle d'optimisation non-linéaire du bruit de deux avions en approche simultanée. Les points abordés sont le développement mathématique du modèle 3D "exact" de leur dynamique de vol, la modélisation mathématique de la commande optimale de ce système dynamique, l'introduction de la consommation du carburant par les avions comme une équation différentielle avec une fonction consommation spécifique variable en fonction de l'évolution de leur dynamique, la modélisation mathématique instantanée de la fonction objectif représentant le bruit global des deux avions en approche. Sa résolution porte sur la méthode directe de programmation séquentielle quadratique avec régions de confiance sous AMPL et KNITRO. Une méthode indirecte a été appliquée sous le principe de maximum de Pontryagin suivie d'une discrétisation de type Runge-Kutta partition-née symplectique d'ordre 4 afin de démontrer la commutation entre l'approche directe et l'approche indirecte. Les résultats obtenus confirment des trajectoires optimales en descente continue, réduisant le bruit au sol ainsi que la consommation de kérosène de deux avions

Les systèmes pédagogiques sont apparus récemment à propos des calculs propositionnels (jusqu'à l'ordre supérieur), et consistent à donner systématiquement des exemples des notions (hypothèses) introduites. Formellement, cela signifie que pour mettre un ensemble Delta de formules en hypothèse, il est requis de donner une substitution sigma telle que les instances de formules sigma(Delta) soient démontrables. Cette nécessité d'exemplification ayant été pointée du doigt par Poincaré (1913) comme relevant du bon sens: une définition d'un objet par postulat n'ayant d'intérêt que si un tel objet peut être construit. Cette restriction appliquée à des systèmes formels intuitionnistes rejoint l'idée des mathématiques sans négation défendues par Griss (1946) au milieu du siècle dernier, et présentées comme une version approfondie de l'intuitionnisme. À travers l'isomorphisme de Curry-Howard (1980), la contrepartie calculatoire est l'utilité des programmes définis dans les systèmes fonctionnels correspondants: toute fonction peut être appliquée à un argument clos. Les premiers résultats concernant les calculs propositionnels jusqu'au second ordre ont été publiés récemment par Colson et Michel (2007, 2008, 2009). Nous exposons dans cette thèse une tentative d'uniformisation et d'extension au Calcul des Constructions (CC) des précédents résultats. Tout d'abord une définition formelle et précise de sous-système pédagogique du Calcul des Constructions est introduite, puis différents tels sous-systèmes sont déclinés en exemple.

Les questions <EM>"Qu'est-ce qu'une preuve?"</EM> et <EM>"Quand deux preuves sont-elles identiques?"</EM> sont fondamentales pour la théorie de la preuve. Mais pour la logique classique propositionnelle --- la logique la plus répandue --- nous n'avons pas encore de réponse satisfaisante. C'est embarrassant non seulement pour la théorie de la preuve, mais aussi pour l'informatique, où la logique classique joue un rôle majeur dans le raisonnement automatique et dans la programmation logique. De même, l'architecture des processeurs est fondée sur la logique classique. Tous les domaines dans lesquels la recherche de preuve est employée peuvent bénéficier d'une meilleure compréhension de la notion de preuve en logique classique, et le célèbre problème NP-vs-coNP peut être réduit à la question de savoir s'il existe une preuve courte (c'est-à-dire, de taille polynomiale) pour chaque tautologie booléenne. Normalement, les preuves sont étudiées comme des objets syntaxiques au sein de systèmes déductifs (par exemple, les tableaux, le calcul des séquents, la résolution, ...). Ici, nous prenons le point de vue que ces objets syntaxiques (également connus sous le nom d'arbres de preuve) doivent être considérés comme des représentations concrètes des objets abstraits que sont les preuves, et qu'un tel objet abstrait peut être représenté par un arbre en résolution ou dans le calcul des séquents. Le thème principal de ce travail est d'améliorer notre compréhension des objets abstraits que sont les preuves, et cela se fera sous trois angles différents, étudiés dans les trois parties de ce mémoire: l'algèbre abstraite (chapitre 2), la combinatoire (chapitres 3 et 4), et la complexité (chapitre 5).

Le but de ce mémoire est d'effectuer un survol de mes travaux effectués depuis janvier 2007. Le sujet d'étude se situe à l'une des intersections entre la combinatoire, la dynamique topologique et la logique via le formalisme des structures ultrahomogènes et de la théorie de Fraïssé. Ce domaine a récemment connu un essor considérable grâce à deux contributions majeures par Kechris, Pestov et Todorcevic, et par Kechris et Rosendal. Mon travail part de la première de ces contributions et se concentre autour des deux thèmes suivants : Théorie de Ramsey structurale et dynamique topologique des groupes de transformation associés.