Abstract
This thesis is situated at the intersection of several disciplines:on the one hand, mathematical logic and theoretical computer science, onthe other hand, natural language processing and formal semantics ofnatural language. The thread tying these topics together is the constant use of tools and methodologies of proof theory and by the philosophical problem that motivated our thesis: what are the links between the notion of proof and that of linguisticmeaning?More concretely, we study formal proofs systems. in these systemsproofs are seen as winning strategies for two-player games. In thegames one player, called the Proponent, tries to construct ajustification for a certain statement while the other, the Opponent,tries to refute this statement.Our thesis is composed of three parts, each part containing a maximum ofthree chapters.The first part is preparatory. In the two chapters that compose it wepresent the mathematical tools used in our thesis as well as thephilosophical question that underlie our research.The second part consists of two long chapters and presents the centralproof-theoretical results of our thesis.n the first chapter of this part we present a dialogical logic systemfor classical first order logic. We show that, given a formula A, A isa logical theorem if and only if there is a proponent winning strategy for A.Dialogical logic systems for classical first-order logic have existedsince the 1960's. However there is no convincing proof of this result inthe literature.In the second chapter of this second part we present a denotationalsemantics for the constructive variant of the modal logic K. Ourdenotational semantics is a game semantics: the proofs of modal logicare interpreted by winning strategies for two-player games. We show thatour game semantics has a remarkable property; it is 'fully complete':every winning strategy is the interpretation of a proof of modal logic.The third and last part of our thesis consists of three chapters. Eachchapter is devoted to an application of proof theory to the semanticsof natural language.In the first chapter, we study the relationship between the categoricalsyntactic analyses of a sentence and the logical representations of thesentence. We show that, when certain conditions are met, the functionthat transforms syntactic analyses of a sentence into logicalrepresentations is injective.In the second chapter of this third part, we use our dialogical logicsystem, together with type logical grammars, to solve textualentailment problems.In the last chapter of this section we present a formal system for theresolution of anaphora and ellipsis. This problem is usually addressedby model-theoretic methods. We, on the contrary, present a solutionbased on proof theory. We develop a dialogical logic system in whichanaphora and ellipsis can be solved in a simple way.In the conclusion, we sketch possible future developments ofour research. Both from a mathematical and logical point of view andfrom the point of view of natural language applications