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.

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