La modélisation et la spécification de systèmes distribués nécessitent une adaptation des modèles logiques utilisés pour leur représentation. Les notions<br />d'emplacements et de ressources jouent notamment un rôle centrale dans la représentation de ces systèmes.<br /><br />On propose tout d'abord à la proposition d'une première logique, la logique linéaire distribuée et mobile (DMLL) qui intègre les notions de distribution et de mobilité. On propose également une sémantique à la Kripke et un calcul des séquents supportant l'élimination des coupures pour cette logique.<br /><br />Cette première étude a mis en avant le rôle centrale de la sémantique pour la modélisation de systèmes distribués. On propose alors la structure des arbres de ressources, des arbres dont les noeuds possèdent des labels et contiennent des ressources appartenant à<br />monoïde partiel de ressources et BI-Loc, une logique pour raisonner sur ces arbres, un langage permettant de modifier les arbres et son axiomatisation correcte et complète sous forme de triplets de Hoare. Concernant BI-Loc, on détermine des conditions suffisantes pour décider de la satisfaction et de la validité par model-checking et on développe une méthode de preuves fondée sur les tableaux sémantiques correcte et complète.<br /><br />On montre comment on peut raisonner sur les tas de pointeurs grâce aux arbres de ressources. Enfin, on détermine comment le modèle des arbres partiel peut être utilisé pour représenter et spécifier les données<br />semi-structurées et raisonner sur la transformation de ce type de données.

Cette thèse se situe dans le domaine des modèles de l’argumentation en intelligence artificielle. Ces modèles constituent des outils très populaires pour l’étude de raisonnements en présence d’incohérences dans les bases de connaissances et lors de la négociation entre agents et la prise de décision. Un modèle argumentatif est un processus interactionnel principalement basé sur la construction d’arguments et de contre-arguments, l’étude des relations entre ces différents arguments et la mise en place de critères permettant de déterminer le statut de chaque argument afin de sélectionner les arguments (les plus) acceptables.Dans ce cadre, ce travail a porté sur l’étude d’un système particulier : le système d’argumentation déductif. Un argument est alors entendu comme un couple prémisses-conclusion tel que la conclusion soit une formule qui puisse être déduite des prémisses. Nous y avons traité plusieurs questions. Tout d’abord, partant du constat que le raisonnement par l’absurde est valide en logique propositionnelle classique, nous proposons une méthode de génération d’arguments en faveur d’une proposition donnée. Cette approche s’étend au calcul des undercuts canoniques, arguments identifiés comme représentant tous les contre-arguments. Contrairement aux autres approches proposées dans la littérature, notre technique est complète au sens où elle permet de générer, modulo une possible explosion combinatoire, tous les arguments relatifs à une formule logique quelconque. Ensuite, nous avons proposé un cadre d’argumentation en logique conditionnelle. Les logiques conditionnelles sont souvent considérées comme étant tout particulièrement adaptées à la formalisation de raisonnements de nature hypothétique. Leur connecteur conditionnel est en effet souvent plus proche de l’intuition que l’on peut avoir de l’implication que ne l’est l’implication matérielle de la logique propositionnelle classique. Ceci nous permet de proposer un concept de contrariété conditionnelle qui couvre à la fois les situations de conflits logiques fondés sur l’incohérence et une forme particulière de conflit qui ne se traduit pas naturellement par un conflit basé sur l’incohérence : quand un agent affirme une règle de type Si alors, une seconde règle qui peut en être déduite et qui impose la satisfaction de prémisses supplémentaires peut apparaître conflictuelle. Nous étudions alors sur cette base les principaux éléments d’une théorie de l’argumentation dans une logique conditionnelle. Enfin, le dernier point étudié dans ce travail concerne le raisonnement au sujet de ressources consommables, dans un cadre où les formules logiques sont elles mêmes consommées dans le processus déductif. Nous proposons une logique, simple et proche du langage et des principes de la logique propositionnelle classique, permettant le raisonnement à partir de ressources consommables et de quantité bornée. Nous y revisitons également les principaux éléments d’une théorie logique de l’argumentation. / This thesis focus on the field of argumentation models in artificial intelligence. These models form very popular tools to study reasoning under inconsistency in knowledge bases, negotiation between agents, and also in decision making. An argumentative model is an interactional process mainly based on the construction of arguments and counter-arguments, then studying the relations between these arguments, and finally the introduction of some criteria to identifying the status of each argument in order to select the (most) acceptable of them.In this context, this work was dealt with the study of a particular system: the deductive argumentation framework. An argument is then understood as a pair premises-conclusion such that conclusion is a logical formula entailed by premises, a non-ordered collection of logical formulas. We have addressed several issues. First of all, on the basis that reductio ad absurdum is valid in classical propositional logic, we propose a method to compute arguments for a given statement. This approach is extended to generate canonical undercuts, arguments identified as the representative of all counter-arguments. Contrary to the other approaches proposed in the literature, our technique is complete in the sense that all arguments relative to the statement at hand are generated and so are all relevant counter-arguments. Secondly, we proposed a logic based argumentation in conditional logic. Conditional logic is often regarded as an appealing setting for the formalization of hypothetical reasoning. Their conditional connective is often regarded as a very suitable connective to encode many implicative reasoning patterns real-life and attempts to avoid some pitfalls of material implication of propositional logic. This allows us to put in light and encompass a concept of conditional contrariety thats covers both usual inconsistency-based conflict and a specific form of conflict that often occurs in real-life argumentation: i.e., when an agent asserts an If then rule, it can be argued that the satisfaction of additional conditions are required for the conclusion of a rule to hold. Then, in that case we study the main foundational concepts of an argumentation theory in conditional logic. Finally, the last point investigated in this work concerns the reasoning about bounded resources, within a framework in which logical formulas are themselves consumed in the deductive process. First, a simple variant of Boolean logic is introduced, allowing us to reason about consuming resources. Then, the main concepts of logic-based argumentation are revisited in this framework.

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

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