Au coeur des liens entre Théorie de la Démonstration et Théorie des Types, la correspondance de Curry-Howard fournit des termes de preuves aux aspects calculatoires et équipés de théories équationnelles, i.e. des notions de normalisation et d'équivalence. Cette thèse contribue à étendre son cadre à des formalismes (comme le calcul des séquents) appropriés à des considérations d'ordre logique comme la recherche de preuve, à des systèmes expressifs dépassant la logique propositionnelle comme des théories des types, et aux raisonnements classiques plutôt qu'intuitionistes.<br />La première partie est intitulée Termes de Preuve pour la Logique Intuitioniste Implicationnelle, avec des contributions en déduction naturelle et calcul des séquents, normalisation et élimination des coupures, sémantiques en appel par nom et par valeur. En particulier elle introduit des calculs de termes de preuve pour le calcul des séquents depth-bounded G4 et la déduction naturelle multiplicative. Cette dernière donne lieu à un calcul de substitutions explicites avec affaiblissements et contractions, qui raffine la beta-réduction.<br />La deuxième partie, intitulée Théorie des Types en Calcul des Séquents, développe une théorie des Pure Type Sequent Calculi, équivalents aux Systèmes de Types Purs mais mieux adaptés à la recherche de preuve.<br />La troisième partie, intitulée Vers la Logique Classique, étudie des approches à la Théorie des Types classique. Elle développe un calcul des séquents pour une version classique du Système Fomega. Une approche à la question de l'équivalence de preuves classiques consiste à calculer les représentants canoniques de preuves équivalentes dans le cadre du Calcul des Structures.

Reproduction de : Habilitation à driger des recherches : Sciences mathématiques. Informatique : Lille 1 : 2005. / N° d'ordre (Lille 1) : 494. Titre provenant de la page de titre du document numérisé. Bibliogr. p. 87-95. Liste des publications.

Alors que la question des dynamiques de cluster est relativement peu considérée dans la littérature économique, les modèles de cluster font référence à différents niveaux de coordination et d'adaptabilité au changement. Cependant, la difficulté de considérer les clusters industriels dans leur environnement fait que ce modèle d'organisation industrielle reste assimilé à un bassin d'attraction, compte tenu de l'homogénéisation des caractéristiques de ses membres. Pour dépasser cette approche ad hoc, notre contribution vise à caractériser les dynamiques de cluster afin d'obtenir une meilleure compréhension de ce modèle en termes de performance (dynamiques de coopération et de concurrence) et d'inscription sociale et territoriale (encastrement structurel et relationnel). Nous analysons, au travers de la littérature sur les proximités, les modalités de coordination des acteurs des clusters en vue de la construction d'actifs spécifiques localisés. Il est argumenté que deux logiques relationnelles co-évolutives sont à l'origine des dynamiques des clusters : portées par des stratégies de court terme comme la résolution de problèmes communs selon une logique professionnelle ; et la construction de relations de long terme comme des alliances patrimoniales, renforçant l'encastrement entre les acteurs, selon une logique historique. Cela nous permet de considérer de manière jointe les deux perspectives temporelles de la stratégie des membres d'un cluster (recherche de flexibilité, pérennisation des activités) et leurs dynamiques d'interaction (renforcement de l'encastrement, découplage). Un modèle de simulation en vie artificielle nous permet d'évaluer les conséquences de l'adoption des deux stratégies sur les clusters : structure du réseau et formes d'encastrement induites, ainsi que les performances individuelle et collective de leurs membres. Nous appliquons le cadre théorique construit à l'analyse du pôle de compétitivité du végétal spécialisé de la Région Pays-de-la-Loire.

Le sepsis est un syndrome observé chez des patients associant une infection documentée (microbiologiquement ou cliniquement suspectée) à une réponse inflammatoire systémique (Systemic Inflammatory Response Syndrome : SIRS).Celui-ci peut évoluer vers un sepsis sévère s'il est associé à la défaillance d'un ou de plusieurs organes. Le choc septique est l'association d'un état septique grave et d'une défaillance hémodynamique caractérisée par une chute aiguë de la pression artérielle ne pouvant pas être corrigée par une procédure standard de remplissage vasculaire. Les syndromes septiques sont aujourd'hui la première cause de mortalité en unités de réanimation. Cette mortalité élevée, en particulier pour les cas les plus graves tels que les chocs septiques, témoigne d'une absence de traitements curatifs pour cette pathologie. Partant de l'hypothèse que les syndromes septiques graves sont la conséquence d'une perte de contrôle précoce de la régulation de la réponse inflammatoire, nous avons étudié, via deux démarches complémentaires, l'initiation de la voie de signalisation TLR4 et les mécanismes intracellulaires contribuant à sa régulation. Dans un premier temps, l'utilisation d'approches transcriptomiques nous a permis d'identifier la voie de signalisation mTOR comme discriminante entre des patients sains (SIRS induit par l'injection d'endotoxines) et des patients souffrant de syndromes septiques graves. Nous avons ensuite développé et utilisé des techniques de modélisation logique pour simuler in silico le rôle joué par la voie mTOR dans la résolution d'une réponse inflammatoire. Ces résultats encourageants ouvrent des perspectives pour de nouvelles applications thérapeutiques dans le domaine du sepsis / Sepsis is a syndrome observed in patients combining a documented infection (microbiologically or clinically suspected) with a systemic inflammatory response (Systemic Inflammatory Response Syndrome : SIRS). It may progress to severe sepsis if it is associated with failures of one or more organs. Septic shock is the combination of a severe sepsis and a hemodynamic dysfunction characterized by an acute fall in blood pressure that cannot be corrected by a procedure of vascular filling.Sepsis syndromes represent today the first cause of mortality in intensive care units around the world. This poor survival rate, in particular for the most severe cases, such as septic shock, testifies a real curative therapeutic demand.Based on the assumption that severe sepsis syndromes are the consequence of a loss of control in early mechanisms of inflammatory response regulation, we studied via two complementary approaches the initiation of TLR4 signaling pathway and the intracellular mechanisms contributing to its regulation.First, the use of transcriptomic approaches allowed us to identify the mTOR signaling pathway as discriminating between healthy patients (SIRS induced by the infusion of endotoxins) and patients with severe septic syndromes. We then developed and used logic modeling approaches to in silico simulate the role played by the mTOR signaling pathway in the resolution of an inflammatory response. These encouraging results open perspectives for new therapeutic applications in the field of sepsis

La logique Here-and-there (HT) est une logique monotone à trois valeurs, intermédiaire entre les logiques intuitionniste et classique. La logique de l'équilibre est un formalisme non-monotone dont la sémantique est donnée par un critère de minimalisation sur les modèles de la logique HT. Ce formalisme est fortement lié à la programmation orientée ensemble réponse (ASP), un paradigme relativement nouveau de programmation déclarative. La logique de l'équilibre constitue la base logique de l'ASP: elle reproduit la sémantique par ensemble réponse des programmes logiques et étend la syntaxe de l'ASP à des théories propositionnelles plus générales, i.e., des ensembles finis de formules propositionnelles. Cette thèse traite aussi bien des logiques modales sous-jacentes à la logique de l'équilibre que de ses extensions modales. Ceci nous permet de produire un cadre complet pour l'ASP et d'examiner de nouveau la base logique de l'ASP. A cet égard, nous présentons d'abord une logique modale monotone appelée MEM et capable de caractériser aussi bien l'existence d'un modèle de la logique de l'équilibre que la relation de conséquence dans ces modèles. La logique MEM reproduit donc la propriété de minimalisation qui est essentielle dans la définition des modèles de la logique de l'équilibre. Nous définissons ensuite une extension dynamique de la logique de l'équilibre. Pour ce faire, nous étendons le langage de la logique HT par deux ensembles de programmes atomiques qui permettent de mettre à jour, si possible, les valeurs de vérité des variables propositionnelles. Ces programmes atomiques sont ensuite combinés au moyen des connecteurs habituels de la logique dynamique. Le formalisme résultant est appelé logique Here-and-there dynamique (D-HT) et permet la mise-à-jour des modèles de la logique de l'équilibre. Par ailleurs, nous établissons un lien entre la logique D-HT et la logique dynamique des affectations propositionnelles (DL-PA): les affectations propositionnelles mettent à vrai ou à faux les valeurs de vérité des variables propositionnelles et transforment le modèle courant comme en logique dynamique propositionnelle. En conséquence, DL-PA constitue également une logique modale sous-jacente à la logique de l'équilibre. Au début des années 1990, Gelfond avait défini les spécifications épistémiques (E-S) comme une extension de la programmation logique disjonctive par des notions épistémiques. L'idée de base des E-S est de raisonner correctement à propos d'une information incomplète au moyen de la notion de vue-monde dans des situations où la notion précédente d'ensemble réponse n'est pas assez précise pour traiter le raisonnement de sens commun et où il y a une multitude d'ensembles réponses. Nous ajoutons ici des opérateurs épistémiques au langage original de la logique HT et nous définissons une version épistémique de la logique de l'équilibre. Cette version épistémique constitue une nouvelle sémantique non seulement pour les spécifications épistémiques de Gelfond, mais aussi plus généralement pour les programmes logiques épistémiques étendus. Enfin, nous comparons notre approche avec les sémantiques existantes et nous proposons une équivalence forte pour les théories de l'E-HT. Ceci nous conduit naturellement des E-S aux ASP épistémiques et peut être considéré comme point de départ pour les nouvelles extensions du cadre ASP. / Here-and-there (HT) logic is a three-valued monotonic logic which is intermediate between classical logic and intuitionistic logic. Equilibrium logic is a nonmonotonic formalism whose semantics is given through a minimisation criterion over HT models. It is closely aligned with answer set programming (ASP), which is a relatively new paradigm for declarative programming. To spell it out, equilibrium logic provides a logical foundation for ASP: it captures the answer set semantics of logic programs and extends the syntax of answer set programs to more general propositional theories, i.e., finite sets of propositional formulas. This dissertation addresses modal logics underlying equilibrium logic as well as its modal extensions. It allows us to provide a comprehensive framework for ASP and to reexamine its logical foundations. In this respect, we first introduce a monotonic modal logic called MEM that is powerful enough to characterise the existence of an equilibrium model as well as the consequence relation in equilibrium models. The logic MEM thus captures the minimisation attitude that is central in the definition of equilibrium models. Then we introduce a dynamic extension of equilibrium logic. We first extend the language of HT logic by two kinds of atomic programs, allowing to update the truth value of a propositional variable here or there, if possible. These atomic programs are then combined by the usual dynamic logic connectives. The resulting formalism is called dynamic here-and-there logic (D-HT), and it allows for atomic change of equilibrium models. Moreover, we relate D-HT to dynamic logic of propositional assignments (DL-PA): propositional assignments set the truth values of propositional variables to either true or false and update the current model in the style of dynamic epistemic logics. Eventually, DL-PA constitutes an alternative monotonic modal logic underlying equilibrium logic. In the beginning of the 90s, Gelfond has introduced epistemic specifications (E-S) as an extension of disjunctive logic programming by epistemic notions. The underlying idea of E-S is to correctly reason about incomplete information, especially in situations when there are multiple answer sets. Related to this aim, he has proposed the world view semantics because the previous answer set semantics was not powerful enough to deal with commonsense reasoning. We here add epistemic operators to the original language of HT logic and define an epistemic version of equilibrium logic. This provides a new semantics not only for Gelfond's epistemic specifications, but also for more general nested epistemic logic programs. Finally, we compare our approach with the already existing semantics, and also provide a strong equivalence result for EHT theories. This paves the way from E-S to epistemic ASP, and can be regarded as a nice starting point for further frameworks of extensions of ASP.

Ce travail contient une investigation sur la théorie phénoménologique de la signification. L'idée-clé du projet est d'expliquer la constitution de la signification au moyen des analyses de l'intentionnalité. Nous avons étudié différents actes intentionnels qui fonctionnent dans l'expression et dans la construction des significations. Nous avons étudié à cet égard, d'abord, l'acte d'expression primordiale, dans lequel le contenu d'une intuition est élevé au domaine de l'idéal, puis les actes de synthèse catégorielle, dans lesquels d'autres significations se constituent en absence de leur propre intuition. Nous avons puis étudié les effets de la théorie de la signification à la conception de la logique pure. En conséquence, nous avons discuté que la sémantique dialogique est un cadre adéquat, selon le phénoménologie, pour interpréter le raisonnement logique et pour expliquer la signification des constantes logiques. Nous avons également discuté la signification de certains connecteurs logiques, et leurs formalisations, en utilisant notre méthode phénoménologique-dialogique. / This work contains an investigation on the phenomenological theory of meaning. The key idea of the project is to explain the constitution of the meaning by means of the analyses of the intentionality. We have investigated different intentional acts which are functioning in expression and in constructing the meanings. In this regard we have studied, first, the act of primordial expression, in which a content of an intuition is raised to the realm of the ideal, and then the acts of categorial synthesis, in which further meanings are constituted in the absence of their proper intuition. We have investigated the effects of the theory of meaning to the conception of pure logic. Dialogical semantic is shown to be an adequate framework to interpret logical reasoning and to explain the meaning of the logical constants as well. We have also discussed the meaning of some logical connectives, and their formalizations, using our phenomenologico-dialogical method.

Doctorat en philosophie et lettres / info:eu-repo/semantics/nonPublished

Montréal Trigonix inc. 2018

L’auteur entreprend dans ce mémoire de faire une présentation des débats axiologiques de philosophie de la logique sous-jacents à la controverse opposant Frege et Hilbert sur les fondements de la géométrie. Contre le parti pris philosophique selon lequel la logique est une discipline achevée, l’auteur entreprend une mise en contexte des positions de Frege et Hilbert afin de montrer que dans leur conception de la logique se trouvent des paradigmes incommensurables, résultant de l’influence de traditions philosophiques et scientifiques diverses. Dans cette perspective, Frege est le défenseur de la vision traditionnelle de la logique comme medium universel de la science, tel qu’incarnée dans la géométrie euclidienne. La logique symbolique de Frege est ainsi vue comme la mise en oeuvre de moyens raffinés pour lutter contre la (( perversion des sciences )) ayant lieu au 19ième siècle et pour la défense de la vision traditionnelle de la science. à l’opposé, l’approche métathéorique de Hilbert représente la conception moderne dite algébrique de la logique telle que développée au 19ième sous l’influence des métamathématiques, et certains rapprochements avec les conceptions (( model-theoretic )) et catégorielles de la logique viennent appuyer cette thèse. / This memoir presents some axiological debates of philosophy of logic underlying the Frege-Hilbert controversy on the foundations of geometry. Against the philosophical bias according to which logic is an achieved discipline, a contextualized presentation of the respective positions of Frege and Hilbert is done in order to show that incommensurable paradigms are found in their view of logic, that is due to the influence of various philosophical and scientific traditions. From this standpoint, Frege is the defender of the traditionalist view of logic as the universal medium of science, as embodied in Euclidean geometry. In this perspective, Frege’s symbolic logic is seen as the achievement of a refined means to counter the 19th-century perversion of science with the purpose of defending the traditional conception of the role of science. On the other hand, Hilbert’s metatheoretical approach represents the so-called algebraic modern conception of logic as developed in the 19th century under the influence of metamathematics. Following this, parallels between Hilbert’s approach and the model-theoretical and categorical conceptions of logic are drawn to show their proximity.

No description available.