Orientador: Prof. Dr. André Ricardo Oliveira da Fonseca / Dissertação (mestrado) - Universidade Federal do ABC, Programa de Pós-Graduação em Mestrado Profissional em Matemática em Rede Nacional, 2014. / Este trabalho busca chamar a atenção para a necessidade do uso da formalização matemática como etapa a se cumprir na aprendizagem do conceito de função para o Ensino Médio, sendo este o principal objetivo. O problema da pesquisa constitui-se em: qual a necessidade do ensino ser contextualizado e a relevância da evolução histórica de conceitos, culminando na necessidade do uso da formalização matemática para o ensino de funções. Este estudo fundamenta-se em BOYER (1974), FIORENTIN (1994), SCHREINER (2004), MACIEL (2011), CARAÇA (1951), LOBEIRO (2000), LIMA (2005, 2006, 2012), FERREIRA (2013), COSTA (1971), DAVIS (1986). Esta pesquisa tem caráter qualitativo e utiliza como instrumentos: questionários para seis voluntários, sendo metade deles oriundos de escola pública ainda cursando o 2 o ano do Ensino Médio e os demais, de escola privada e já cursando o 1 o semestre do Ensino Superior. Aula direcionada baseada nos dados colhidos a partir dos questionários e como última etapa do processo, enquete sobre o reconhecimento da importância da formalização matemática. Os resultados apontam para uma preocupação com a qualidade das aulas ministradas sobre funções, de maneira que a formalização deva ser trabalhada de modo consistente, equilibrada, e principalmente, provida de significado ao educando. Em síntese o ponto inicial para o sucesso é uma alfabetização matemática de qualidade, promovendo situações de desafios e estímulos que facilitem o uso de abstrações. Sendo fundamental a qualificação e aperfeiçoamento dos professores de todos os níveis de ensino. / This work seeks to call attention to the need of the use of the mathematical formalization as a phase to go through the learning of the concept of function for secondary school (High School), being this its main goal. The problem of the research lies in: what the need of the contextualized teaching is and the relevance of the historical evolution of concepts, culminating on the need of the use of the mathematical formalization for the teaching of functions. This study is based on BOYER (1974), FIORENTINI (1974), SCHREINER (2004), MACIEL ( 2011), CARAÇA (1951), LOBEIRO (2000), LIMA (2005, 2006, 2012), FERREIRA (2013), COSTA (1971), DAVIS (1986). This research has a qualitative character and utilizes as instruments: questions for six volunteers, being half of them public school still coursing the 2nd year of High School and the others, from private school and already in the first semester of college or university. Directed class based on the data picked from the questions and as the last phase in the process, a survey about the acknowledgement of the importance of the mathematical formalization. The results point to a concern with the quality of the classes ministrated on functions, so that the formalization should be worked in a consistent, balanced way, and mainly provided with the meaning to the learner. Summing up, the start to success is a qualified mathematical literacy, promoting situations of challenges and stimuli which facilitate the use of abstractions. Being fundamental the qualificaon and perfectioning of teachers in all levels of teaching.

The formalization of Rural Family Farming (RFF) is understood here as a complex process‟, because it is suit industry standards an activity that once served as household value and whose features handmade become valued by consumers as differentiated products for industrial products. The literature suggests that the viability of this possibility marketing involves the organization of farmers, with the action of different actors, to promote cooperation among stakeholders. It is characterized, therefore, an economic phenomenon that is inserted‟ in a context of internal social relations family, but also relationships that constitute the external actors with expertise, for specific socio-spatial to the issue. These are variables that make up the institutional environment in which RFF are immersed and shape the study of the problem that arises in order to understand how Rural Family Farming are formalized, featuring actors and the relationships that are established to overcome the adversities that the institutional environment exerts on those experiences. Thus, this study aims to analyze the dynamics inherent in the formalization of Rural Family Farming, trying to understand the contribution of the actors to overcome adversity related to the institutional environment. The theoretical orientation of the research is located predominantly in the tradition of the New Economic Sociology. We used the method of comparative study of cases‟, the analytical units are located in the municipalities of Jaguari-RS and Chapecó-SC. Data collection was conducted from secondary sources (bibliographies and databases), but mostly from primary sources (interviews, documents and free observation) with farmers and the actors with whom they relate on the basis of projects of RFF, using specific instruments (scripts semi-structured) for each category. We used a qualitative approach, supported occasionally by quantitative methods (frequency distribution), where the organization of the information collected was to enable the analysis of content, supporting the interpretations based on the theoretical framework presented. The results call into question the effectiveness of the ways in which family farming is organized and is represented, as well as their own support services to overcome barriers to the institutional environment (especially with regard to the requirements of the existing legal framework) imposes on projects of family farming. The study suggests that advances in potential do not occur by the individual action of farmers, either by deterministic State action, but as a construction carried out by farmers' organizations, supported decisively by their forms of representation, by organizations of social movements and the government. / A formalização das Agroindústrias Familiares Rurais (AFRs) é compreendida aqui como um processo complexo‟, pois se trata de adequar a padrões de mercado uma atividade que outrora servira como valor de uso doméstico e cujas características artesanais passam a ser valorizadas pelos consumidores como produtos diferenciados dos produtos industriais. A literatura aponta que a viabilização dessa possibilidade mercadológica envolve a organização dos agricultores, com a ação de diferentes atores, no sentido de promover a cooperação entre os envolvidos. Fica caracterizado, com isso, um fenômeno econômico que ocorre inserido‟ em um contexto de relações sociais internas a família, mas também de relações que se constituem com atores externos às experiências, conferindo especificidade socioespacial à problemática. Essas são variáveis que compõem o ambiente institucional em que as AFRs estão imersas e configuram o problema do estudo que se coloca de modo a compreender como as Agroindústrias Familiares Rurais são formalizadas, caracterizando os atores e as relações que se estabelecem para superar as adversidades que o ambiente institucional exerce sobre essas experiências. Diante disso, este estudo se propõe a analisar a dinâmica inerente à formalização das Agroindústrias Familiares Rurais, buscando compreender a contribuição dos atores para superar adversidades relacionadas ao ambiente institucional. A orientação teórica da pesquisa está situada, predominantemente, na tradição da Nova Sociologia Econômica. Foi utilizado o método de estudo comparativo de casos‟, cujas unidades de análise localizam-se nos municípios de Jaguari-RS e Chapecó-SC. A coleta de dados foi conduzida a partir de fontes secundárias (bibliografias e bases de dados), mas principalmente de fontes primárias (entrevistas, documentos e observação livre) com agricultores(as) e os atores com os quais estes se relacionam em função dos projetos de AFRs, empregando instrumentos específicos (roteiros semi-estruturados) para cada categoria. Utilizou-se de abordagem qualitativa, apoiada pontualmente por métodos quantitativos (distribuição de frequências), onde a organização das informações coletadas ocorreu de modo a permitir a análise de conteúdo, subsidiando as interpretações à luz do marco teórico proposto. Os resultados colocam em xeque a eficácia das formas pelas quais a agricultura familiar se organiza e é representada, assim como dos próprios serviços de apoio, na superação de barreiras que o ambiente institucional (sobretudo no que diz respeito às exigências do quadro legal vigente) impõe aos empreendimentos da agricultura familiar. O estudo sugere que avanços em potenciais não ocorram pela ação individual dos agricultores, tampouco pela ação determinista do Estado, mas como uma construção protagonizada pelas organizações de agricultores, apoiadas de maneira decisiva por suas formas de representação, pelas organizações dos movimentos sociais e pelo poder público.

Le langage mathématique courant et les langages mathématiques formelssont très éloignés. Par <<langage mathématique courant>> nousentendons la prose que le mathématicien utilise tous les jours dansses articles et ses livres. C'est une langue naturelle avec desexpressions symboliques et des notations spécifiques. Cette langue està la fois flexible et structurée mais reste sémantiquementintelligible par tous les mathématiciens.Cependant, il est très difficile de formaliser automatiquement cettelangue. Les raisons principales sont: la complexité et l'ambiguïté deslangues naturelles en général, le mélange inhabituel entre languenaturelle et notations symboliques tout aussi ambiguë et les sautsdans le raisonnement qui sont pour l'instant bien au-delà descapacités des prouveurs de théorèmes automatiques ou interactifs.Pour contourner ce problème, les assistants de preuves actuelsutilisent des langages formels précis dans un système logique biendéterminé, imposant ainsi de fortes restrictions par rapport auxlangues naturelles. En général ces langages ressemblent à des langagesde programmation avec un nombre limité de constructions possibles etune absence d'ambiguïté.Ainsi, le monde des mathématiques est séparé en deux, la vastemajorité qui utilise la langue naturelle et un petit nombre utilisantaussi des méthodes formelles. Cette seconde communauté est elle-mêmesubdivisée en autant de groupes qu'il y a d'assistants de preuves. Onperd alors l'intelligibilité des preuves pour tous les mathématiciens.Pour résoudre ce problème, on peut se demander:est-il possible d'écrire un programme qui comprend la langue naturellemathématique et qui la traduit vers un langage formel afin depermettre sa validation?Ce problème se subdivise naturellement en deux sous-problèmes tous lesdeux très difficiles:1. l'analyse grammaticale des textes mathématiques et leur traductiondans un langage formel,2. la validation des preuves écrites dans ce langage formel.Le but du projet MathNat (Mathematics in controlled Natural languages)est de faire un premier pas pour répondre à cette question trèsdifficile, en se concentrant essentiellement sur la première question.Pour cela, nous développons CLM (Controlled Language for Mathematics)qui est un sous-ensemble de l'anglais avec une grammaire et un lexiquerestreint, mais qui inclut tout de même quelques ingrédientsimportants des langues naturelles comme les pronoms anaphoriques, lesréférences, la possibilité d'écrire la même chose de plusieursmanières, des adjectifs distributifs ou non, ...Le second composant de MathNath est MathAbs (Mathematical Abstractlanguage). C'est un langage formel, indépendant du choix d'un systèmelogique permettant de représenter la sémantique des textes enpréservant leur structure et le fil du raisonnement. MathAbs est conçucomme un langage intermédiaire entre CLM et un système logique formelpermettant la vérification des preuves.Nous proposons un système qui permet de traduire CLM vers MathAbsdonnant ainsi une sémantique précise à CLM. Nous considèrons que cetravail est déjà un progrès notable, même si pour l'instant on estloin de pouvoir vérifier formellement toutes les preuves en MathAbsainsi générées.Pour le second problème, nous avons réalisé une petite expérience entraduisant MathAbs vers une liste de formules en logique du premierordre dont la validité garantit la correction de la preuve. Nous avonsensuite essayé de vérifier ces formules avec des prouveurs dethéorèmes automatiques validant ainsi quelques exemples. / There is a wide gap between the language of mathematics and itsformalized versions. The term "language of mathematics" or"mathematical language" refers to prose that the mathematician uses inauthoring textbooks and publications. It mainly consists of naturallanguage, symbolic expressions and notations. It is flexible,structured and semantically well-understood by mathematicians.However, it is very difficult to formalize it automatically. Some ofthe main reasons are: complex and rich linguistic features of naturallanguage and its inherent ambiguity; intermixing of natural languagewith symbolic mathematics causing problems which are unique of itskind, and therefore, posing more ambiguity; and the possibility ofcontaining reasoning gaps, which are hard to fill using the currentstate of art theorem provers (both automated and interactive).One way to work around this problem is to abandon the use of thelanguage of mathematics. Therefore in current state of art of theoremproving, mathematics is formalized manually in very precise, specificand well-defined logical systems. The languages supported by thesesystems impose strong restrictions. For instance, these languages havenon-ambiguous syntax with a limited number of possible syntacticconstructions.This enterprise divides the world of mathematics in two groups. Thefirst group consists of a vast majority of mathematicians whose relyon the language of mathematics only. In contrast, the second groupconsists of a minority of mathematicians. They use formal systems suchas theorem provers (interactive ones mostly) in addition to thelanguage of mathematics.To bridge the gap between the language of mathematics and itsformalized versions, we may ask the following gigantic question:Can we build a program that understands the language of mathematicsused by mathematicians and can we mechanically verify its correctness?This problem can naturally be divided in two sub-problems, both very hard:1. Parsing mathematical texts (mainly proofs) and translating thoseparse trees to a formal language after resolving linguistic issues.2. Verification of this formal version of mathematics.The project MathNat (Mathematics in controlled Natural language) aimsat being the first step towards solving this problem, focusing mainlyon the first question.First, we develop a Controlled Language for Mathematics (CLM) which isa precisely defined subset of English with restricted grammar anddictionary. To make CLM natural and expressive, we support some richlinguistic features such as anaphoric pronouns and references,rephrasing of a sentence in multiple ways and the proper handling ofdistributive and collective readings.Second, we automatically translate CLM to a system independent formaldescription language (MathAbs), with a hope to make MathNat accessibleto any proof checking system. Currently, we translate MathAbs intoequivalent first order formulas for verification.

Submitted by Fabio Sobreira Campos da Costa (fabio.sobreira@ufpe.br) on 2016-08-08T13:11:15Z No. of bitstreams: 2 license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) tese.pdf: 4855618 bytes, checksum: 717d268b142705bdc8ce106731a257db (MD5) / Made available in DSpace on 2016-08-08T13:11:15Z (GMT). No. of bitstreams: 2 license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) tese.pdf: 4855618 bytes, checksum: 717d268b142705bdc8ce106731a257db (MD5) Previous issue date: 2016-03-28 / CAPEs / Proof assistants are software-based tools that are used in the mechanization of proof construction and validation in mathematics and computer science, and also in certified program development. Different such tools are being increasingly used in order to accelerate and simplify proof checking, and the Coq proof assistant is one of the most known and used. Language and automata theory is a well-established area of mathematics, relevant to computer science foundations and information technology. In particular, context-free language theory is of fundamental importance in the analysis, design and implementation of computer programming languages. This work describes a formalization effort, using the Coq proof assistant, of fundamental results of the classical theory of context-free grammars and languages. These include closure properties (union, concatenation and Kleene star), grammar simplification (elimination of useless symbols, inaccessible symbols, empty rules and unit rules), the existence of a Chomsky Normal Form for context-free grammars and the Pumping Lemma for context-free languages. To achieve this, several steps had to be fulfilled, including (i) understanding of the characteristics, importance and benefits of mathematical formalization, specially in computer science, (ii) familiarization with the underlying mathematical theories used in proof assistants, (iii) familiarization with the Coq proof assistant, (iv) review of the strategies used in the informal proofs of the main results of the context-free language theory and finally (iv) selection and adequation of the representation and proof strategies adopted in order the achieve the desired objectives. The result is an important set of libraries covering the main results of context-free language theory, with more than 500 lemmas and theorems fully proved and checked. This is probably the most comprehensive formalization of the classical context-free language theory in the Coq proof assistant done to the present date, and includes the remarkable result that is the formalization of the Pumping Lemma for context-free languages. The perspectives for the further development of this work are diverse and can be grouped in three different areas: inclusion of new devices and results, code extraction and general enhancements of its libraries. / Assistentes de prova são ferramentas de software que são usadas na mecanização da construção e da validação de provas na matemática e na ciência da computação, e também no desenvolvimento de programas certificados. Diferentes ferramentas estão sendo usadas de forma cada vez mais frequente para acelerar e simplificar a verificação de provas, e o assistente de provas Coq é uma das mais conhecidas e utilizadas. A teoria de linguagens e de autômatos é uma área bem estabelecida da matemática, com relevância para os fundamentos da ciência da computação e a tecnologia da informação. Em particular, a teoria das linguagens livres de contexto é de fundamental importância na análise, no projeto e na implementação de linguagens de programação de computadores. Este trabalho descreve um esforço de formalização, usando o assistente de provas Coq, de resultados fundamentais da teoria clássica das gramáticas e linguagens livres de contexto. Estes incluem propriedades de fechamento (união, concatenação e estrela de Kleene), simplificação gramatical (eliminação de símbolos inúteis, de símbolos inacessíveis, de regras vazias e de regras unitárias), a existência da Forma Normal de Chomsky para gramáticas livres de contexto e o Lema do Bombeamento para linguagens livres de contexto. Para alcançar estes resultados, diversas etapas precisaram ser cumpridas, incluindo (i) o entendimento das características, da importância e dos benefícios da formalização matemática, especialmente na ciência da computação, (ii) a familiarização com as teorias matemáticas fundamentais utilizadas pelos assistentes de provas, (iii) a familiarização com o assistente de provas Coq, (iv) a revisão das estratégias usadas nas provas informais dos principais resultados da teoria das linguagens livres de contexto e, finalmente, (v) a seleção e adequação das estratégias de representação e prova adotadas para permitir o alcance dos resultados pretendidos. O resultado é um importante conjunto de bibliotecas cobrindo os principais resultados da teoria das linguagens livres de contexto, com mais de 500 lemas e teoremas totalmente provados e verificados. Esta é provavelmente a formalização mais abrangente da teoria clássica das linguagens livres de contexto jamais feita no assistente de provas Coq, e inclui o importante resultado que é a formalização do Lema do Bombeamento para linguagens livres de contexto. As perspectivas para novos desenvolvimentos a partir deste trabalho são diversas e podem ser agrupadas em três áreas diferentes: inclusão de novos dispositivos e resultados, extração de código e aprimoramentos gerais das suas bibliotecas.

In their first meeting of the new millennium the UN Security Council put HIV/AIDS on the agenda as a security issue. This was the first time a non-traditional security issue was discussed in such a forum. Based upon the normative discussions raging within the field of securitization theory, this study seeks to analyse the empirical outcomes that the securitization effort, of putting HIV/AIDS on the Security Council agenda, might have had. While many studies argue the normative points of securitization when it comes to non-traditional security issues, this study turns to an empirical case. Based upon the resolution 1308, following the Security Council’s meeting, UNAIDS was chosen in order to uncover the possible outcomes of the securitization efforts. By using bureaucratic theory to develop a framework for the textual analysis of UNAIDS meeting documents from 1998-2005, this study uncovers undeniable changes to the nature and structure of the organization. The positive results yielded in the analysis of UNAIDS highlight that the use of securitization as a practical policy tool in to advance an issue at hand could well be a way forward with similar areas lacking sufficient attention and/or funding.

Nowadays, geoprocessing has moved in large parts from isolated desktop usage into the Web. Thereby, the overall availability of geoprocessing functionality has theoretically improved. Nevertheless, web-based geoprocessing functionality is still not readily available and usable as means to find and subsequently compare functionality are yet missing. Discoverability and exchangeability of geoprocessing functionality are limited, and the fundamental benefits of online usage are not fully exploited. To close this gap, this thesis defines a conceptualization with geooperators representing well-defined geoprocessing functionality, and categories representing distinct geooperator attributes as a starting point. Geooperators and categories are connected by associative and hierarchical links forming an interlinked network. The conceptualization serves as basis for two purposes: On the one hand, discovery of geooperators has to be improved. There is a multitude of different GIS users from varying backgrounds, all having a slightly different view on geoprocessing functionality. To embrace these varying views, several actually existing and established categorizations for geooperators are integrated into the conceptualization and structured hierarchically. Thus, multiple different perspectives on geooperators are enabled. The perspectives and the underlying categorizations are integrated into a geooperator browser serving as client that users can employ for discovery. The geooperator browser offers a faceted browsing interface based on the derived perspectives and categories. Several different search modes are offered and can be used simultaneously, thereby facilitating an improved discovery. On the other hand, to establish comparability and subsequently semantically interoperable exchangeability of geooperators, respective geooperator attributes are defined. Thereby, backend and provider independence of geoprocessing services is achieved. The conceptualization is formalized to allow for machine readability and processing which is required for usage in Spatial Data Infrastructures and the Semantic Web. The formalized conceptualization is labeled geooperator thesaurus. It is encoded by Semantic Web standards and offered in a Semantic Web compliant manner. The integration into geoprocessing service metadata is enabled by injecting semantic annotations that link to the respective concepts in the geooperator thesaurus. The thesaurus serves as the underlying data model for the geooperator browser. The thesis concludes with an outlook and discussions of future work. Foremost, the content of the geooperator thesaurus needs to be extended as it currently only comprises a representative subset of geooperators. An approach is suggested to involve the geoprocessing community as an important source of geoprocessing expertise in the maintenance and further development of the thesaurus. On a conceptual level, the thesaurus needs to be extended to a fully-fledged ontology including a formal geoprocessing algebra to support the creation of geooperator workflows. From a discovery point of view, the concept of geoprocessing patterns is outlined. Geoprocessing patterns list geooperators that are commonly used for certain geoprocessing tasks, and provide best practices about applying them in a meaningful manner and sequence. / An Stelle von isolierter Desktop-basierter Nutzung von Geoprozessierung werden heutzutage mehr und mehr webbasierte Angebote zur Verfügung gestellt. Dadurch hat sich die generelle Verfügbarkeit von Geoprozessierungsfunktionalität theoretisch verbessert. Da jedoch das Auffinden und anschließend oft notwendige Vergleichen von Funktionalität nur eingeschränkt möglich ist, können die Vorteile einer webbasierten Verfügbarkeit nicht vollständig genutzt werden. Um dieser Problematik zu begegnen, wird im Rahmen der vorliegenden Arbeit eine Konzeptualisierung entwickelt, die wohldefinierte Geoprozessierungsfunktionalität als Geooperatoren und Kategorien als Unterscheidungsmerkmale für Geooperatoren zur Verfügung stellt. Geooperatoren und Kategorien sind über assoziative und hierarchische Links zu einem Netzwerk verknüpft. Diese Konzeptualisierung erfüllt zwei grundlegende Aufgaben: Einerseits muss das Auffinden von Geooperatoren für Nutzer mit unterschiedlichsten Anwendungshintergründen möglich sein. Diese Nutzer haben unterschiedlichste Sichten auf Geooperatoren, die berücksichtigt und unterstützt werden sollen. Dazu werden etablierte Kategorisierungen aus Literatur und Praxis in die Konzeptualisierung integriert, entsprechend hierarchisch strukturiert und als Perspektiven auf Geooperatoren für den Zugriff nach Außen zur Verfügung gestellt. Diese Perspektiven und die darunterliegenden Kategorien werden als Facetten in einen Geooperatorbrowser integriert, der als webbasierter Client von den Nutzern für das Auffinden von Geooperatoren verwendet werden kann. Die explorative Suche über Facetten nach Geoprozessierungsfunktionalität wird durch eine Schlüsselwortsuche und einen geführten Suchmodus ergänzt und damit insgesamt die Auffindbarkeit von Geooperatoren verbessert. Andererseits sollen die Vergleichbarkeit und der anschließend semantisch interoperable Austausch von Geooperatoren ermöglicht werden. Dazu werden durch einen Vergleich von Geooperatorattributen Ähnlichkeiten von Geooperatoren definiert und zusammen mit der Konzeptualisierung als Geooperatorthesaurus formalisiert. Durch die Formalisierung wird eine Maschinenlesbarkeit und -prozessierbarkeit erreicht. Nur so kann ein anbieter- und backendunabhängiger Austausch von Geoprozessierungsdiensten in Geodateninfrastrukturen ermöglicht werden. Der Thesaurus nutzt Semantic-Web-Standards und wird in einer Semantic-Web-kompatiblen Art und Weise im Web publiziert. Die Integration in Metadaten von Geoprozessierungsdiensten wird durch semantische Annotationen erreicht, die auf die entsprechenden Konzepte im Thesaurus verlinken. Der Thesaurus dient als Datenbasis für den Geooperatorenbrowser. Die Arbeit schließt mit einem Ausblick auf und einer Diskussion von zukünftigen Forschungsarbeiten ab. Da der Thesaurus zurzeit nur eine repräsentative Menge an Beispieldaten enthält, muss als erster wichtiger Schritt der Inhalt des Thesaurus erweitert werden. Für die mittel- und langfristige Instandhaltung und Weiterentwicklung des Thesaurus wird ein Konzept zur Einbindung der GIS-Community vorgeschlagen, da hier gebündelte Geoprozessierungsexpertise vorhanden ist. Auf einer konzeptuellen Ebene muss der Thesaurus für eine semantisch und technisch verbesserte Verkettung von Geooperatoren zu einer vollständigen Ontologie mit einer formalen Geoprozessierungsalgebra weiterentwickelt werden. Für eine weitere Verbesserung der Auffindbarkeit von Geooperatoren wird das Konzept von Geoprozessierungspatterns skizziert, die Geooperatoren zusammenfassen, die oft im Kontext einer bestimmten Aufgabe zusammen genutzt werden. Zusätzlich werden über die Patterns Best Practices zur sinnvollen Anwendung und Verkettung der enthaltenen Geooperatoren zur Verfügung gestellt.

Les travaux de recherche présentés dans ce mémoire s’inscrivent dans le cadre de la valorisation des connaissances issues des expériences passées afin d’améliorer les performances des processus industriels. La connaissance est considérée aujourd'hui comme une ressource stratégique importante pouvant apporter un avantage concurrentiel décisif aux organisations. La gestion des connaissances (et en particulier le retour d’expérience) permet de préserver et de valoriser des informations liées aux activités d’une entreprise afin d’aider la prise de décision et de créer de nouvelles connaissances à partir du patrimoine immatériel de l’organisation. Dans ce contexte, les progrès des technologies de l’information et de la communication jouent un rôle essentiel dans la collecte et la gestion des connaissances. L’implémentation généralisée des systèmes d’information industriels, tels que les ERP (Enterprise Resource Planning), rend en effet disponible un grand volume d’informations issues des événements ou des faits passés, dont la réutilisation devient un enjeu majeur. Toutefois, ces fragments de connaissances (les expériences passées) sont très contextualisés et nécessitent des méthodologies bien précises pour être généralisés. Etant donné le potentiel des informations recueillies dans les entreprises en tant que source de nouvelles connaissances, nous proposons dans ce travail une démarche originale permettant de générer de nouvelles connaissances tirées de l’analyse des expériences passées, en nous appuyant sur la complémentarité de deux courants scientifiques : la démarche de Retour d’Expérience (REx) et les techniques d’Extraction de Connaissances à partir de Données (ECD). Le couplage REx-ECD proposé porte principalement sur : i) la modélisation des expériences recueillies à l’aide d’un formalisme de représentation de connaissances afin de faciliter leur future exploitation, et ii) l’application de techniques relatives à la fouille de données (ou data mining) afin d’extraire des expériences de nouvelles connaissances sous la forme de règles. Ces règles doivent nécessairement être évaluées et validées par les experts du domaine avant leur réutilisation et/ou leur intégration dans le système industriel. Tout au long de cette démarche, nous avons donné une place privilégiée aux Graphes Conceptuels (GCs), formalisme de représentation des connaissances choisi pour faciliter le stockage, le traitement et la compréhension des connaissances extraites par l’utilisateur, en vue d’une exploitation future. Ce mémoire s’articule en quatre chapitres. Le premier constitue un état de l’art abordant les généralités des deux courants scientifiques qui contribuent à notre proposition : le REx et les techniques d’ECD. Le second chapitre présente la démarche REx-ECD proposée, ainsi que les outils mis en œuvre pour la génération de nouvelles connaissances afin de valoriser les informations disponibles décrivant les expériences passées. Le troisième chapitre présente une méthodologie structurée pour interpréter et évaluer l’intérêt des connaissances extraites lors de la phase de post-traitement du processus d’ECD. Finalement, le dernier chapitre expose des cas réels d’application de la démarche proposée à des interventions de maintenance industrielle. / The research work presented in this thesis relates to knowledge extraction from past experiences in order to improve the performance of industrial process. Knowledge is nowadays considered as an important strategic resource providing a decisive competitive advantage to organizations. Knowledge management (especially the experience feedback) is used to preserve and enhance the information related to a company’s activities in order to support decision-making and create new knowledge from the intangible heritage of the organization. In that context, advances in information and communication technologies play an essential role for gathering and processing knowledge. The generalised implementation of industrial information systems such as ERPs (Enterprise Resource Planning) make available a large amount of data related to past events or historical facts, which reuse is becoming a major issue. However, these fragments of knowledge (past experiences) are highly contextualized and require specific methodologies for being generalized. Taking into account the great potential of the information collected in companies as a source of new knowledge, we suggest in this work an original approach to generate new knowledge based on the analysis of past experiences, taking into account the complementarity of two scientific threads: Experience Feedback (EF) and Knowledge Discovery techniques from Databases (KDD). The suggested EF-KDD combination focuses mainly on: i) modelling the experiences collected using a knowledge representation formalism in order to facilitate their future exploitation, and ii) applying techniques related to data mining in order to extract new knowledge in the form of rules. These rules must necessarily be evaluated and validated by experts of the industrial domain before their reuse and/or integration into the industrial system. Throughout this approach, we have given a privileged position to Conceptual Graphs (CGs), knowledge representation formalism chosen in order to facilitate the storage, processing and understanding of the extracted knowledge by the user for future exploitation. This thesis is divided into four chapters. The first chapter is a state of the art addressing the generalities of the two scientific threads that contribute to our proposal: EF and KDD. The second chapter presents the EF-KDD suggested approach and the tools used for the generation of new knowledge, in order to exploit the available information describing past experiences. The third chapter suggests a structured methodology for interpreting and evaluating the usefulness of the extracted knowledge during the post-processing phase in the KDD process. Finally, the last chapter discusses real case studies dealing with the industrial maintenance domain, on which the proposed approach has been applied.

Le véhicule autonome est un véhicule qui se conduira, à terme, sans aucune intervention du conducteur, quelle que soit la situation de conduite. Ce véhicule comprend une nouvelle fonction, nommée fonction AD, pour Autonomous Driving, en charge de la conduite autonome. Cette fonction peut se trouver dans des états différents (Active, Disponible par exemple) selon l'évolution des conditions environnementales. Le changement de ses états est géré par une fonction de Supervision, nommée Supervision AD. Le principal objet de ces travaux consiste à garantir que la fonction AD se trouve constamment dans un état sûr. Ceci revient à s'assurer que la Supervision AD respecte l'ensemble des exigences fonctionnelles et de sûreté qui spécifient son comportement. Ces deux types d'exigences sont émis par deux métiers distincts : l'Architecte Métier Système (AMS) et le pilote Sûreté de Fonctionnement (SdF). Ces deux disciplines d'ingénierie, bien qu'elles contribuent à la conception d'une même fonction, se distinguent en de nombreux points : objectifs, contraintes, planning, outils... Dans notre cas d'étude, ces différences s'illustrent par les exigences considérées : les exigences fonctionnelles sont allouées à la fonction AD globale, tandis que les exigences de sûreté spécifient le comportement de sous-fonctions locales redondantes assurant une continuité de service en cas de défaillance. La mise en cohérence de ces deux perspectives métier au plus tôt dans le cycle de conception et dans un contexte industriel, est la problématique centrale traitée. Les enjeux de SdF soulevés par le véhicule autonome rendent ce problème primordial pour les constructeurs automobiles. Afin de répondre à ces préoccupations, nous avons proposé une démarche outillée et collaborative de conception sûre de la Supervision AD. Cette démarche est intégrée dans les processus normatifs en vigueur (normes ISO 15288 et ISO 26262) ainsi que dans les processus de conception internes chez Renault. Elle est fondée sur la vérification formelle par model checking, la composition parallèle d'automates finis et l'expertise métier. Cette démarche prône l'utilisation d'un même formalisme (l'automate à états finis) par les deux métiers pour mener à bien des activités partageant un objectif de modélisation commun : la vérification d'exigences de comportement en phase amont de conception. Une méthode pour traduire les exigences en propriétés formelles et construire les modèles d'état a été déployée. Il en résulte une consolidation progressive des exigences traitées, initialement rédigées en langage naturel. Les potentielles ambigüités, incohérences et incomplétudes sont exhibées et traitées. / The Autonomous Vehicle is meant to drive itself, without any driver intervention, whatever the driving situation. This vehicle includes a new function, called AD, for Autonomous Driving, function. This function can be in different states (Available, Active for example) according to environmental conditions evolution. This states change is managed by a supervision function, named AD Supervision. The main goal of my works consists in guaranteeing that AD function remains always in a safe state. In other words, the AD Supervision must always respect all the functional and safety requirements that specify its behavior. These two requirements types are produced by two different professions: the System Architect (SA) and the Safety Engineer (SE). These two fields contribute to the design of the same function but distinguish at several aspects: objectives, constraints, planning, tools… In our case study, these differences are illustrated by considered requirements: the functional requirements are allocated to global AD function, while the safety requirements specify the behavior of local redundant sub-functions ensuring a continuous service in case of failure. The consistency of the two perspectives as early as possible in the design phase and in an industrial context, is the central problematic addressed. The safety issues due to Autonomous Vehicle make this topic essential for the automotive manufacturers. To meet these concerns, we proposed a tooled and collaborative approach for safe design of AD Supervision. This approach is integrated in the normative processes (standards ISO 26262 and ISO 15288) as well as in the internal design processes at Renault. It is based on formal verification by model checking, parallel composition of finite sate automata and technical expertise. This approach advocates the utilization of a same formalism (state automata) by the two professions to perform activities sharing a common goal: behavior requirements verification in preliminary design phase. A method to translate requirements into formal properties and to build state models has been deployed. The result is a progressive consolidation of treated requirements, initially expressed in free natural language. The potential ambiguities, inconsistencies and incompleteness are exhibited and treated. Two main contributions are in this way illustrated: highlighting of several formal credible (i.e. validated by expertise) specifications from informal requirements; and precise definition of technical expertise role (milestones, planning). However, this reinforcement – in silos – of the two profession viewpoints does not guarantee that they are mutually consistent. Thus, we proposed a convergence method, relying on expertise and on parallel composition of state automata, for the comparison of local and global views.

The purpose of this study is to map different understandings of the formalization of the informal financial sector in the developing world. Utilizing a qualitative approach and interview methodology, this study focuses on the case of South Africa and maps different perceptions about the formalization process by operators in the informal economic sector, which are in turn contrasted with the perceptions of experts and policymakers in the field. The issue at hand is a deeper understanding of how and why different groups perceive formalization in different ways. Some of the main findings of this study confirm that there are different understandings of formalization that can be found amongst different groups in South Africa, that the overall positive understanding of formalization efforts are greater than the negative ones, and that formalization efforts are formulated more inclusive than informal operators believe they are. The theoretical contribution of this study is to state that moral arguments play a bigger role in individuals economical decision-making processes than the economy itself shapes individuals' moral behavior. In addition, the findings are of relevance for the design and implementation of financial inclusion policies in the developing world.

Les micro-entreprises domestiques constituent une part importante, si ce n'est dominante, de toutes les économies en développement. C’est aussi le cas au Vietnam où le poids du secteur informel diminue peu malgré une croissance économique rapide. Les quatre chapitres de ce travail posent quatre questions fondamentales pour informer les politiques publiques. Leur originalité est d'adopter le point de vue des entreprises informelles elles-mêmes. Quels bénéfices y a-t-il à rejoindre le secteur formel (chapitre 1)? Quelle est la vulnérabilité de ces unités de production, dont le budget est souvent confondu avec celui du ménages, aux chocs de santé (chapitre 2) ? L’assurance santé permet-elle de réduire efficacement cette vulnérabilité (chapitre 3) ? Enfin, quelle est l’importance du mode de gestion de ces micro-entreprises (chapitre 4) ? Tous les chapitres s’appuient en premier lieu sur des données d’enquêtes quantitatives, de première ou seconde main. L’approche quantitative est complétée par des enquêtes qualitatives. Les résultats dressent le portrait d’un secteur dynamique, dont la persistance ne peut être ignorée, et suggèrent des mécanismes pour améliorer la productivité de ces entreprises qui opèrent dans des conditions largement précaires. / This PhD dissertation is built around four main chapters. Their topic shall sound familiar to policy makers, and to all empirical economists working on microenterprises, as they quesion the common mottos to deal with the informal sector: “formalize them”, “protect them”, and “train them”. Little of these recommendations rely on actual evidence, in particular regarding their effects for the firms themselves. Chapter one starts by questioning the relevance of formalization: what exactly do these production units have to gain from registration? The second chapter investigates the vulnerability of microenterprises to health problems: how much do they suffer from the consequences of health shocks within the household? The third chapter deals with the complementary question of the protection mechanisms, and questions the mitigating potential of health insurance. The fourth chapter finally deals with their managerial capital: do the business skills that are considered standard among larger firms have any meaning for informal micro enterprises?