Paul Ricouer: entre hermenêutica e crítica das ideologias

This work exposes the Paul Ric ur s thought in relation to the contemporary complaint between the hermeneutics and the ideologies criticism. It shows, in this direction, the unity between text and action according to Ric ur s perspective. The philosophical view of Ric ur, It affirms, is far from any eclecticism, but if it characterizes for a dynamic style, explained here from the analogies with the movement of the particles, of the quantum physics, which help to excuse to the make a mistake idea of compilation and eclecticism, resultant of superficial readings of its texts. In deep, this work nothing more it is that a contribution to the construction of a theory of the reading of the text of this notable philosopher

O conceito de liberdade em o ser e o nada de Jean-Paul Sartre

This dissertation aims to address the concept of freedom from the perspective of the French philosopher Jean-Paul Sartre with reference to the main work Being and Nothingness. After presenting the concept of freedom we will try to show that it is related to the notion of responsibility, which will lead, ultimately, to define the Sartrean philosophy as a philosophy of action. In the first chapter we will present in passing the phenomenology of Edmund Husserl, philosopher from which Sartre will develop his concept of freedom. The Husserlian notion of consciousness (intentionality) is the way to develop his analysis of Sartre phenomenon of being. From this analysis Sartre submits their concepts of being in-itself and being for-itself. Being initself is defined as the things of the world devoid of consciousness, are the things that surround us. The In-itself has as its main brand positivity: it is what it is, is all that can be said about him. In turn being For-itself is the very being of man, which differs radically from the In-itself. The For-itself has as its main intentionality, ie, its ability to project outside itself in existence. That's when Sartre shows that this type of being realizes its existence on the basis of a constant nihilation. Here comes the notion of anything. Among the relations of the For-itself with the surrounding world stands a very special: relationship between consciousnesses. It is when we discuss the issue of another. Intersubjectivity, through sartrean analysis of look, show that the For-itself assumes a new existential dimension: the being-for others. That's when Sartre will emphasize his notion of conflict. The conflict in intersubjectivity would come from the fact that you want to take another- For-itself as an object. Given this we will analyze what Sartre called the concrete relations with others. The philosopher submit such relations in the form of ducts and conduits assimilation of ownership. In the first my-self to try to "get lost" in the consciousness of another, ownership of my conduct in-itself tries to "take ownership" of the subjectivity of the other and try to treat others as things, as objects. In this sense Sartre examines the experiences of love, masochism, indifference, desire and sadism. Following this route we will enter the land of freedom itself, which is the major theme of our work. Since Sartre defines the For-itself as a being that is projected to create your way of being, it can only define it as freedom. The freedom of the For-itself is taken in terms of autonomy of choice. Once the For-itself has no way of being a thing as being in-itself, it just may be picking up, that is, making your being. Here Sartre speaks of the anguish that would be the symptom of freedom itself. The fact that the For-itself have to choose on whether the call as one being distressed. However, in most cases the For-itself tries to escape from the anguish of freedom and takes refuge in bad faith. After setting the man (For-itself) as freedom Sartre defends that he is totally responsible for what he does of himself. Once the philosopher holds that man is not predetermined, ie, does not have an a priori essence, his philosophy has as its basic assumption the action. If Sartre argues that the For-itself must constantly choose your way of being, the action is the basis on which man will exercise his own freedom. In this sense we conclude the work with an approach to work Existentialism is a Humanism, which represent the entry of the philosopher on the practical aspects of life

Prova automática de satisfatibilidade módulo teoria aplicada ao método B

Este trabalho apresenta uma extensão do provador haRVey destinada à verificação de obrigações de prova originadas de acordo com o método B. O método B de desenvolvimento de software abrange as fases de especificação, projeto e implementação do ciclo de vida do software. No contexto da verificação, destacam-se as ferramentas de prova Prioni, Z/EVES e Atelier-B/Click n Prove. Elas descrevem formalismos com suporte à checagem satisfatibilidade de fórmulas da teoria axiomática dos conjuntos, ou seja, podem ser aplicadas ao método B. A checagem de SMT consiste na checagem de satisfatibilidade de fórmulas da lógica de primeira-ordem livre de quantificadores dada uma teoria decidível. A abordagem de checagem de SMT implementada pelo provador automático de teoremas haRVey é apresentada, adotando-se a teoria dos vetores que não permite expressar todas as construções necessárias às especificações baseadas em conjuntos. Assim, para estender a checagem de SMT para teorias dos conjuntos destacam-se as teorias dos conjuntos de Zermelo-Frankel (ZFC) e de von Neumann-Bernays-Gödel (NBG). Tendo em vista que a abordagem de checagem de SMT implementada no haRVey requer uma teoria finita e pode ser estendida para as teorias nãodecidíveis, a teoria NBG apresenta-se como uma opção adequada para a expansão da capacidade dedutiva do haRVey à teoria dos conjuntos. Assim, através do mapeamento dos operadores de conjunto fornecidos pela linguagem B a classes da teoria NBG, obtem-se uma abordagem alternativa para a checagem de SMT aplicada ao método B

Deciding difference logic in a Nelson-Oppen combination framework

O método de combinação de Nelson-Oppen permite que vários procedimentos de decisão, cada um projetado para uma teoria específica, possam ser combinados para inferir sobre teorias mais abrangentes, através do princípio de propagação de igualdades. Provadores de teorema baseados neste modelo são beneficiados por sua característica modular e podem evoluir mais facilmente, incrementalmente. Difference logic é uma subteoria da aritmética linear. Ela é formada por constraints do tipo x − y ≤ c, onde x e y são variáveis e c é uma constante. Difference logic é muito comum em vários problemas, como circuitos digitais, agendamento, sistemas temporais, etc. e se apresenta predominante em vários outros casos. Difference logic ainda se caracteriza por ser modelada usando teoria dos grafos. Isto permite que vários algoritmos eficientes e conhecidos da teoria de grafos possam ser utilizados. Um procedimento de decisão para difference logic é capaz de induzir sobre milhares de constraints. Um procedimento de decisão para a teoria de difference logic tem como objetivo principal informar se um conjunto de constraints de difference logic é satisfatível (as variáveis podem assumir valores que tornam o conjunto consistente) ou não. Além disso, para funcionar em um modelo de combinação baseado em Nelson-Oppen, o procedimento de decisão precisa ter outras funcionalidades, como geração de igualdade de variáveis, prova de inconsistência, premissas, etc. Este trabalho apresenta um procedimento de decisão para a teoria de difference logic dentro de uma arquitetura baseada no método de combinação de Nelson-Oppen. O trabalho foi realizado integrando-se ao provador haRVey, de onde foi possível observar o seu funcionamento. Detalhes de implementação e testes experimentais são relatados

Contribuições para verificação automática de applets javacard

The widespread growth in the use of smart cards (by banks, transport services, and cell phones, etc) has brought an important fact that must be addressed: the need of tools that can be used to verify such cards, so to guarantee the correctness of their software. As the vast majority of cards that are being developed nowadays use the JavaCard technology as they software layer, the use of the Java Modeling Language (JML) to specify their programs appear as a natural solution. JML is a formal language tailored to Java. It has been inspired by methodologies from Larch and Eiffel, and has been widely adopted as the de facto language when dealing with specification of any Java related program. Various tools that make use of JML have already been developed, covering a wide range of functionalities, such as run time and static checking. But the tools existent so far for static checking are not fully automated, and, those that are, do not offer an adequate level of soundness and completeness. Our objective is to contribute to a series of techniques, that can be used to accomplish a fully automated and confident verification of JavaCard applets. In this work we present the first steps to this. With the use of a software platform comprised by Krakatoa, Why and haRVey, we developed a set of techniques to reduce the size of the theory necessary to verify the specifications. Such techniques have yielded very good results, with gains of almost 100% in all tested cases, and has proved as a valuable technique to be used, not only in this, but in most real world problems related to automatic verification