Στην διπλωματική εργασία παρουσιάζεται μια νέα δομή δεδομένων ειδικά σχεδιασμένη για δίκτυα μεταφορών ευρείας κλίμακας τα οποία αλλάζουν δυναμικά. Η νέα δομή δεδομένων γραφημάτων μας παρέχει ταυτόχρονα τρία μοναδικά χαρακτηρισ τικά: 1. Σύμπτυξη(Compactness): ικανότητα να προσπελάσει αποδοτικά διαδοχικές κορυφές και ακμές, μια απαίτηση όλων των αλγορίθμων γραφημάτων). 2. Ευκινησία (Agility): ικανότητα να αλλάξει και να ρυθμίσει εξαρχής την εσωτερική της διάταξη με σκοπό να βελτιώσει την τοπικότητα των αναφορών των στοιχείων, σύμφωνα με έναν δεδομένο αλγόριθμο. 3. Δυναμικότητα (Dynamicity): ικανότητα να ενθέσει ή να διαγράψει αποδοτικά κορυφές και ακμές. Όλες οι προηγούμενες γνωστές δομές γραφημάτων δεν υποστήριζαν τουλάχιστον ένα από τα προηγούμενα χαρακτηριστικά ή/και δεν μπορούσαν να εφαρμοστούν σε δυναμικά δίκτυα μεταφορών ευρείας κλίμακας. Σε αυτή τη διπλωματική εργασία, παρουσιάζεται η πρακτικότητα της νέας δομής γραφημάτων εκτελώντας μια εκτενή πειραματική μελέτη για δρομολόγηση συντομότερων διαδρομών σε Ευρωπαϊκά οδικά δίκτυα ευρείας κλίμακας με μερικές δεκάδες εκατομμύρια κορυφές και ακμές. Χρησιμοποιώντας κλασικούς αλγόριθμους εύρεσης συντομότερων διαδρομών, επιτυγχάνονται εύκολα χρόνοι ερωτημάτων από μια αρχική κορυφή σε μια τελική κορυφή της τάξης των milliseconds, ενώ η νέα δομή γραφημάτων μας μπορεί να ενημερωθεί σε μόλις μερικά microseconds μετά από μια ένθεση ή διαγραφή μιας κορυφής ή ακμής. / We present a new graph data structure specifically suited for large scale transportation networks in dynamic scenario. Our graph data structure provides tree unique characteristics, namely compactness, agility and dynamicity. All previous data structures were lacking support in at least one of the aforementioned characteristics. We demonstrate the practicality of the new graph data structure by conducting experiments on large scale European road networks, achieving query times of classical routing algorithms in the order of milliseconds and update times in the order of a few microseconds.

Alors que la complexité des fonctions d'ordre 1 est bien définie et étudiée, il n'existe pas de notion satisfaisante à tout ordre. Une telle théorie existe déjà à l'ordre 2 et permet de définir une classe analogue aux fonctions calculables en temps polynomial usuelles. Cela est tout particulièrement intéressant dans le domaine de l'analyse récursive où l'on peut représenter, entre autres, les nombres et les fonctions réelles par des fonctions d'ordre 1. On peut alors remarquer un lien fort entre calculabilité et continuité, et aussi rapprocher la complexité avec certaines propriétés analytiques, ce que nous illustrons dans le cas des opérateurs réels. Nous prouvons cependant que, du point de vue de la complexité, les fonctions d'ordre 1 ne permettent pas de représenter fidèlement certains espaces mathématiques. Ce résultat appuie tout particulièrement la nécessité d'une théorie de la complexité d'ordre supérieur. Nous développons alors un modèle de calcul basé sur la sémantique des jeux, où l'application de deux fonctions est représentée par la confrontation de deux stratégies dans un jeu. En définissant la taille de telles stratégies, nous pouvons déduire une notion robuste et pertinente de complexité pour ces stratégies et donc pour les fonctions d'ordre supérieur. Nous définissons aussi une classe de fonctions calculables en temps polynomial qui paraît être un bon candidat pour définir une classe de complexité raisonnable à tout ordre / While first order complexity is well defined and studied, higher order lacks a satisfactory notion of complexity. Such a theory already exists at order 2 and provides a complexity class analogue to usual polynomial time computable functions. This is already especially interesting in the domain of computable analysis, where real numbers or real functions for example can be represented by first order functions. In particular, there is a clear link between computability and continuity, and we also illustrate in the case of real operators that complexity can be related to some analytical properties. However, we prove that, from a complexity point of view, some mathematical spaces can not be faithfully represented by order 1 functions and require higher order ones. This result underlines that there is a need to develop a notion of complexity at higher types which will be, in particular but not only, useful to computable analysis. We have developed a computational model for higher type sequential computations based on a game semantics approach, where the application of two functions is represented by the game opposing two strategies. By defining the size of such strategies, we are able to define a robust and meaningful notion of complexity at all types, together with a class of polynomial time computable higher order functionals which seems to be a good candidate for a class of feasible functionals at higher types

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'étude non destructive du bois à partir de scanners à rayons X nécessite d’imaginer de nouvelles solutions adaptées à l'analyse des images. Préoccupation à la fois de la recherche agronomique et du milieu industriel des scieries, la segmentation des nœuds de bois est un défi majeur en termes de robustesse aux spécificités de chaque espèce et aux conditions d'acquisition des images. Les travaux menés dans cette thèse permettent de proposer un processus de segmentation en deux phases. Il isole d'abord chaque nœud dans une zone réduite puis segmente le nœud unique de chaque zone. Les solutions proposées pour chaque phase permettent d'intégrer les connaissances sur l'organisation interne du tronc et les mécanismes inhérents à sa croissance, à travers des outils classiques du traitement et de l'analyse d'image. La première phase repose en grande partie sur un principe de détection du mouvement emprunté à l'analyse vidéo et revisité. Deux approches de segmentation sont ensuite proposées, considérant pour l'une les coupes tomographiques initiales, et pour l'autre de nouvelles coupes ré-échantillonnées pour chaque nœud, orthogonalement à sa trajectoire. L'intégralité du processus a été implémenté dans un logiciel dédié aussi bien à l'expérimentation et la validation de l'approche qu'aux échanges interdisciplinaires. Le support applicatif du bois souligne la capacité de spécialisation des algorithmes génériques du traitement et de l'analyse d'image, et la pertinence de l'intégration de connaissances a priori dans cette optique / The non-destructive study of wood from X-Ray CT scanners requires to imagine new solutions adapted to analysis of images. Relating both agronomic research and industrial sector of sawmills, segmentation of wood knots is a major challenge in terms of robustness to specificities of each species and to image acquisition conditions. The works carried out in this thesis allow to propose a segmentation process in two phases. It first isolates each knot in a reduced area then it segments the unique knot of each area. Proposed solutions for each phase allow to integrate knowledges about internal organization of trunk and mechanisms inherent to its growth, through classical tools of image analysis and processing. The first phase is essentially based on a movement detection principle borrowed from video analysis and revisited. Two segmentation approaches are then proposed, considering for one the initial CT slices and for the other news slices resampled for each knot orthogonally to its trajectory. The complete process has been implemented in a software dedicated both for experimentation and validation of approach, and to interdisciplinary dialogs. The applicative support of wood emphasizes the specialization abilities of generic image analysis and processing algorithms, and the relevance to integrate priori knowledges in this perspective

Dans cette thèse, nous nous concentrons sur le développement des méthodes d'optimisation pour résoudre certaines classes de problèmes d'apprentissage avec la parcimonie et/ou avec l'incertitude des données. Nos méthodes sont basées sur la programmation DC (Difference of Convex functions) et DCA (DC Algorithms) étant reconnues comme des outils puissants d'optimisation. La thèse se compose de deux parties : La première partie concerne la parcimonie tandis que la deuxième partie traite l'incertitude des données. Dans la première partie, une étude approfondie pour la minimisation de la norme zéro a été réalisée tant sur le plan théorique qu'algorithmique. Nous considérons une approximation DC commune de la norme zéro et développons quatre algorithmes basées sur la programmation DC et DCA pour résoudre le problème approché. Nous prouvons que nos algorithmes couvrent tous les algorithmes standards existants dans le domaine. Ensuite, nous étudions le problème de la factorisation en matrices non-négatives (NMF) et fournissons des algorithmes appropriés basés sur la programmation DC et DCA. Nous étudions également le problème de NMF parcimonieuse. Poursuivant cette étude, nous étudions le problème d'apprentissage de dictionnaire où la représentation parcimonieuse joue un rôle crucial. Dans la deuxième partie, nous exploitons la technique d'optimisation robuste pour traiter l'incertitude des données pour les deux problèmes importants dans l'apprentissage : la sélection de variables dans SVM (Support Vector Machines) et le clustering. Différents modèles d'incertitude sont étudiés. Les algorithmes basés sur DCA sont développés pour résoudre ces problèmes. / In this thesis, we focus on developing optimization approaches for solving some classes of optimization problems in sparsity and robust optimization for data uncertainty. Our methods are based on DC (Difference of Convex functions) programming and DCA (DC Algorithms) which are well-known as powerful tools in optimization. This thesis is composed of two parts: the first part concerns with sparsity while the second part deals with uncertainty. In the first part, a unified DC approximation approach to optimization problem involving the zero-norm in objective is thoroughly studied on both theoretical and computational aspects. We consider a common DC approximation of zero-norm that includes all standard sparse inducing penalty functions, and develop general DCA schemes that cover all standard algorithms in the field. Next, the thesis turns to the nonnegative matrix factorization (NMF) problem. We investigate the structure of the considered problem and provide appropriate DCA based algorithms. To enhance the performance of NMF, the sparse NMF formulations are proposed. Continuing this topic, we study the dictionary learning problem where sparse representation plays a crucial role. In the second part, we exploit robust optimization technique to deal with data uncertainty for two important problems in machine learning: feature selection in linear Support Vector Machines and clustering. In this context, individual data point is uncertain but varies in a bounded uncertainty set. Different models (box/spherical/ellipsoidal) related to uncertain data are studied. DCA based algorithms are developed to solve the robust problems

Dans la société moderne, le stress s’avère un problème omniprésent. Un stress permanent peut entraîner divers problèmes mentaux et physiques notamment pour des personnes confrontées à des situations d'urgence comme par exemple des pompiers en intervention: il peut modifier leurs actions et les mettre en danger. Par conséquent, dans ce contexte, il est pertinent de chercher à évaluer le stress de la personne. Sur la base de cette idée, a été proposé le projet Psypocket qui vise à concevoir un système portable capable d'analyser précisément l'état de stress d'une personne en fonction de ses modifications physiologiques, psychologiques et comportementales, puis de proposer des solutions de rétroaction pour réguler cet état. Cette thèse s’inscrit dans le cadre du projet Psypocket. Nous y discutons de la faisabilité et de l'intérêt de la reconnaissance du stress à partir de données hétérogènes. Non seulement les signaux physiologiques, tels que l'électrocardiographie (ECG), l'élecchtromyographie (EMG) et l'activité électrodermale (EDA), mais aussi le temps de réaction (RT) sont adoptés pour discriminer différents états de stress d'une personne. Pour cela nous proposons une approche basée sur un classifieur SVM (Machine à Vecteurs de Support). Les résultats obtenus montrent que le temps de réaction peut-être un moyen d’estimation du niveau de stress de l’individu en complément ou non des signaux physiologiques. En outre, nous discutons de la faisabilité d'un système embarqué à même de réaliser la chaîne globale de traitement des signaux. Cette thèse contribue donc à la conception d’un système portable de reconnaissance du stress d'une personne en temps réel en adoptant des données hétérogènes, en l’occurrence les signaux physiologiques et le temps de réaction / In modern society, the stress of an individual has been found to be a common problem. Continuous stress can lead to various mental and physical problems and especially for the people who always face emergency situations (e.g., fireman): it may alter their actions and put them in danger. Therefore, it is meaningful to provide the assessment of the stress of an individual. Based on this idea, the Psypocket project is proposed which is aimed at making a portable system able to analyze accurately the stress state of an individual based on his physiological, psychological and behavioural modifications. It should then offer solutions for feedback to regulate this state.The research of this thesis is an essential part of the Psypocket project. In this thesis, we discuss the feasibility and the interest of stress recognition from heterogeneous data. Not only physiological signals, such as Electrocardiography (ECG), Electromyography (EMG) and Electrodermal activity (EDA), but also reaction time (RT) are adopted to recognize different stress states of an individual. For the stress recognition, we propose an approach based on a SVM classifier (Support Vector Machine). The results obtained show that the reaction time can be used to estimate the level of stress of an individual in addition or not to the physiological signals. Besides, we discuss the feasibility of an embedded system which would realize the complete data processing. Therefore, the study of this thesis can contribute to make a portable system to recognize the stress of an individual in real time by adopting heterogeneous data like physiological signals and RT

Une Fonction Latticielle Polynômiale (FLP) sur un treillis L est une fonction p : Ln → L, qui peut être exprimée à partir de variables, de constantes et des opérateurs de treillis ∧ et ∨ . Dans les cas où L est distributif et borné, les FLP incluent les intégrales de Sugeno. Celles-ci sont des fonctions d'agrégation qui permettent de fusionner des valeurs sur des échelles ordinales non numériques, et qui sont utilisées notamment dans l'approche qualitative de l'Aide à la Décision Multi Critères en tant qu'alternatives ordinales aux intégrales de Choquet. Dans une première partie, nous traitons la tâche d'interpolation par des FLP, c'est à dire : pour un treillis L, un sous-ensemble fini D de Ln et une fonction f : D → L, retourner une FLP p : Ln → L telle que p(x) = f(x) pour tout x ∊ D (si une telle FLP existe). Nous traitons successivement le cas où L est un treillis fini et le cas où L est une treillis distributif borné. Dans les deux cas, nous donnons des algorithmes qui résolvent ce problème en temps polynomial. Dans une seconde partie, nous abordons les généralisations des intégrales de Sugeno appelées Fonctions d'Utilité de Sugeno (FUS), qui permettent la fusion de valeurs appartenant à des échelles ordinales différentes, ainsi que leur application à la tâche de classification monotone. Nous introduisons un modèle composé de plusieurs FUS, ainsi qu'un algorithme d'apprentissage d'un tel modèle. Nous comparons ce modèle aux ensembles de règles de décision appris par VC-DomLEM, et étudions le nombre de FUS nécessaires afin de modéliser des données empiriques / A Lattice Polynomial Function (LPF) over a lattice L is a map p : Ln → L that can be defined by an expression involving variables, constants and the lattice operators ∧ and ∨. If L is a distributive lattice, these maps include the so-called Sugeno integrals that are aggregation functions capable of merging ordinal values, not necessarily numerical. They are widely used in the qualitative approach to Multiple Criteria Decision Aiding (MCDA), and they can be thought of as the ordinal counterparts of Choquet integrals. In the first part of this thesis, we tackle the task of interpolating a partial function by an LPF, stated as follows: for a lattice L, a finite subset D of Ln, and a function f : D → L, return an LPF p : Ln → L such that p(x) = f(x) for all x ∊ D (if such an LPF exists). We treat the cases where L is a finite lattice, and then the cases where L is a bounded distributive lattice. In both cases, we provide algorithms that solve this problem in polynomial time. In the second part, we consider generalizations of Sugeno integrals in the multi-attribute setting, in particular, the Sugeno Utility Functions (SUFs), that are able to merge values coming from different ordinal scales. We consider the their use in monotonic classification tasks. We present a model based on a set of SUFs and an algorithm for learning such model from data. We compare this model to the sets of monotonic decision rules learned by VC-DomLEM, and study the number of SUFs that are required in order to model empirical data

Nous étudions dans ce mémoire les propriétés des ensembles de pavages engendrés par des jeux de tuiles de Wang exhibant une ou plusieurs directions de déterminisme local, en accordant une importance toute particulière aux jeux déterministes dans les quatre directions diagonales simultanément, dits 4-way déterministes. Après avoir proposé une construction alternative d’un jeu de tuiles apériodique 4-way déterministe, nous étudions plusieurs problèmes de décision sur ces objets et complétons en particulier le résultat d’indécidabilité du problème du pavage dans le cadre 4-way déterministe établi par Lukkarila en montrant l’indécidabilité du problème du pavage périodique 4-way déterministe. Nous montrons également que des familles complexes de coloriages du plan telles que celles engendrées par les substitutions restent sofiques dans un cadre 4-way déterministe. Nous proposons une bi-déterminisation des constructions de jeux de tuiles point-fixe de Durand, Romashchenko et Shen et en tirons quelques premières applications. Enfin, nous considérons l’opportunité d’élargir le rayon de la règle locale de déterminisme afin de limiter les directions d’expansivité et ainsi de permettre la construction localement déterministe de systèmes de particules et collisions non triviaux. Nous introduisons un nouveau modèle syntaxique commode afin de travailler à rayon deux et revisitons des problématiques de Lukkarila dans ce cadre. / In this thesis, we study some properties of the sets of tilings generated by Wang tilesets that exhibit one or more directions of local determinism, focusing in particular on tilesets that are simultaneously deterministic in the four diagonal directions, referred to as 4-way deterministic. After having exposed an alternative construction of a 4-way deterministic aperiodic tileset, we study several decision problems on these objects and complete in particular Lukkarila’s result of undecidability of the Domino Problem in the 4-way deterministic setting proving the undecidability of the 4-way deterministic periodic Domino Problem. We also prove that some complex families of colorings of the plane such that those generated by substitutions remain sofic in the 4-way deterministic setting. We propose a bi-determinization of the constructions by Durand, Romashchenko and Shen of fixed-point tilesets and give some first applications. Finally, we investigate the idea of extending the radius of the local rule of determinism in order to reduce the set of directions of expansiveness and thus allow the local realization of non-trivial particles and collisions systems. We introduce a new and convenient syntactic model to deal with radius two and revisit some of Lukkarila’s problems in this setting.

Nous considérions des modèles à espace d'état où les observations sont multicatégorielles et longitudinales, et l'état est décrit par des modèles du type CHARN. Nous estimons l'état au moyen des récursivités de Kalman généralisées. Celles-ci reposent sur l'application d'une variété de filtres particulaires et de l’algorithme EM. Nos résultats sont appliqués à l'estimation du trait latent en qualité de vie. Ce qui fournit une alternative et une généralisation des méthodes existantes dans la littérature. Ces résultats sont illustrés par des simulations numériques et une application aux données réelles sur la qualité de vie des femmes ayant subi une opération pour cause de cancer du sein / We consider state space models where the observations are multicategorical and longitudinal, and the state is described by CHARN models. We estimate the state by generalized Kalman recursions, which rely on a variety of particle filters and EM algorithm. Our results are applied to estimating the latent trait in quality of life, and this furnishes an alternative and a generalization of existing methods. These results are illustrated by numerical simulations and an application to real data in the quality of life of patients surged for breast cancer

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