”När man kollar på bilden tänker man så här” : en receptionsstudie av gymnasieelevers uppfattning om bilder som kunskapskällor i historieundervisningen

Images are used in history education for a variety of reasons, not least to generate interest through a better understanding of historical events and people. The aim of this study was to investigate how historical pictures, either illustrated or documentary/photographic, can be used as a resource for activating and improving pupils' historical empathy, in the way described by Stéphane Lévasque. I conducted a reception study on five different focus groups consisting of pupils from different upper secondary schools in Sweden. The pupils varied with regard to number of credits for admission to upper secondary school. A sixth group of pupils was interviewed as a contrasting control group in order to add perspective to the results. The discussions were based on the pupils' interpretations of 34 selected pictures, all of which were taken from the most common history textbooks. Each pupil was asked to choose the picture he/she felt was the most representative historical image. On the basis of the strategies used by the pupils when interpreting the pictures and discussing them, the material was analysed in accordance with Lévesque's categories: imagination, historical contextualisation and morals. The last category, morals, was further divided into three sub-categories: sense of justice, sympathy and progression. The reflections of the pupils and the degree of contextualisation varied. It appeared that the pupils were less inclined to discuss assumptions about the persons in the pictures; instead they chose to discuss the historical context in question. The pictures in this study did not seem to trigger the pupils to fabricate anachronistic reasoning about history; when they did produce lengthy reasoning, it was contextual, structural and metahistorical. In this context, the pupils who belonged to the group with the highest average of credits showed some signs of reflection on the basis of historical context and some criticism about the historical sources. On no occasion did any of the pupils choose a picture as a concrete expression of injustice. One of the questions this study aimed to explore was whether a lack of historical context affects how pictures trigger emotions and reasoning on the basis of moral aspects. Some of the pupils displayed moral standpoints, primarily the degree of morals concerning injustice. One possible interpretation could be that the feeling of being unfairly treated and subjected to insulting behaviour and social injustice was something the pupils could relate to. The group of pupils who had not yet studied history at upper secondary school, the control group, generally made reflections using this sort of reasoning when they discussed the historical aspects of the pictures.

Fred: An approach to generating real, correct, reusable programs from proofs

In this paper we describe our system for automatically extracting "correct" programs from proofs using a development of the Curry-Howard process. Although program extraction has been developed by many authors, our system has a number of novel features designed to make it very easy to use and as close as possible to ordinary mathematical terminology and practice. These features include 1. the use of Henkin's technique to reduce higher-order logic to many-sorted (first-order) logic; 2. the free use of new rules for induction subject to certain conditions; 3. the extensive use of previously programmed (total, recursive) functions; 4. the use of templates to make the reasoning much closer to normal mathematical proofs and 5. a conceptual distinction between the computational type theory (for representing programs)and the logical type theory (for reasoning about programs). As an example of our system we give a constructive proof of the well known theorem that every graph of even parity, which is non-trivial in the sense that it does not consist of isolated vertices, has a cycle. Given such a graph as input, the extracted program produces a cycle as promised.

A Compositional Semantics of UML-RSDS

This paper provides a semantics for the UML-RSDS (Reactive System Development Support) subset of UML, using the real-time action logic (RAL) formalism. We show how this semantics can be used to resolve some ambiguities and omissions in UML semantics, and to support reasoning about specifications using the B formal method and tools. We use `semantic profiles' to provide precise semantics for different semantic variation points of UML. We also show how RAL can be used to give a semantics to notations for real-time specification in UML. Unlike other approaches to UML semantics, which concentrate on the class diagram notation, our semantic representation has behaviour as a central element, and can be used to define semantics for use cases, state machines and interactions, in addition to class diagrams.

Coalition Formation through Motivation and Trust

Cooperation is the fundamental underpinning of multi-agent systems, allowing agents to interact to achieve their goals. Where agents are self-interested, or potentially unreliable, there must be appropriate mechanisms to cope with the uncertainty that arises. In particular, agents must manage the risk associated with interacting with others who have different objectives, or who may fail to fulfil their commitments. Previous work has utilised the notions of motivation and trust in engendering successful cooperation between self-interested agents. Motivations provide a means for representing and reasoning about agents' overall objectives, and trust offers a mechanism for modelling and reasoning about reliability, honesty, veracity and so forth. This paper extends that work to address some of its limitations. In particular, we introduce the concept of a clan: a group of agents who trust each other and have similar objectives. Clan members treat each other favourably when making private decisions about cooperation, in order to gain mutual benefit. We describe mechanisms for agents to form, maintain, and dissolve clans in accordance with their self-interested nature, along with giving details of how clan membership influences individual decision making. Finally, through some simulation experiments we illustrate the effectiveness of clan formation in addressing some of the inherent problems with cooperation among self-interested agents.

Valores nas forças armadas brasileiras: uma análise sobre o reconhecimento da sociedade civil

A presente dissertação tem como objetivo refletir sobre a percepção dosvalores nas F orças Almadas Brasileiras por segmentos da sociedade civil organizada. Utilizando como base os estudos de diversos autores, procura desenvolver a fundamentação teórica sobre os valores e as organizações. Neste sentido, busca a construção das nuances explicativas, com base na conceituação e na importância dos valores, tanto para o ser humano como para as mais diversas organizações. A pesquisa de campo se desenvolve por meio de questionários semi-estruturados, suscitando aspectos valiosos em relação aos indivíduos, às organizações militares e à sociedade com os valores de um modo geral.

Mudar o ensino?: concepções, perspectivas e valores de professores de 5ª a 8ª séries

O artigo relata uma experiência, parte de Projeto mais amplo, visando conduzir professores de 1° grau a refletirem sobre os fundamentos de sua prática e sensibilizá-los à mudança. O trabalho desenvolveu-se em encontros semanais mediante debates, painéis, dramatização, coleta de dados junto a alunos e aplicação da técnica das palavras-chave. Os resultados mostram avanços na tomada de consciência do professor quanto ao próprio papel e aos pressupostos de sua ação, além do predomínio de visão equilibrada sobre o modelo tradicional de ensino e perspectiva positiva quanto a sua mudança. As conclusões apontam para a necessidade constante de o professor rever os fundamentos de sua atuação e de buscar ultrapassar o nível do simples fazer da prática, em direção a sua compreensão.

Organização e gestão dos núcleos de atendimento especializado da criança e do adolescente da Defensoria Pública do Pará

A Defensoria Pública é uma das instituições essenciais à função jurisdicional do Estado, encarregada constitucionalmente de garantir o acesso à justiça a população legalmente necessitada, através da orientação jurídica e defesa judicial e extrajudicial em todos os graus. Dentro de sua missão institucional especializou e interiorizou seu atendimento na área infanto juvenil implantando os Núcleos de Atendimento Especializado da Criança e do Adolescente (NAECA‟s) na capital e em mais doze cidades do Pará. Em razão da carência de estudos científicos que demonstrem soluções teóricas e práticas de resolução dos problemas organizacionais da Defensoria Pública, esta dissertação objetiva analisar a gestão e a estrutura organizacional dos NAECA‟s da Defensoria Pública do Estado do Pará, visando à garantia da qualidade de atendimento e da proteção integral de crianças e adolescentes. Utilizou-se a metodologia sistêmica com um estudo de caso múltiplo e, para consolidar os resultados obtidos, usou-se a observação sistemática da instituição pesquisada, realizando entrevistas semiestruturadas e a análise de conteúdo, buscando a descrição do conteúdo manifestado na comunicação que foi realizada. Foi empregado um robusto marco conceitual para a fundamentação da pesquisa a respeito das organizações, das relações de poder e da gestão pública, suporte esse que possibilitou a confirmação das hipóteses formuladas na pesquisa e o alcance dos objetivos propostos, concluindo-se que o problema da pesquisa foi respondido afirmativamente, visto que se conseguiu visualizar o funcionamento da estrutura organizacional e da gestão dos NAECA‟s e sua interrelação, bem como de que modo tal estrutura tem contribuído para garantia da qualidade de atendimento e proteção integral de crianças e adolescentes. Nas conclusões da pesquisa, ficou perceptível que, apesar do trabalho que está sendo realizado, fato comprovado na pesquisa e no projeto redescobrindo o assistido, muito ainda tem que ser feito e a instituição ainda padece de deficiências como a necessidade de maiores investimentos, principalmente em infraestrutura física e de pessoal. Com todos esses desafios, a instituição esbarra na inércia do poder público em densificar o preceito constitucional de garantir o acesso à justiça através de uma instituição que garanta os direitos dos cidadãos em condições de igualdade com o estado-juiz e o estado-acusador e na falta de investimentos para o fortalecimento da instituição que vem lutando para se estabelecer e garantir o acesso à ordem jurídica justa para a população de nosso Estado.

O sistema de cotas para negros na Universidade Federal do Maranhão: uma política de ação afirmativa para a população afromaranhense

Coordenação de Aperfeiçoamento de Pessoal de Nível Superior (CAPES)

Interactive theorem provers: issues faced as a user and tackled as a developer

Interactive theorem provers (ITP for short) are tools whose final aim is to certify proofs written by human beings. To reach that objective they have to fill the gap between the high level language used by humans for communicating and reasoning about mathematics and the lower level language that a machine is able to “understand” and process. The user perceives this gap in terms of missing features or inefficiencies. The developer tries to accommodate the user requests without increasing the already high complexity of these applications. We believe that satisfactory solutions can only come from a strong synergy between users and developers. We devoted most part of our PHD designing and developing the Matita interactive theorem prover. The software was born in the computer science department of the University of Bologna as the result of composing together all the technologies developed by the HELM team (to which we belong) for the MoWGLI project. The MoWGLI project aimed at giving accessibility through the web to the libraries of formalised mathematics of various interactive theorem provers, taking Coq as the main test case. The motivations for giving life to a new ITP are: • study the architecture of these tools, with the aim of understanding the source of their complexity • exploit such a knowledge to experiment new solutions that, for backward compatibility reasons, would be hard (if not impossible) to test on a widely used system like Coq. Matita is based on the Curry-Howard isomorphism, adopting the Calculus of Inductive Constructions (CIC) as its logical foundation. Proof objects are thus, at some extent, compatible with the ones produced with the Coq ITP, that is itself able to import and process the ones generated using Matita. Although the systems have a lot in common, they share no code at all, and even most of the algorithmic solutions are different. The thesis is composed of two parts where we respectively describe our experience as a user and a developer of interactive provers. In particular, the first part is based on two different formalisation experiences: • our internship in the Mathematical Components team (INRIA), that is formalising the finite group theory required to attack the Feit Thompson Theorem. To tackle this result, giving an effective classification of finite groups of odd order, the team adopts the SSReflect Coq extension, developed by Georges Gonthier for the proof of the four colours theorem. • our collaboration at the D.A.M.A. Project, whose goal is the formalisation of abstract measure theory in Matita leading to a constructive proof of Lebesgue’s Dominated Convergence Theorem. The most notable issues we faced, analysed in this part of the thesis, are the following: the difficulties arising when using “black box” automation in large formalisations; the impossibility for a user (especially a newcomer) to master the context of a library of already formalised results; the uncomfortable big step execution of proof commands historically adopted in ITPs; the difficult encoding of mathematical structures with a notion of inheritance in a type theory without subtyping like CIC. In the second part of the manuscript many of these issues will be analysed with the looking glasses of an ITP developer, describing the solutions we adopted in the implementation of Matita to solve these problems: integrated searching facilities to assist the user in handling large libraries of formalised results; a small step execution semantic for proof commands; a flexible implementation of coercive subtyping allowing multiple inheritance with shared substructures; automatic tactics, integrated with the searching facilities, that generates proof commands (and not only proof objects, usually kept hidden to the user) one of which specifically designed to be user driven.

Justified Belief Change

Justification Logic is a framework for reasoning about evidence and justification. Public Announcement Logic is a framework for reasoning about belief changes caused by public announcements. This paper develops JPAL, a dynamic justification logic of public announcements that corresponds to the modal theory of public announcements due to Gerbrandy and Groeneveld. JPAL allows us to reason about evidence brought about by and changed by Gerbrandy--Groeneveld-style public announcements.