Pour modéliser le fonctionnement d'un système, décrire une situation ou représenter des idées, on se met intuitivement à dessiner des bulles et les lier par des flèches sous forme de graphes étiquetés. Les logiques modales constituent un cadre formel expressif et extensible qui permet de définir ces graphes sous forme de « modèles », et d'exprimer certaines propriétés de ces graphes sous forme de « formules » afin de pouvoir raisonner là-dessus: model checking, test de satisfiabilité ou de validité, etc. Pour des formules et modèles de tailles importantes, ces tâches deviennent compliquées. De ce fait, un outil permettant de les réaliser automatiquement s'avère nécessaire. LoTREC en est un exemple. Il permet à son utilisateur de créer sa propre méthode de preuve, grâce à un langage simple et de haut niveau, sans avoir besoin d'aucune expertise spécifique en programmation. Durant ma thèse, j'ai revu le travail qui était déjà accompli dans LoTREC et j'ai apporté de nouvelles extensions qui s'avéraient nécessaires pour pouvoir traiter de nouvelles logiques (K.alt1, universal modality, Hybrid Logic HL(@),Intuitionistic logic, Public Announcement Logic, ...) et offrir à l'utilisateur certaines nouvelles techniques. D'autre part, j'ai examiné les origines de LoTREC dans le monde de réécriture de graphes et j'ai spécifié la sémantique de son moteur de réécriture. Cela a permis d'éclaircir comment l'on peut hériter dans nos méthodes de preuve des résultats et des propriétés théoriques déjà bien établies dans le domaine de la réécriture de graphes.

En informatique, la notion de ressource est une notion centrale. Nous considérons comme ressource toute entité pouvant être composée ou décomposée en sous-entités. Plusieurs logiques ont été proposées afin de modéliser et d’exprimer des propriétés sur celles-ci, comme la logique BI exprimant des propriétés de partage et de séparation. Puisque les systèmes informatiques manipulent des ressources, la proposition de nouveaux modèles capturant la dynamique de ces ressources, ainsi que la vérification et la preuve de propriétés sur ces modèles, sont des enjeux cruciaux. Dans ce contexte, nous définissons de nouvelles logiques permettant la modélisation logique de la dynamique des ressources, proposant de nouveaux modèles et permettant l’expression de nouvelles propriétés sur cette dynamique. De plus, pour ces logiques, nous proposons des méthodes des tableaux et d’extraction de contre-modèles. Dans un premier temps, nous définissons de nouveaux réseaux de Petri, nommés ß-PN, et proposons une nouvelle sémantique à base de ß-PN pour BI. Puis nous proposons une première extension modale de BI, nommée DBI, permettant la modélisation de ressources ayant des propriétés dynamiques, c’est-à-dire évoluant en fonction de l’état courant d’un système. Ensuite, nous proposons une logique, nommée DMBI, modélisant des systèmes manipulant/produisant/consommant des ressources. Par ailleurs, nous proposons une nouvelle logique (LSM) possédant de nouvelles modalités multiplicatives (en lien avec les ressources). Pour finir, nous introduisons la séparation au sein des logiques épistémiques, obtenant ainsi une nouvelle logique ESL, exprimant de nouvelles propriétés épistémiques / In computer science, the notion of resource is a central concern. We consider as a resource, any entity that can be composed or decomposed into sub-entities. Many logics were proposed to model and express properties on these resources, like BI logic, a logic about sharing and separation of resources. As the computer systems manipulate resources, a crucial issue consists in providing new models that capture the dynamics of resources, and also in verifying and proving properties on these models. In this context, we define new logics with new models and new languages allowing to respectively capture and express new properties on the dynamics of resources. Moreover, for all these logics, we also study the foundations of proof search and provide tableau methods and counter-model extraction methods. After defining new Petri nets, called ß-PN, we propose a new semantics based on ß-PN for BI logic, that allows us to show that BI is able to capture a kind of dynamics of resources. After observing that it is necessary to introduce new modalities in BI logic, we study successively different modal extensions of BI. We define a logic, called DBI, that allows us to model resources having dynamic properties, meaning that they evolve during the iterations of a system. Then, we define a logic, called DMBI, that allows us to model systems that manipulate/produce/consume resources. Moreover, we define a new modal logic, called LSM, having new multiplicative modalities, that deals with resources. Finally, we introduce the notion of separation in Epistemic Logic, obtaining a new logic, called ESL, that models and expresses new properties on agent knowledge

L’objectif de cette thèse est de développer et de proposer de nouvellesméthodes de réduction de dimension pour la construction d’indicateurs composites dequalité de vie à l’échelle communale. La méthodologie statistique développée met l’accentsur la prise en compte de la multidimensionnalité du concept de qualité de vie, avecune attention particulière sur le traitement de la mixité des données (variables quantitativeset qualitatives) et l’introduction des conditions environnementales. Nous optonspour une approche par classification de variables et pour une méthode multi-tableaux(analyse factorielle multiple pour données mixtes). Ces deux méthodes permettent deconstruire des indicateurs composites que nous proposons comme mesure des conditionsde vie à l’échelle communale. Afin de faciliter l’interprétation des indicateurscomposites construits, une méthode de sélection de variables de type bootstrap estintroduite en analyse factorielle multiple. Enfin nous proposons la méthode hclustgeode classification d’observations qui intègre des contraintes de proximité géographiqueafin de mieux appréhender la spatialité des phénomènes mis en jeu. / The purpose of this thesis is to develop and suggest new dimensionreduction methods to construct composite indicators on a municipal scale. The developedstatistical methodology highlights the consideration of the multi-dimensionalityof the quality of life concept, with a particular attention on the treatment of mixeddata (quantitative and qualitative variables) and the introduction of environmentalconditions. We opt for a variable clustering approach and for a multi-table method(multiple factorial analysis for mixed data). These two methods allow to build compositeindicators that we propose as a measure of living conditions at the municipalscale. In order to facilitate the interpretation of the created composite indicators, weintroduce a method of selections of variables based on a bootstrap approach. Finally,we suggest the clustering of observations method, named hclustgeo, which integratesgeographical proximity constraints in the clustering procedure, in order to apprehendthe spatiality specificities better.

L'un des moyens pour faire face à la réduction de l'utilisation d'intrants de synthèse est de favoriser durablement les services agro-écologiques de la diversité végétale. Pour cela, l'agriculteur devra adapter ses modes de gestion. Ma thèse s'inscrit dans l'objectif finalisé d'apporter à l'agriculteur, de l'aide à la gestion de cette diversité végétale sur le territoire de son exploitation. Je me suis fixé 2 objectifs de recherche : i) vérifier si les interchamps et le stock semencier constituent des sources d'espèces pour le centre des parcelles agricoles et ii) quantifier l'influence de la dynamique de deux grands groupes de facteurs, représentée sous la forme de trajectoires de parcelles, sur la diversité végétale : les pratiques agricoles et les caractéristiques de la mosaïque paysagère.J'ai mené ce travail sur l'ensemble du parcellaire de l'Installation Expérimentale de l'Inra ASTER Mirecourt, dont les systèmes de production (polyculture-élevage bovin laitier) sont convertis à l'agriculture biologique depuis 2004. J'ai caractérisé la végétation - en place dans les interchamps et au centre des parcelles, et dans le stock semencier - des parcelles en prairies permanentes et en champs cultivés selon deux approches complémentaires : taxonomique au rang de l'espèce et fonctionnelle à partir de sept propriétés rendant compte de la dissémination, de l'établissement et de la survie des espèces végétales. J'ai caractérisé les trajectoires des parcelles, sur une durée de neuf ans, soit à partir des pratiques agricoles mises en œuvre chaque année, soit à partir des caractéristiques annuelles de la mosaïque paysagère. Cette mosaïque correspond aux différentes occupations du sol obtenues à partir de relevés de terrain ou d'enquêtes auprès des exploitants.Je montre que le stock semencier et les interchamps ne constituent pas des sources potentielles d'espèces végétales pour le centre des parcelles, champs cultivés ou prairies permanentes. En revanche, ce sont des refuges importants pour une grande partie des espèces prairiales. Au vu de mes résultats, je fais l'hypothèse que les interchamps sont des puits d'espèces adventices en champs cultivés. J'ai également mis en évidence que le gradient fonctionnel de la végétation prairiale entre la bordure et le centre s'étend jusqu'à 2 m seulement.Enfin, la diversité végétale des parcelles étudiées est principalement influencée par la trajectoire des parcelles selon les caractéristiques de la mosaïque paysagère et par les pratiques agricoles mises en œuvre durant l'année en cours. Les caractéristiques du sol ont un rôle très minoritaire. Ces trois groupes de facteurs expliquent à eux seuls plus des trois quarts de la variabilité de la composition fonctionnelle de la végétation.La gestion de la diversité végétale des parcelles agricoles d'une exploitation peut donc être menée en partie par l'agriculteur. Cependant, compte-tenu des effets de la trajectoire des parcelles selon les caractéristiques paysagères, il est nécessaire de mettre aussi en place une gestion collective de la végétation entre les différents acteurs partageant le territoire / One of the means to offset the decrease of pesticide use is to favour agro-ecological services of plant diversity. In this aim, farmer will have to adapt its farming management. My work partly answers to the following applied objective: to bring to the farmer some advices for the management of plant diversity on the farm territory. I have two scientific objectives: i) to verify if field boundaries and soil seed bank are potential sources of plant species for field centres; ii) to quantify the relative influence of dynamics of two factor groups, characterized as field paths, on plant diversity: farming practices and characteristics of landscape mosaïc.I have carried out this study on the experimental farm of INRA ASTER Mirecourt. Its farming systems (mixed crop-dairy systems) have been converted to organic farming since 2004. I have characterized vegetation - established vegetation in field boundaries and in field centres, and vegetation in the soil seed bank - of permanent grasslands and arable fields with complementary approaches: taxonomical approach based on the species, and functional approach based on seven functional properties about dispersal, establishment and persistence of plant species. I have characterized field paths, along nine years, either from farming practices set up on field, either from annual characteristics of landscape mosaïc. I have represented this landscape mosaïc as a mosaïc of distinct land-uses. All of them and their spatialization have been determined from farmer surveys or landscape observations.My results show that soil seed bank and field bboundaries are not potential sources of plant species for field centres, in both permanent grasslands and arable fields. On the other hand, they are efficient refuges for a large part of grassland species. According to my results, I hypothesize that field boudaries are species sinks in arable fields. I also highlight that functional gradient of grassland vegetation in the field edge, between field margins and field centres, is spread until 2 m only.Finally, plant diversity in studied fields is mainly influenced by field path according landscape mosaïc and by farming practices set up the same year of vegetation sampling. Soil characteristics have a minor influence. These three groups of influent factors explain more than 75 % of the functional composition variability of the vegetation in field centres.The management of plant diversity in agricultural fields of a given farm can be partly reach by the farmer. However, according to the effects of field paths about landscape mosaïc, it is necessary to set up a collective management of plant diversity with all actors sharing the studied territory