Dans cette thèse nous étudions les sémantiques ludothéoriques, conçues comme les altérnatives à la sémantique traditionelle de Tarski, qui metent en marche le princip Meaning is in use et l’idée des jeux de language de second Wittgenstein: le sens des constantes logiques est donné par les règles qui en fixent l’usage et qui apparaissent dans les interactions social que sont les jeux de langage. Deux traditions ludotheorique sont présentées: Game Theoretical Semantics (GTS), proposé par Hintikka et Sandu en 1968 et Dialogical logic, proposé initialement par Paul Lorenzen et Kuno Lorenz en 1955 et developé à partir de 1993 par Shahid Rahman et ses collègues. En 1989 Hintikka et Sandu ont arrivé à l’idée des jeux avec des informations imparfaits qui les a emmené à Independence Friendly Logique (IF logic), logique du premiere ordre qui dépasse en expressivité la logique classique. Deux chapitres de cette thèse sont consacrés à l’axiom de choix et au traitement de l’anaphore, deux sujets choisis par Hintikka pour démontrer la fécondité de la logique IF et de GTS. Le but de cette thèse et de montrer que’il est possible de rendre compte aussi bien et à moindre frais dans le cadre dialogique. Plus précisément, la logique IF est comparée avec la théorie constructive des types dans la forme dialogique pour conclure à la supériorité de cette dernière qui a le même pouvoir explicatif qu’IF sans sacrifier pour autant la dimension inférentielle de la logique. / This thesis studies game-theoretically oriented semantics which provide an alternative to traditional Tarski-style semantics, implementing Wittgenstein’s idea of the meaning as use. Two different game theoretical traditions are presented: Game Theoretical Semantics (GTS), developed by Jaako Hintikka and Gabriel Sandu, and Dialogical logic, first introduced by Paul Lorenzen and Kuno Lorenz and further developed by Shahid Rahman and his associates. In 1989 Hintikka and Sandu came up with games with imperfect information. Those games yielded Independence friendly first-order logic (IF logic), exceeding the expressive power of classical first-order logic. It is expressive enough to enable formulating linearly, and at the first-order level, sentences containing branching quantification. Because of this characteristic, Hintikka claims that IF logic is most suitable for at least two main purposes: to be the logic of the first-order fragment of natural language; and to be the medium for the foundation of mathematics. This thesis aims to explore the above uses of IF logic. The properties of IF logic are discussed, as well as the advantages of this approach such as the possibility of taking account of (in)dependency relations among variables; GTS-account of two different notions of scope of quantifiers; the “outside–in” direction in approaching the meaning, which turns out to be advantageous over the traditional “inside-out” approach; the usefulness of game-theoretic reasoning in mathematics; the expressiveness of IF language, which allows formulating branching quantifiers on the first-order level, as well as defining the truth predicate in the language itself. We defend Hintikka’s stance on the first-order character of IF logic against some criticisms of this point. The weak points are also discussed: first and foremost, the lack of a full axiomatization for IF logic and second, the problem of signalling, a problematic phenomenon related to the possibility of imperfect information in a game. We turn to another game-theoretically oriented semantics, that of Dialogical Logic linked with Constructive Type Theory, in which dependency relations can be accounted for, but without using more means than constructive logic and the dialogical approach to meaning have to offer. This framework is used first to analyse and confront Hintikka’s take on the axiom of choice, and second to analyse the GTS account of anaphora.

Dans ce mémoire, nous proposons une solution possible à la question suivante : comment formaliser des environnements associés à un processus (quelconque) et comment utiliser les informations qu'ils contiennent pour produire des actions pertinentes ? Cette question nous a amené à introduire la notion de contexte ainsi qu'une représentation réutilisable des connaissances pour le formaliser. Nous nous sommes donc intéressés aux notions d'ontologies, de contextes et d'actions. Pour la représentation et le raisonnement sur les contextes et les actions, nous proposons une solution appelée DTF. Celle-ci étend une théorie constructive des types existante permettant ainsi de disposer d'une grande expressivité, de la décidabilité de la véri cation de types et d'un mécanisme de sous-typage e cace. Nous montrons comment modéliser les contextes et les actions sous la forme de types dépendants à partir des données fournies sur un problème et des actions à entreprendre pour le résoudre. En n, pour tester la faisabilité et pouvoir juger de la complexité d'une telle solution, un "démonstrateur de contexte " est réalisé avec un langage fonctionnel. Puis, une application test appelée " le monde du Wumpus " où un agent logiciel se déplace dans un environnement inconnu, est alors implantée en LISP.