Beschreibungslogiken (Description logics, DLs) sind eine Klasse von Wissensrepraesentationsformalismen mit wohldefinierter, logik-basierter Semantik und entscheidbaren Schlussfolgerungsproblemen, wie z.B. dem Erfuellbarkeitsproblem. Zwei wichtige Entscheidungsverfahren fuer das Erfuellbarkeitsproblem von DL-Ausdruecken sind Tableau- und Automaten-basierte Algorithmen. Diese haben aufgrund ihrer unterschiedlichen Arbeitsweise komplementaere Eigenschaften: Tableau-Algorithmen eignen sich fuer Implementierungen und fuer den Nachweis von PSPACE- und NEXPTIME-Resultaten, waehrend Automaten sich besonders fuer EXPTIME-Resultate anbieten. Zudem ermoeglichen sie eine vom Standpunkt der Theorie aus elegantere Handhabung von unendlichen Strukturen, eignen sich aber wesentlich schlechter fuer eine Implementierung. Ziel der Dissertation ist es, die Gruende fuer diese Unterschiede zu analysieren und Moeglichkeiten aufzuzeigen, wie Eigenschaften von einem Ansatz auf den anderen uebertragen werden koennen, um so die positiven Eigenschaften von beiden Ansaetzen miteinander zu verbinden. Unter Anderem werden Methoden entwickelt, mit Hilfe von Automaten PSPACE-Resultate zu zeigen, und von einem Tableau-Algorithmus automatisch ein EXPTIME-Resultat abzuleiten. / Description Logics (DLs) are a family of knowledge representation languages with well-defined logic-based semantics and decidable inference problems, e.g. satisfiability. Two of the most widely used decision procedures for the satisfiability problem are tableau- and automata-based algorithms. Due to their different operation, these two classes have complementary properties: tableau algorithms are well-suited for implementation and for showing PSPACE and NEXPTIME complexity results, whereas automata algorithms are particularly useful for showing EXPTIME results. Additionally, they allow for an elegant handling of infinite structures, but they are not suited for implementation. The aim of this thesis is to analyse the reasons for these differences and to find ways of transferring properties between the two approaches in order to reconcile the positive properties of both. For this purpose, we develop methods that enable us to show PSPACE results with the help of automata and to automatically derive an EXPTIME result from a tableau algorithm.

Facing the growing amount of information in today's society, the task of specifying human knowledge in a way that can be unambiguously processed by computers becomes more and more important. Two acknowledged fields in this evolving scientific area of Knowledge Representation are Description Logics (DL) and Formal Concept Analysis (FCA). While DL concentrates on characterizing domains via logical statements and inferring knowledge from these characterizations, FCA builds conceptual hierarchies on the basis of present data. This work introduces Relational Exploration, a method for acquiring complete relational knowledge about a domain of interest by successively consulting a domain expert without ever asking redundant questions. This is achieved by combining DL and FCA: DL formalisms are used for defining FCA attributes while FCA exploration techniques are deployed to obtain or refine DL knowledge specifications.

This research seeks to connect the philosophical focus of the agency-structure debate with the practice of management through a comparative study of organisational decision-making in situations involving stakeholder consultation. Set in the context of decision-making following an airport master plan consultation, the study considers how the stakeholder framework can be integrated within institutional theory using institutional logics as a theoretical link between these two literatures. This thesis, which adopts a critical realist perspective, takes a comparative case approach of four airports, each owned in different ways. Interviews with airport managers are supplemented by discussions with stakeholders and industry experts. Two sets of a priori themes were identified from the literature. The first focuses on the institutional logics prevailing in the field and their influence on managers as they make decisions. The second considers four decision-making strategies managers might employ in this situation. Findings centre on the causal powers acting upon airport managers as they make their decisions. Whilst normative isomorphic pressure enables stakeholder consultation, the coercive pressure on the decision-making process deriving from English planning law, the adversarial and oscillating nature of Central Government policy, and a mimetic response to the nature of local authority development plans constrain the actions of airport managers. Indeed, the current bureaucratic form of capitalism limits stakeholder contribution to final master plans. This research makes four main contributions: Firstly, reflecting upon the agency-structure debate from a critical realist perspective has facilitated development of a model integrating the stakeholder framework within institutional theory. Secondly, it improves our understanding of how stakeholder contribution is managed in master planning. Thirdly, the study adds to the growing body of work that employs a critical realist perspective. Lastly, since reconciling conflicting stakeholder opinions may well be of vital importance to the future of the UK’s airport infrastructure, this work has practical significance for airport managers, government policy-makers and stakeholders as they strive to formulate worthwhile airport consultations.

Starting from the overall Revitalizing Small Millets in South Asia (RESMISA) project objective and question, how to increase millet production and consumption, I will use the same to enter Chintaguda and understand how that can be accomplished in the village. As millets do not occupy a significant aspect of the lives of people in Chintaguda, I essentially sought to understand the general decision-making logics that operate therein. This objective will help me understand which factors and their interactions influence activities around socio-ecological engagements. I aim to devise a framework to comprehend these logics and the complexities found in Chintaguda by using social theories. These will help me stitch together a narrative for Chintaguda that will contextualize the people’s relationship to millets. This study will show the various ways people can and do relate to millets. / February 2016

No description available.

Description Logics (DLs) are a class of knowledge representation formalisms that can represent terminological and assertional knowledge using a well-defined semantics. Often, knowledge engineers are experts in their own fields, but not in logics, and require assistance in the process of ontology design. This thesis presents three methods that can extract terminological knowledge from existing data and thereby assist in the design process. They are based on similar formalisms from Formal Concept Analysis (FCA), in particular the Next-Closure Algorithm and Attribute-Exploration. The first of the three methods computes terminological knowledge from the data, without any expert interaction. The two other methods use expert interaction where a human expert can confirm each terminological axiom or refute it by providing a counterexample. These two methods differ only in the way counterexamples are provided.

The use of formal methods in software development seeks to increase our confidence in the resultant system. Their use often requires tool support, so the integrity of a development using formal methods is dependent on the integrity of the tool-set used. Specifically its integrity depends on the theorem prover, since in a typical formal development system the theorem prover is used to establish the validity of the proof obligations incurred by all the steps in the design and refinement process. In this thesis we are concerned with tool-based formal development systems that are used to develop high-integrity software. Since the theorem prover program is a critical part of such a system, it should ideally have been itself formally verified. Unfortunately, most theorem provers are too complex to be verified formally using currently available techniques. An alternative approach, which has many advantages, is to include a proof checker as an extra component in the system, and to certify this. A proof checker is a program which reads and checks the proofs produced by a theorem prover. Proof checkers are inherently simpler than theorem provers, since they only process actual proofs, whereas much of the code of a theorem prover is concerned with searching the space of possible proofs to find the required one. They are also free from all but the simplest user interface concerns, since their input is a proof produced by another program, and their output may be as simple as a `yes/no' reply to the question: Is this a valid proof? plus a list of assumptions on which this judgement is based. When included in a formal development system a stand-alone proof checker is, in one sense, superfluous, since it does not produce any proofs -- the theorem prover does this. Instead its importance is in establishing the integrity of the results of the system -- it provides extra assurance. A proof checker provides extra assurance simply by checking the proofs, since all proofs have then been validated by two independent programs. However a proof checker can provide an extra, and higher, level of assurance if it has been formally verified. In order for formal verification to be feasible the proof checker must be as simple as possible. In turn the simplicity of a proof checker is dependent on the complexity of the data which it processes, that is, the representation of the proofs that it checks. This thesis develops a representation of proofs that is simple and generic. The aim is to produce a generic representation that is applicable to the proofs produced by a variety of theorem provers. Simplicity facilitates verification, while genericity maximises the return on the effort of verification. Using a generic representation places obligations on the theorem provers to produce a proof record in this format. A flexible recorder/translator architecture is proposed which allows proofs to be recorded by existing theorem provers with minimal changes to the original code. The prover is extended with a recorder module whose output is then, if necessary, converted to the generic format by a separate translator program. A formal specification of a checker for proofs recorded in this representation is given. The specification could be used to formally develop a proof-checker, although this step is not taken in this thesis. In addition the characteristics of both the specification and possible implementations are investigated. This is done to assess the size and feasibility of the verification task, and also to confirm that the design is not over-sensitive to the size of proofs. This investigation shows that a checker developed from the specification will be scalable to handle large proofs. To investigate the feasibility of a system based on this architecture, prototype proof recorders were developed for the Ergo 5 and Isabelle 98 theorem provers. In addition a prototype checker was written to check proofs in the proposed format. This prototype is compatible with the formal specification. The combined system was tested successfully using existing proofs for both the Ergo 5 and Isabelle 98 theorem provers.

Les logiques multivalentes sont définies comme une famille de logiques non classiques dont la caractéristique commune est de ne pas restreindre les valeurs de vérité aux seuls « vrai » et « faux ». À cet égard, Kleene (1938) a offert une logique se fondant sur l’intuition que tout énoncé est soit vrai, soit faux ; mais qu’il existe néanmoins des énoncés dont la valeur de vérité n’est pas connue. La formalisation d’une telle intuition amena Kleene à introduire une troisième attribution de valeur de vérité pour les énoncés : « inconnu ». Pour autant, une telle formalisation reste ambiguë : elle échoue à résoudre la dichotomie entre le fait que tout énoncé est soit vrai, soit faux et le fait qu’il existe des énoncés dont l’attribution de valeur de vérité n’est ni « vrai », ni « faux ». L’enjeu de la présente thèse sera l’introduction d’une nouvelle logique multivalente intitulée logique de l’agent rationnel se fondant sur les idées de Kleene tout en en éliminant l’ambiguïté décrite plus haut.La logique de l’agent rationnel permet de modéliser le raisonnement d’un agent en considérant la connaissance (ou l’ignorance) qu’il peut avoir de la valeur de vérité classique des énoncés. D’un point de vue technique, nous introduisons plusieurs définitions de la notion de conséquence logique dans ce cadre, et construisons sur cette base, des sémantiques complètes de notre logique. Nous montrons ensuite l’intérêt d’une telle formalisation en l’appliquant à l’étude d’un problème épistémologique connu sous le nom de « paradoxe de la connaissabilité ». D’un point de vue épistémologique, l’introduction de la logique de l’agent rationnel permet d’analyser la notion d’ignorance comme indépendante de celle de connaissance. Une telle formalisation ouvre ainsi la voie à une position inédite, selon laquelle la notion d’ignorance est primitive et non analysable. / Many-valued logics is a family of non-classical logics, which is characterized by the fundamental fact that they do not restrict the truth values to only truth and falsity. According to this line of inquiry, Kleene (1938) constructed a logic that is based on the idea that every proposition is either true, or false, but there exist propositions for which the truth value is unknown. The formalisation of this idea leads to the introduction of a third assignment of truth value to propositions, interpreted as “unknown”. However, this formalisation contains an ambiguity, because it does not permit the resolution of a contradiction between the fact that every proposition is either true or false, and the fact that there exist propositions for which the assignment of truth value is neither “true” nor “false”. The initial aim of the present thesis is to explore Kleene’s idea in order to introduce and analyse a new many-valued logic, to be called the logic of a rational agent, that is founded on Kleene’s ideas, but that eliminates the above-mentioned ambiguity.The logic of a rational agent models the reasoning of an agent, taking into account the knowledge (or ignorance) of the classical truth value of a proposition that the agent can have. On the technical level, we introduce diverse definitions of entailment relations and construct consistent and complete semantics on this base. We then show the interest inherent in such a formalisation, by proposing an application of this logic to a famous epistemological problem, known as the “knowability paradox”. On the epistemological level, the logic of a rational agent permits us to offer an analysis of the notion of ignorance, as understood independently from the notion of knowledge. Such a formalization.

O objetivo deste estudo foi investigar a legitimidade das atividades relativas à comercialização da ciência através da participação de cientistas em mecanismos de transferência de tecnologia e conhecimento para empresas em uma universidade pública no Brasil. O ponto de partida da pesquisa remete às discussões em torno da relação universidade-empresa, estudadas por distintas perspectivas que ressaltam desde a emergência de novos paradigmas na produção do conhecimento científico, tais como os argumentos da universidade empreendedora, até análises mais críticas, ora sublinhando os efeitos negativos, ora demonstrando a manutenção de fronteiras institucionais entre as duas organizações. A investigação utilizou dois métodos: 1) levantamento da participação de pesquisadores em processos de transferência de tecnologia para a indústria, utilizando dados secundários; e 2) pesquisa qualitativa por meio de entrevistas semiestruturadas, identificando os diferentes tipos de manipulação de lógicas institucionais nas práticas acadêmicas, ora voltadas para a comercialização, ora imersas na ciência pública. Verificou-se elevado crescimento de interações da universidade com a indústria. Entretanto, dois aspectos são ponderados. O primeiro diz respeito à predominância de mecanismos tradicionais de transferência de tecnologia, comparado aos outros tipos de interações. O segundo refere-se ao baixo nível de legitimação de práticas empreendedoras nos casos analisados, visto a defesa da lógica científica sobre a lógica comercial. Para a avaliação da incorporação de novos valores e normas sociais na ciência pública, estabeleceram-se tipologias de orientações científicas: orientação tradicional, orientação tradicional híbrida e orientação empreendedora. A partir dos resultados, conclui-se que o argumento da universidade empreendedora apresenta sérias limitações, visto a baixa legitimidade de novos processos de transferência de tecnologia na amostra analisada. Assim, a difusão de novas práticas científicas orientadas para o maior contato com as demandas econômicas, não necessariamente expressam um processo de institucionalização do empreendedorismo acadêmico, como a incorporação de novos valores, normas e orientações científicas. / The objective of this study was to investigate the legitimacy of the activities related to commercialization of science, through the participation of scientists in mechanisms for transferring technology and knowledge to companies in a public university in Brazil. The starting point of the research refers to the discussions around the relationship between universities and business, studied by different perspectives that highlight since the emergence of new paradigms in the production of scientific knowledge, such as the arguments of the entrepreneurial university, even more critical analysis, sometimes stressing negative effects, sometimes demonstrating the maintenance of institutional boundaries between the two organizations. The research used two methods: 1) raising the participation of researchers in the process of technology transfer to industry, using secondary data and 2) qualitative research using semi-structured interviews, identifying the different types of institutional logics handling academic practices, now focused on marketing, sometimes immersed in public science. There was considerable growth in the university's interactions with industry. However, two aspects are considered. The first concerns the predominance of traditional mechanisms of technology transfer, compared to other types of interactions. The second refers to the low level of legitimation of entrepreneurial practices in the cases analyzed, since the defense of scientific logic on the business logic. To evaluate the incorporation of new values and social norms in public science, settled types of scientific orientations: traditional orientation, hybrid traditional orientation and entrepreneurial orientation. From the results it is concluded that the argument of the entrepreneurial university has serious limitations, as the low legitimacy of new processes of technology transfer in the sample. Thus, the diffusion of new scientific practices oriented more contact with the economic demands, not necessarily express a process of institutionalization of academic entrepreneurship, such as the incorporation of new values, norms and scientific orientations.

Submitted by Michelle Holperin (mimoretz@gmail.com) on 2017-07-05T11:36:45Z No. of bitstreams: 1 The Institutional Pluralism of the State.pdf: 4295867 bytes, checksum: 8d35c5e25d3078a289613f86df68e81b (MD5) / Approved for entry into archive by Maria Almeida (maria.socorro@fgv.br) on 2017-07-07T18:37:35Z (GMT) No. of bitstreams: 1 The Institutional Pluralism of the State.pdf: 4295867 bytes, checksum: 8d35c5e25d3078a289613f86df68e81b (MD5) / Made available in DSpace on 2017-07-07T18:38:02Z (GMT). No. of bitstreams: 1 The Institutional Pluralism of the State.pdf: 4295867 bytes, checksum: 8d35c5e25d3078a289613f86df68e81b (MD5) Previous issue date: 2017-06-05 / What are the logics that public organizations enact in their daily activities? This doctoral dissertation investigated the institutional logics of the State. The institutional logic concept adopted was the one of Friedland and colleagues: institutional logics are 'stable constellations of practice', the necessary coupling of substances and material practices that constitutes the institutions’ organizing principles (Friedland et.al., 2014). The State is understood as one of the central institutions of society, composed by two dimensions. One is the bureaucratic dimension, permeated by different ideas about how things should be done in the State. The other is the capitalist dimension, permeated by different ideas about what should be done,i.e., what should be the role of the State. I have chosen a specific type of public organization to explore the logic of the State: the Brazilian independent regulatory agencies (IRAs). IRAs have diffused widely in the past years, and the literature suggests that they represent the 'appropriate model of governance' of the capitalist economy (Levi-Faur, 2005). They changed both how things were done - emphasizing the state's rule-making instruments - and what should be done - focusing on competition promotion and correcting market failures (Majone, 1994). In Brazil, IRAs were part of a broader process of State Reform, and represented an important innovation in terms of organizational design, based on autonomy, and role to be performed, based on competition promotion. However, the process of IRAs’ diffusion was largely impacted by the local context and despite being idealized as purely regulatory, their policies and activities indicate that they do much more than promoting competition. In fact, state policies in general, and regulatory policies in particular, 'are rooted in changing conceptions of what the state is, what it can and should do' (Friedland & Alford, 1991). To assess the institutional logics of the State, this research investigated over 9,000 press releases published by three formal independent regulatory agencies in Brazil between 2002 and 2016. Those press releases cover all the news they released since their creation. Press releases are frequently used by Brazilian IRAs, and they serve as a good proxy of the policies and activities conducted by these agencies. I applied a correlated topic model (CTM) to extract the main themes discussed by the agencies in the past years. Originating from the study areas of natural language processing and machine learning, topic models are probabilistic models that uncover the semantic structure of a collection of documents, or corpus (Blei, 2012; Blei, Ng & Jordan, 2003). Differently from other content analysis techniques, topic models are purely inductive and conform to the ‘relationality’ of meaning assumption of the institutional logics literature (DiMaggio, Nag & Blei, 2013). The results indicated that the logics enacted by independent agencies do not refer only to procedural correctness (Meyer & Hammerschmid, 2006) or democracy (Ocasio, Mauskapf & Steele, 2015). In fact, much of what they do is grounded on broader substantive values, reflecting developmental-, pro-competition- and social-oriented interpretations of the role of the State. Yet, the bureaucratic logic is very pervasive within IRAs: it permeates substantive logics, but also it stands up as a logic of its own. Regulatory agencies enact it more often when they are not able to perform their substantive mission. IRAs re-frame at their discretion the practices of administrative police (standards setting and inspections) and public participation (procedural fairness) during periods of crisis, in order to justify their actions. By doing so, they were able to legitimate their existence, gain a new sense of mission and avoid blame for their actions.