L'idée de l'argumentation est de rechercher dans une base de connaissances, pour chaque proposition dont on souhaite évaluer la validité, les raisons qui étayent cette proposition et celles qui l'infirment. Un argument est alors entendu comme une paire comprenant une proposition et les raisons qui la justifient. Notre propos est d'offrir des outils formels pour la génération automatique d'arguments par deux agents en situation de dialogue. Ces outils reposent sur les X-logiques, formalisme non-monotone proposé en 1996 par Siegel et Forget et déterminant un cadre fondateur autour de la notion de preuve pour le raisonnement non-monotone. En particulier l'ensemble X servant à paramétrer la relation d'inférence confère une souplesse inégalée à la gestion dynamique des arguments. Après un tour d'horizon des travaux passés en matière de représentations logiques pour l'argumentation, nous introduisons les X-logiques, à partir desquelles est composée la notion d'attitude d'un agent par rapport à une formule. Nous définissons ensuite des opérateurs de confrontation qui permettent d'associer des ensembles de formules aux attitudes d'un agent. Le concept de réponse d'un agent à un ensemble de formules est alors élaboré en tant que motivation de l'attitude de cet agent vis-à-vis de l'ensemble en question. Plusieurs formes de réponses sont distinguées parmi lesquelles les notions de réponse pertinente ou encore de mensonge. Une réponse représente les raisons qui justifient la conclusion d'un argument : c'est à partir du calcul de ces réponses que nous exhibons une procédure de génération automatique d'arguments. Enfin nous montrons que notre cadre argumentatif permet de générer les contre-arguments conservatifs maximaux de Besnard et Hunter (2001), arguments retenus pour leur pertinence.

La symétrie est par définition un concept multidisciplinaire. Il apparaît dans de nombreux domaines. En général, elle revient à une transformation qui laisse invariant un objet. Le problème de satisfaisabilité (SAT) occupe un rôle central en théorie de la complexité. Il est le problème de décision de référence de la classe NP-complet (Cook, 71). Il consiste à déterminer si une formule CNF admet ou non une valuation qui la rend vraie. Dans la première contribution de ce mémoire, nous avons introduit une nouvelle méthode complète qui élimine toutes les symétries locales pour la résolution du problème SAT en exploitant son groupe des symétries. Les résultats obtenus montrent que l'exploitation des symétries locales est meilleure que l'exploitation des symétries globales sur certaines instances SAT et que les deux types de symétries sont complémentaires, leur combinaison donne une meilleure exploitation.En deuxième contribution, nous proposons une approche d'apprentissage de clauses pour les solveurs SAT modernes en utilisant les symétries. Cette méthode n'élimine pas les modèles symétriques comme font les méthodes statiques d'élimination des symétries. Elle évite d'explorer des sous-espaces correspondant aux no-goods symétriques de l'interprétation partielle courante. Les résultats obtenus montrent que l'utilisation de ces symétries et ce nouveau schéma d'apprentissage est profitable pour les solveurs CDCL.En Intelligence Artificielle, on inclut souvent la non-monotonie et l'incertitude dans le raisonnement sur les connaissances avec exceptions. Pour cela, en troisième et dernière contribution, nous avons étendu la notion de symétrie à des logiques non classiques (non-monotones) telles que les logiques préférentielles, les X-logiques et les logiques des défauts.Nous avons montré comment raisonner par symétrie dans ces logiques et nous avons mis en évidence l'existence de certaines symétries dans ces logiques qui n'existent pas dans les logiques classiques. / Symmetry is by definition a multidisciplinary concept. It appears in many fields. In general, it is a transformation which leaves an object invariant. The problem of satisfiability (SAT) is one of the central problems in the complexity theory. It is the first decision Np-complete problem (Cook, 71). It deals with determining if a CNF formula admits a valuation which makes it true. First we introduce a new method which eliminates all the local symmetries during the resolution of a SAT problem by exploiting its group of symmetries. Our experimental results show that for some SAT instances, exploiting local symmetries is better than exploiting just global symmetries and both types of symmetries are complementary. As a second contribution, we propose a new approach of Conflict-Driven Clause Learning based on symmetry. This method does not eliminate the symmetrical models as the static symmetry elimination methods do. It avoids exploring sub-spaces corresponding to symmetrical No-goods of the current partial interpretation. Our experimental results show that using symmetries in clause learning is advantageous for CDCL solvers.In artificial intelligence, we usually include non-monotony and uncertainty in the reasoning on knowledge with exceptions. Finally, we extended the concept of symmetry to non-classical logics that are preferential logics, X-logics and default logics. We showed how to reason by symmetry in these logics and we prove the existence of some symmetries in these non-classical logics which do not exist in classical logics.