Cette thèse étudie la théorie de la correspondance et la théorie des preuves pour la logique modale monotone et les logiques qui en sont proches.La première partie de la thèse établit une connexion formelle entre la théorie de la correspondance algorithmique et des résultats de caractérisation duale pour les treillis finis, similaire à la caractérisation par Nation d'une hiérarchie de variétés de treillis qui généralise les treillis distributifs. Cette connexion formelle est établie en utilisant la logique modale monotone. Nous adaptons l'algorithme ALBA pour la correspondance à l'environnement de la logique modale monotone, et nous utilisons un encodage, induit par une dualité, des treillis finis sous forme de 'neighbourhood frames' pour traduire les termes de la théorie des treillis en formules de la logic modal monotone.La deuxième partie de la thèse étend la théorie des 'display calculi' à la logique Baltag-Moss-Solecki pour les actions épistémiques et la connaissance (Epistemic Actions and Knowledge), à la logique modale monotone et à la logique propositionnelle dynamique (PDL). Nos résultats incluent plusieurs méta-théorèmes d'élimination de la coupure qui généralisent le théorème original de Belnap dans des dimensions différentes et indépendantes. Les deux principales généralisations des 'display calculi' traitées dans la thèse sont : la généralisation d'une théorie pour les langages ne contenant qu'un seul type à une théorie pour les langages contenant plusieurs types, et la généralisation d'une théorie pour les calculs satisfaisant la propriété de 'display' aux calculs ne la satisfaisant pas. / The present thesis focuses on Monotone Modal Logic and closely related logics from the point of view of Correspondence Theory and Proof Theory.The first part of the thesis establishes a formal connection between algorithmic corre- spondence theory and certain dual characterization results for finite lattices, similar to Nation's characterization of a hierarchy of pseudovarieties of finite lattices progressively generalizing finite distributive lattices. This formal connection is established through monotone modal logic. Specifically, we adapt the correspondence algorithm ALBA to the setting of monotone modal logic, and we use a certain duality-induced encoding of finite lattices as monotone neighbourhood frames to translate lattice terms into formulas in monotone modal logic.The second part of the thesis extends the theory of display calculi to Baltag-Moss- Solecki's logic of Epistemic Actions and Knowledge (EAK), Monotone Modal Logic (MML), and Propositional Dynamic Logic (PDL). Our results include several cut-elimination metatheorems, which generalize the original metatheorem of Belnap in different and mutually independent dimensions. The two main generalizations of display calculi treated in the thesis are: the generalization from single type to multi-type languages, and from the full or relativized display property to no display property.

Le développement de nouveaux formalismes logiques est au cœur de nombreuses problématiques de méthodes formelles. Ces formalismes doivent répondre à la fois à des impératifs de modélisation (ils doivent permettre de décrire certains systèmes) et de calcul (ils doivent fournir des méthodes de calcul correctes et complètes). Dans ce contexte, nous nous intéressons aux logiques de ressources, en particulier les logiques BI et BBI qui traitent du partage et de la séparation de ressources et qui ont conduit aux diverses logiques de séparation dont les applications à la vérification de programmes se sont développées fortement ces dernières années. Nous proposons dans cette thèse d’étudier, à partir des logiques BI et BBI, des logiques de séparation modales et épistémiques en se focalisant sur leurs capacités de modélisation et leur expressivité mais aussi les nouveaux calculs de preuve pour ces logiques. Une première étude a porté sur la modélisation de propriétés dynamiques de ressources au travers d’une nouvelle logique LTBI, qui est une logique de séparation temporelle, fondée sur la logique BI et des modalités temporelles. Cette logique offre notamment des perspectives intéressantes de modélisation temporelle branchante, permettant par exemple de caractériser les processus multi-thread. Une étude complémentaire a porté sur la modélisation de l’accès par des agents à des propriétés sous conditions de posséder certaines ressources, au travers d’une nouvelle logique ERL, qui est une logique de séparation épistémique, fondée sur la logique BBI et des modalités épistémiques. Cette logique permet de nombreuses modélisations de systèmes de contrôle d’accès. En vue d’étendre l’expressivité de telles logiques de séparation, comme la logique BBI et ses variantes, une étude sur l’internalisation des symboles de ressources dans la syntaxe de la logique a été développée au travers des nouvelles logiques HRL et HBBI (version hybride de BBI). L’internalisation permet à la fois d’étendre l’expressivité des logiques et d’axiomatiser la logique BBI et certaines de ses variantes. Outre la conception de ces logiques, l’étude de leur sémantique et aussi de leurs capacités de modélisation, une partie de cette thèse a été consacrée à la définition de calculs de preuve, ici de tableaux, pour ces nouvelles logiques ainsi qu’à leurs preuves de correction et de complétude / The design of new logical formalisms is at the heart of several problems in formal methods. Those formalisms must respond to requirements both concerning modelling (they must be able to describe certain systems) and computing (they must provide complete and sound calculus methods). In this context, we look at resource logics, and in particular BI and BBI logics, that deal with the separation and sharing of resources and have led to several separation logics whose applications to software verification have been widely developped recently. We propose in this thesis, starting from BI and BBI logics, to study some modal and epistemic separation logics by focusing on their modelling capacities and their expresiveness, as well as on the new proof calculi for those logics. A first study deals with the modelling of dynamic resource properties through new logic LTBI, which is a temporal separation logic, based on BI logic and temporal modalities. This logic notably offers interesting perspectives in temporal branching modelling, allowing for instance to characterize multi-thread processes. A complementary study concerns the modelling of access by agents to properties under the conditions of posessing some resources, through a new logic ERL, which is an epistemic separation logic, based on BBI logic and epistemic modalities. This logic allows many modellings of access control systems. In order to extend the expressivity of such separation logics, like BBI logic and its variants, a study on the internalization of resources symbols in the logic’s syntax has been developed through the new logics HRL and HBBI (hybrid version of BBI). Internalization allows both the extension of the expressivity of logics and the axiomatisation of BBI logic and some of its variants. In addition to the conception of those logics, the study of their semantics and their modelling capacities, a part of this thesis is dedicated to the definition of proof calculs, here tableaux calculus, for those new logics, as well as their proof of soundness and completeness