Orientador: Hércules de Araújo Feitosa / Banca: Maria Cláudia Cabrini Grácio / Banca: Ítala Maria Loffredo D’Ottaviano / Resumo: Em 1999, Grácio introduziu a Lógica do Plausível como uma particularização de uma família de sistemas lógicos, caracterizados pela inclusão de um quantificador generalizado na sintaxe da lógica clássica de predicados, a saber, as Lógicas Moduladas, cuja formalização semântica é dada por um subconjunto do conjunto das partes do universo. Nesta particularização de lógica modulada, é incluído o quantificador do Plausível P, que engendra a formalização de um raciocínio indutivo de maneira que "uma 'boa parte' dos indivíduos possui determinada propriedade". O presente trabalho introduz um novo sistema dedutivo para a Lógica do Plausível, denominado TLP, construído seguindo os princípios de tableaux semânticos clássicos. Na elaboração do sistema de tableaux TLP, há uma forma original de localizar pontos nos ramos de um dado tableau. Ademais, por meio do raciocínio indutivo engendrado por esta lógica, discussões sucederam acerca da indução ser considerada um processo genuinamente lógico, tendo por ponto de partida o problema epistemológico da indução. / Abstract: The Logic of the Plausible was introduced in 1999 by Grácio as a particularization of a family of logical systems characterized by the inclusion of a generalized quantifier in the syntax of the classical logic of predicates, denominated the Modulated Logics, whose semantical interpretation is given by a subset of the power set of the universe. In this particularization of modulated logics, it is included the quantifier of Plausible P that engenders the formalization of a type of inductive reasoning so that "a 'good' number of individuals possesses certain property ". This work introduces a new deductive system for the Logic of the Plausible, denominated TLP, built according to the principles of the classical semantical tableaux. In the construction of the tableaux system TLP, an original form of locating points in the branches of any tableaux is presented. Besides, through the inductive reasoning engendered by this logic, the work also promotes discussions concerning the consideration of the induction as a genuinely logical process, beginning from the epistemological problem of the induction. / Mestre

Cette thèse se divise en trois parties. Dans l'introduction, nous rappelons d'abord les problèmes et les motivations philosophiques a l'origine de l'étude des logiques polyvalentes. Nous élaborons une methode qui permet d'obtenir mécaniquement a partir de la définition matricielle d'une logique, des règles d'inférence pour les connecteurs propositionnels d'un calcul des tableaux. Un traitement similaire est fait pour les règles d'inférence pour les quantificateurs. Le raffinement étudie alors est une skolemisation paresseuse. Elle permet l'utilisation de l'unification pour calculer les instances utiles a la construction d'un tableau ferme. Une implémentation dans atinf les concrétise. Nous proposons les logiques polyvalentes avec égalité graduelle, un calcul par resolution-paramodulation ordonnées. La première partie finit par une extension qui consiste a munir les valeurs de vérité de structures de treillis ou de treillis bi-dimensionnels. Au traitement systématique des logiques finies suit une étude de deux cas typiques de logiques polyvalentes infinies du premier ordre une étude systématique étant théoriquement impossible : les logiques de post et de Ukasiewicz. Le lien entre les logiques de Horn et les logiques de post est utilise, pour proposer une automatisation des logiques de post basée sur une sémantique des mondes possibles. A partir de cette sémantique nous définissons un calcul des tableaux préfixes. Afin d'augmenter l'efficacité, des contraintes, résolues en temps polynomial sur les préfixes sont introduites. Chaque développement inclut une étude bibliographique très documentée du domaine de la logique mathématique, de l'intelligence artificielle et de la déduction automatique

.

Le travail décrit dans cette thèse s'inscrit dans le contexte du développement et de la validation des systèmes réactifs synchrones. Il vise à tirer parti de certaines formes de structuration des programmes durant le processus de développement et de validation. Nous étudions premièrement l'utilisation d'opérateurs réguliers de types "itérateurs" qui permettent d'exprimer assez facilement des programmes réguliers manipulant des tableaux. Nous montrons aussi comment, au moment de la validation, on peut tirer partie de ces structures régulières pour rendre la preuve d'une propriété plus<br />simple. Nous nous intéressons ensuite à la spécification dite "par contrat" où un couple (assume, guarantee) est associé à chaque composant pour spécifier les hypothèses sur l'environnement et les<br />propriétés satisfaites par le composant sous ces hypothèses. Nous montrons l'intérêt de tels contrats à la fois en terme de spécification et de vérification pour le cas particulier des systèmes synchrones.<br />Nous proposons une série d'algorithmes de transformations de programmes (aussi bien autour de l'utilisation des itérateurs que des contrats) utilisable comme pre-processeur d'objectifs de preuve pour les outils de validation. Nos propositions, notamment sur l'aspect langage des itérateurs, ont répondu à des besoins rencontrés dans les applications industrielles, particulièrement autour du langage Lustre, auquel nous appliquons nos résultat. Ces propositions seront bientôt incluses dans la version industrielle du langage.

Dans leur environnement actuel, les hôpitaux se voient contraints de développer des outils d'évaluation de la performance, et ce principalement dans les secteurs à forte consommation de ressources et à forte valeur ajoutée comme, par exemple, les blocs opératoires. Notre apport est une méthodologie innovante destinée à réduire les lacunes existantes en termes d'évaluation de la performance hospitalière. Cette méthodologie combine une approche pratique avec un outil d'aide à la conception qui vise à générer un système global d'évaluation de la performance utilisable dans les blocs opératoires. Notre méthodologie comporte quatre grandes étapes : détermination de la stratégie et des objectifs, description des processus et identification des inducteurs de performance, définition des plans d'action, établissement des indicateurs de performance et conception des tableaux de bord. Grâce à une approche générique pratique, au respect des étapes de conception et aux outils de développement présentés, cette méthode donne aux gestionnaires de blocs opératoires la capacité de concevoir et de générer un système d'évaluation de la performance (indicateurs, tableaux de bord) qui convient à chaque contexte et répond aux exigences de chaque type d'organisation dans le domaine des soins de santé. Les différentes étapes de cette approche ont été appliquées à un cas réel dans un bloc opératoire de 8 salles. En rendant notre modèle compréhensible et facile à utiliser par les professionnels de la santé, notre collaboration avec les équipes du bloc opératoire et de la direction médicale ont conduit à une réelle appropriation des résultats par l'hôpital.

Si l'analyse automatique des accès aux tableaux a été largement étudiée, on trouve très peu de résultats convaincants sur l'analyse du contenu des tableaux. Pour une telle analyse, les analyses numériques sont centrales. Notamment, si l'on découvre l'invariant i ≠ j, on évite d'affaiblir la connaissance sur a[j] lors d'une affectation à a[i]. Nous proposons une nouvelle analyse numérique faiblement relationnelle, combinant des contraintes de zones (x - y ≤ c ou ±x ≤ c) à des contraintes de non-égalités (x ≠ y ou x ≠ 0). Cette analyse a une complexité en O(n4), si les variables prennent leur valeurs dans un ensemble dense. Dans le cas arithmétique, décider de la satisfaisabilité d'une conjonction de telles contraintes est un problème NP-complet. Nous proposons une analyse en O(n4) également pour ce cas. Au cœur des analyses du contenu des tableaux on trouve aussi des analyses de partitionnement symbolique. Pour une boucle " for i = 1 to n ", où un tableau est accédé à la cellule i, il est nécessaire de considérer le contenu des tableaux sur les tranches [1, i - 1], [i, i] et [i + 1, n] pour être précis. Nous définissons une analyse de partitionnement sémantique, puis une analyse du contenu des tableaux basée sur ses résultats. Cette dernière associe à chaque tranche φ une propriété ψ dont les variables représentent le contenu des tableaux sur cette tranche. La propriété ψ est interprétée cellule-par-cellule, ainsi pour φ = [1, i - 1] et ψ = (a = b + 1) il est exprimé que ∀ k ∈ [1, i - 1], a[k] = b[k] + 1. Les résultats expérimentaux montrent que notre analyse automatique est efficace et précise, sur une classe de programmes simples : tableaux unidimensionnels, indexés par une variable au plus (x + c ou c), traversés par des boucles, imbriquées ou non, avec des compteurs suivant une progression arithmétique. Elle découvre par exemple que le résultat d'un tri par insertion est un tableau trié, ou que durant le parcours d'un tableau gardé par une "sentinelle", tous les accès à ce tableau sont corrects.

Pour modéliser le fonctionnement d'un système, décrire une situation ou représenter des idées, on se met intuitivement à dessiner des bulles et les lier par des flèches sous forme de graphes étiquetés. Les logiques modales constituent un cadre formel expressif et extensible qui permet de définir ces graphes sous forme de « modèles », et d'exprimer certaines propriétés de ces graphes sous forme de « formules » afin de pouvoir raisonner là-dessus: model checking, test de satisfiabilité ou de validité, etc. Pour des formules et modèles de tailles importantes, ces tâches deviennent compliquées. De ce fait, un outil permettant de les réaliser automatiquement s'avère nécessaire. LoTREC en est un exemple. Il permet à son utilisateur de créer sa propre méthode de preuve, grâce à un langage simple et de haut niveau, sans avoir besoin d'aucune expertise spécifique en programmation. Durant ma thèse, j'ai revu le travail qui était déjà accompli dans LoTREC et j'ai apporté de nouvelles extensions qui s'avéraient nécessaires pour pouvoir traiter de nouvelles logiques (K.alt1, universal modality, Hybrid Logic HL(@),Intuitionistic logic, Public Announcement Logic, ...) et offrir à l'utilisateur certaines nouvelles techniques. D'autre part, j'ai examiné les origines de LoTREC dans le monde de réécriture de graphes et j'ai spécifié la sémantique de son moteur de réécriture. Cela a permis d'éclaircir comment l'on peut hériter dans nos méthodes de preuve des résultats et des propriétés théoriques déjà bien établies dans le domaine de la réécriture de graphes.

A partir de l'identification des 3 hypothèses que sont l'information imparfaite, l'asymétrie informationnelle et la rationalité limitée, la science économique a du profondément modifier la représentation et l'explication des phénomènes économiques du modèle standard. Ce mouvement a concerné à la fois la vision des marchés et celle de la firme. A partir de la notion de « firme processeur d'information » qui est celle largement retenue dans l'orthodoxie néo-classique ou apparentée, cette thèse propose de penser l'articulation entre organisation, information et pouvoir. Afin de dépasser la double tradition en économie qui consiste soit à postuler le pouvoir (approche des radicaux), soit à le nier (courant néo-classique), une démarche pragmatique essaie d'aller chercher en dehors des frontières de l'économie des modèles susceptibles de donner des pistes de représentation du pouvoir intra-organisationnel. Ce choix est renforcé par les travaux de micro-économie contemporain qui mobilisent eux-mêmes des travaux d'inspiration « sociologique » et qui permettent de penser l'introduction du pouvoir dans les modèles de al théorie standard. Cette démarche aboutit au choix d'une définition opérationnelle du pouvoir ouvrant la voie à une quantification de l'organisation. Celle-ci est menée en utilisant la théorie des graphes d'influence, qui allie la représentation topologique de la théorie des graphes au calcul matriciel de la méthodologie input-output. Les indicateurs qu'elle fournit sont calculés dans le cadre de l'étude d'une organisation concrète. La base de données est construite à partir des flux d'échange de mails. Ils fournissent une caractérisation assez fine de l'organisation en distinguant notamment le niveau global du niveau local. Ils permettent également de discuter de l'articulation entre la structure formelle et la structure informelle. <br />Finalement sur la base de trois définitions des notions d'organisation, d'information et de pouvoir, élaborées à partir d'une large revue de la littérature en économie des organisations, cette thèse propose des indicateurs permettant de déterminer qui a le pouvoir dans une organisation concrète définie comme une structure d'échanges d'informations.

Rapport de stage diplôme de conservateur des bibliothèques : Bibliothéconomie : Villeurbanne, ENSSIB : 2003.

Mémoire d'étude DCB : Ecole nationale supérieure des sciences de l'information et des bibliothèques : 2003.