A identidade da marca Visobel Itallique

Dissertação apresentada à Universidade Fernando Pessoa como parte dos requisitos para obtenção do grau de Mestre em Ciências Empresariais

Lightweight Formal Verification in Classroom Instruction of Reasoning about Functional Code

In college courses dealing with material that requires mathematical rigor, the adoption of a machine-readable representation for formal arguments can be advantageous. Students can focus on a specific collection of constructs that are represented consistently. Examples and counterexamples can be evaluated. Assignments can be assembled and checked with the help of an automated formal reasoning system. However, usability and accessibility do not have a high priority and are not addressed sufficiently well in the design of many existing machine-readable representations and corresponding formal reasoning systems. In earlier work [Lap09], we attempt to address this broad problem by proposing several specific design criteria organized around the notion of a natural context: the sphere of awareness a working human user maintains of the relevant constructs, arguments, experiences, and background materials necessary to accomplish the task at hand. We report on our attempt to evaluate our proposed design criteria by deploying within the classroom a lightweight formal verification system designed according to these criteria. The lightweight formal verification system was used within the instruction of a common application of formal reasoning: proving by induction formal propositions about functional code. We present all of the formal reasoning examples and assignments considered during this deployment, most of which are drawn directly from an introductory text on functional programming. We demonstrate how the design of the system improves the effectiveness and understandability of the examples, and how it aids in the instruction of basic formal reasoning techniques. We make brief remarks about the practical and administrative implications of the system’s design from the perspectives of the student, the instructor, and the grader.

An investigation of innovation and knowledge creation in virtual worlds

The Internet and World Wide Web have had, and continue to have, an incredible impact on our civilization. These technologies have radically influenced the way that society is organised and the manner in which people around the world communicate and interact. The structure and function of individual, social, organisational, economic and political life begin to resemble the digital network architectures upon which they are increasingly reliant. It is increasingly difficult to imagine how our ‘offline’ world would look or function without the ‘online’ world; it is becoming less meaningful to distinguish between the ‘actual’ and the ‘virtual’. Thus, the major architectural project of the twenty-first century is to “imagine, build, and enhance an interactive and ever changing cyberspace” (Lévy, 1997, p. 10). Virtual worlds are at the forefront of this evolving digital landscape. Virtual worlds have “critical implications for business, education, social sciences, and our society at large” (Messinger et al., 2009, p. 204). This study focuses on the possibilities of virtual worlds in terms of communication, collaboration, innovation and creativity. The concept of knowledge creation is at the core of this research. The study shows that scholars increasingly recognise that knowledge creation, as a socially enacted process, goes to the very heart of innovation. However, efforts to build upon these insights have struggled to escape the influence of the information processing paradigm of old and have failed to move beyond the persistent but problematic conceptualisation of knowledge creation in terms of tacit and explicit knowledge. Based on these insights, the study leverages extant research to develop the conceptual apparatus necessary to carry out an investigation of innovation and knowledge creation in virtual worlds. The study derives and articulates a set of definitions (of virtual worlds, innovation, knowledge and knowledge creation) to guide research. The study also leverages a number of extant theories in order to develop a preliminary framework to model knowledge creation in virtual worlds. Using a combination of participant observation and six case studies of innovative educational projects in Second Life, the study yields a range of insights into the process of knowledge creation in virtual worlds and into the factors that affect it. The study’s contributions to theory are expressed as a series of propositions and findings and are represented as a revised and empirically grounded theoretical framework of knowledge creation in virtual worlds. These findings highlight the importance of prior related knowledge and intrinsic motivation in terms of shaping and stimulating knowledge creation in virtual worlds. At the same time, they highlight the importance of meta-knowledge (knowledge about knowledge) in terms of guiding the knowledge creation process whilst revealing the diversity of behavioural approaches actually used to create knowledge in virtual worlds and. This theoretical framework is itself one of the chief contributions of the study and the analysis explores how it can be used to guide further research in virtual worlds and on knowledge creation. The study’s contributions to practice are presented as actionable guide to simulate knowledge creation in virtual worlds. This guide utilises a theoretically based classification of four knowledge-creator archetypes (the sage, the lore master, the artisan, and the apprentice) and derives an actionable set of behavioural prescriptions for each archetype. The study concludes with a discussion of the study’s implications in terms of future research.

L’isola delle madri assenti: tracce di presenza femminile nella narrativa storica siciliana contemporanea (1990-2007)

The watershed constituted by the historical novels of Leonardo Sciascia (1921- 1989), Vincenzo Consolo (1933-2012) and Andrea Camilleri (born 1925), are starting points for analysing subsequent writings of history in Sicily, particularly those that deal with the hermeneutical function of literature as a means of critically reading official historiography. Nevertheless, whereas ample critical attention has been paid to male writers, whose work is deemed ‘mainstream’, there has been insufficient analysis of the role of female authors in relation to literary representations of Sicilian history. By considering the distinctiveness of the Sicilian literary tradition, the thesis identifies a series of transformations of the genre which have occurred in recent years within the context of feminine writing, and examines the historical narratives of contemporary Sicilian writers Maria Attanasio, Silvana La Spina and Maria Rosa Cutrufelli produced between 1990 and 2007. The study problematizes the lack of critical debate about feminine narratives in Sicily, and places these works in relation to developments in gender and genre theory, focusing particularly on Margherita Ganeri’s studies on the historical genre and the canon. After an introductory chapter which argues the case for examining Sicilian female historical fiction as a distinct literary practice, the subsequent chapters feature textual analyses of each author’s main historical fiction works, supporting the reading of the texts with theoretical readings, including the micro-history of Carlo Ginzburg, the écriture féminine of Hélène Cixous, the abjection theory of Julia Kristeva, the theoretical propositions on “experience” by Joan Wallach Scott and Teresa De Lauretis, and the theory of gender as performance proposed by Judith Butler. The analyses underline the importance of the authors’ distinct feminine perspective over Sicilian history and ultimately suggest that the three writers represent significant examples of a “nomadic writing” to be placed outside the Sicilian male literary tradition.

Examining the post-adoptive infusion of mobile technology in a healthcare domain: determinants and outcomes

The healthcare industry is beginning to appreciate the benefits which can be obtained from using Mobile Health Systems (MHS) at the point-of-care. As a result, healthcare organisations are investing heavily in mobile health initiatives with the expectation that users will employ the system to enhance performance. Despite widespread endorsement and support for the implementation of MHS, empirical evidence surrounding the benefits of MHS remains to be fully established. For MHS to be truly valuable, it is argued that the technological tool be infused within healthcare practitioners work practices and used to its full potential in post-adoptive scenarios. Yet, there is a paucity of research focusing on the infusion of MHS by healthcare practitioners. In order to address this gap in the literature, the objective of this study is to explore the determinants and outcomes of MHS infusion by healthcare practitioners. This research study adopts a post-positivist theory building approach to MHS infusion. Existing literature is utilised to develop a conceptual model by which the research objective is explored. Employing a mixed-method approach, this conceptual model is first advanced through a case study in the UK whereby propositions established from the literature are refined into testable hypotheses. The final phase of this research study involves the collection of empirical data from a Canadian hospital which supports the refined model and its associated hypotheses. The results from both phases of data collection are employed to develop a model of MHS infusion. The study contributes to IS theory and practice by: (1) developing a model with six determinants (Availability, MHS Self-Efficacy, Time-Criticality, Habit, Technology Trust, and Task Behaviour) and individual performance-related outcomes of MHS infusion (Effectiveness, Efficiency, and Learning), (2) examining undocumented determinants and relationships, (3) identifying prerequisite conditions that both healthcare practitioners and organisations can employ to assist with MHS infusion, (4) developing a taxonomy that provides conceptual refinement of IT infusion, and (5) informing healthcare organisations and vendors as to the performance of MHS in post-adoptive scenarios.

Spinoza on method and freedom

The thesis as a whole argues that Spinoza’s Ethics in both method and content is aimed at the normal, partly rational person. Chapter 1 is on Spinoza’s writing style, finding that rather than being arid and technical, it aims to convince the reader by means of various rhetorical techniques, so does not assume an already rational reader. The following chapters of Part 1 examine whether the Ethics’ use of the synthetic geometric method exposes it to Descartes’ critique of that method in the “Second Replies” to his Meditations, that it is not suitable for pedagogy. This involves a consideration of the role of the TIE, finding in that early text not the analytic wing of a two-part analytic-synthetic method, but rather a defence and necessitation of a stand-alone synthetic method. Part 2 of the thesis develops this study of Spinoza’s writing for the common man to consider whether he is writing about the common man. This is done by examining one of the seemingly most abstract propositions in the Ethics, 4P72, which claims that a free man will not deceive even to save his own life. The study examines who exactly is this “free man” and what is his role in the Ethics. The study looks at the examples of free men in the TTP and at the concept of the model in the Ethics, and finds that rather than the free man being an impossible ideal which we can aim at but never achieve, everyone is free to some extent, and that even normal people are at times “the free man”.

A reified temporal logic

This paper presents a reified temporal logic for representing and reasoning about temporal and non-temporal relationships between non-temporal assertions. A clear syntax and semantics for the logic is formally provided. Three types of predicates, temporal predicates, non-temporal predicates and meta-predicates, are introduced. Terms of the proposed language are partitioned into three types, temporal terms, non-temporal terms and propositional terms. Reified propositions consist of formulae with each predicate being either a temporal predicate or a meta-predicate. Meta-predicates may take both temporal terms and propositional terms together as arguments or take propositional terms alone. A standard formula of the classical first-order language with each predicate being a non-temporal predicate taking only non-temporal terms as arguments is reified as just a propositional term. A general time ontology has been provided which can be specialized to a variety of existing temporal systems. The new logic allows one to predicate and quantify over propositional terms while according a special status of time; for example, assertions such as ‘effects cannot precede their causes’ is ensured in the logic, and some problematic temporal aspects including the delay time between events and their effects can be conveniently expressed. Applications of the logic are presented including the characterization of the negation of properties and their contextual sentences, and the expression of temporal relations between actions and effects.

Reified temporal logics: an overview

There are three main approaches to the representation of temporal information in AI literature: the so-called method of temporal arguments that simply extends functions and predicates of first-order language to include time as the additional argument; modal temporal logics which are extensions ofthe propositional or predicate calculus with modal temporal operators; and reified temporal logics which reify standard propositions of some initial language (e.g., the classical first-order or modal logic) as objects denoting propositional terms. The objective of this paper is to provide an overview onthe temporal reified approach by looking closely atsome representative existing systems featuring reified propositions, including those of Allen, McDermott, Shoham, Reichgelt, Galton, and Ma and Knight. We shall demonstrate that, although reified logics might be more complicated in expressing assertions about some given objects with respect to different times, they accord a special status to time and therefore have several distinct advantages in talking about some important issues which would be difficult (if not impossible) to express in other approaches.

A framework for state-based time-series analysis and prediction

Time-series analysis and prediction play an important role in state-based systems that involve dealing with varying situations in terms of states of the world evolving with time. Generally speaking, the world in the discourse persists in a given state until something occurs to it into another state. This paper introduces a framework for prediction and analysis based on time-series of states. It takes a time theory that addresses both points and intervals as primitive time elements as the temporal basis. A state of the world under consideration is defined as a set of time-varying propositions with Boolean truth-values that are dependent on time, including properties, facts, actions, events and processes, etc. A time-series of states is then formalized as a list of states that are temporally ordered one after another. The framework supports explicit expression of both absolute and relative temporal knowledge. A formal schema for expressing general time-series of states to be incomplete in various ways, while the concept of complete time-series of states is also formally defined. As applications of the formalism in time-series analysis and prediction, we present two illustrating examples.

The completeness and soundness of temporal theories

Generally speaking, the term temporal logic refers to any system of rules and symbolism for representing and reasoning about propositions qualified in terms of time. In computer science, particularly in the domain of Artificial Intelligence, there are mainly two known approaches to the representation of temporal information: modal logic approaches including tense logic and hybrid temporal logic, and predicate logic approaches including temporal arguement method and reified temporal logic. On one hand, while tense logic, hybrid temporal logic and temporal argument method enjoy formal theoretical foundations, their expressiveness has been criticised as not power enough for representing general temporal knowledge; on the other hand, although reified temporal logic provides greater expressive power, most of the current systems following the temporal reification lack of complete and sound axiomatic theories. With there observations in mind, a new reified temporal logic with clear syntax and semantics in terms of a sound and complete axiomatic formalism is introduced in this paper, which retains all the expressive power of temporal reification.

A critical evaluation of Enterprise Resource Planning (ERP) software sourcing and provision using theoretical constructs

Deliberating on Enterprise Resource Planning (ERP) software sourcing and provision, this paper contrasts the corporate environment with the small business environment. The paper is about Enterprise Resource Planning client (ERPc) expectations and Enterprise Resource Planning vendor (ERPv) value propositions as a mutually compatible process for achieving acceptable standards of ERP software performance. It is suggested that a less-than-equitable vendor–client relationship would not contribute to the implementation of the optimum solution. Adapting selected theoretical concepts and models, the researchers analyse ERPv to ERPc relationship. This analysis is designed to discover if the provision of the very large ERP vendors who market systems such as SAP, and the provision of the smaller ERP vendors (in this instance Eshbel Technologies Ltd who market an ERP software solution called Priority) when framed as a value proposition (Walters, D. (2002) Operations Strategy. Hampshire, UK: Palgrave), is at all comparable or distinctive.

Sistema integrado para empresas de construcción en Cusco

Actualmente las empresas requieren estrategias innovadoras, que permitan gestionar de forma integral, optimizando los recursos y maximizando los resultados. Siendo el objetivo del presente trabajo de investigación, diseñar un instrumento de gestión integral (gestión de la calidad, ambiental, seguridad y salud ocupacional) para el sector construcción en Cusco. Se realizó un análisis actual de la actividad de construcción, se planteó a diferencia de otras propuestas, el diseño que inicia con el diagnóstico, planificación, organización, ejecución, supervisión y optimización del sistema integral. Los resultados están expresados en el diagnóstico de los 3 sistemas, información clave, para el planteamiento y propuesta de las etapas posteriores; estructurando el planteamiento de los subprogramas basados en el diagnóstico integral, para finalmente determinar los lineamientos estratégicos, de implementación, evaluación y verificación del sistema, teniendo en cuenta la norma ISO 9001: 2008, ISO 14001:2004 y OSHAS 18001:2007; así como la legislación vigente para el Perú.

Orientación al mercado y tipología de las cooperativas agroalimentarias en base a la competitividad. Caso-estudio de las citrícolas españolas

La globalización ha recrudecido más si cabe la competencia en los mercados y las empresas deben afianzar y mejorar su posición competitiva para asegurar la supervivencia. Para ello resulta vital, entre otras cuestiones, velar por los intereses de los inversores al tiempo que cuidan de sus clientes. Las cooperativas sufren una coyuntura semejante respecto a sus socios y el mercado, es decir respecto a sus clientes internos (socios) y externos (mercado). El enfoque de las actividades y la estrategia de la cooperativa frente a esta dualidad determina su grado de orientación al mercado.Los estudios relacionados con la orientación al mercado en cooperativas son escasos en comparación con otras formas empresariales y han estado normalmente centrados en la figura de las cooperativas de segundo grado y circunscritos a sectores muy específicos.El sector citrícola español es uno de los más dinámicos y desarrollados del panorama productivo agrario. Su extensa experiencia comercial tanto a nivel doméstico como internacional confiere un carácter diferenciador a las entidades que operan en este subsector. Este trabajo analiza la posición de las cooperativas citrícolas españolas en relación a la orientación al mercado así como los factores de gestión y estrategia que están relacionadoscon ella. Para ello se utiliza una escala MARKOR, validada en estudios anteriores, sobre una muestra de 45 cooperativas.Se establece además una tipología de cooperativas citrícolas en base a los factores de competitividad que permiten ahondar en el conocimiento que existe sobre esta cuestión en entidades de economía social. Los resultados ponen de manifiesto un elevado grado de relación entre la innovación, el perfil del empresario y el conocimiento del entorno en relación con el grado de orientación al mercado.

Organs of the human brain, created by the human hand? The social epistemology of information technology

Purpose
– Information science has been conceptualized as a partly unreflexive response to developments in information and computer technology, and, most powerfully, as part of the gestalt of the computer. The computer was viewed as an historical accident in the original formulation of the gestalt. An alternative, and timely, approach to understanding, and then dissolving, the gestalt would be to address the motivating technology directly, fully recognizing it as a radical human construction. This paper aims to address the issues.

Design/methodology/approach
– The paper adopts a social epistemological perspective and is concerned with collective, rather than primarily individual, ways of knowing.

Findings
– Information technology tends to be received as objectively given, autonomously developing, and causing but not itself caused, by the language of discussions in information science. It has also been characterized as artificial, in the sense of unnatural, and sometimes as threatening. Attitudes to technology are implied, rather than explicit, and can appear weak when articulated, corresponding to collective repression.

Research limitations/implications
– Receiving technology as objectively given has an analogy with the Platonist view of mathematical propositions as discovered, in its exclusion of human activity, opening up the possibility of a comparable critique which insists on human agency.

Originality/value
– Apprehensions of information technology have been raised to consciousness, exposing their limitations.

tts: A SAT-Solver for Small, Difficult Instances

The Ternary Tree Solver (tts) is a complete solver for propositional satisfiability which was designed to have good performance on the most difficult small instances. It uses a static ternary tree data structure to represent the simplified proposition under all permissible partial assignments and maintains a database of derived propositions known to be unsatisfiable. In the SAT2007 competition version 4.0 won the silver medal for the category handmade, speciality UNSAT solvers and was the top qualifier for the second stage for handmade benchmarks, solving 11 benchmarks which were not solved by any other entrant. We describe the methods used by the solver and analyse the competition Phase 1 results on small benchmarks. We propose a first version of a comprehensive suite of small difficult satisfiability benchmarks (sdsb) and compare the worst-case performance of the competition medallists on these benchmarks.