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

Em direção a uma representação para equações algébricas :uma lógica equacional local

The intervalar arithmetic well-known as arithmetic of Moore, doesn't possess the same properties of the real numbers, and for this reason, it is confronted with a problem of operative nature, when we want to solve intervalar equations as extension of real equations by the usual equality and of the intervalar arithmetic, for this not to possess the inverse addictive, as well as, the property of the distributivity of the multiplication for the sum doesn t be valid for any triplet of intervals. The lack of those properties disables the use of equacional logic, so much for the resolution of an intervalar equation using the same, as for a representation of a real equation, and still, for the algebraic verification of properties of a computational system, whose data are real numbers represented by intervals. However, with the notion of order of information and of approach on intervals, introduced by Acióly[6] in 1991, the idea of an intervalar equation appears to represent a real equation satisfactorily, since the terms of the intervalar equation carry the information about the solution of the real equation. In 1999, Santiago proposed the notion of simple equality and, later on, local equality for intervals [8] and [33]. Based on that idea, this dissertation extends Santiago's local groups for local algebras, following the idea of Σ-algebras according to (Hennessy[31], 1988) and (Santiago[7], 1995). One of the contributions of this dissertation, is the theorem 5.1.3.2 that it guarantees that, when deducing a local Σ-equation E t t in the proposed system SDedLoc(E), the interpretations of t and t' will be locally the same in any local Σ-algebra that satisfies the group of fixed equations local E, whenever t and t have meaning in A. This assures to a kind of safety between the local equacional logic and the local algebras

Especificação do tipo intervalar parametrizado em CASL

The interval datatype applications in several areas is important to construct a interval type reusable, i.e., a interval constructor can be applied to any datatype and get intervals this datatype. Since the interval is, of certain form, a set of elements limited for two bounds, left and right, with a order notions, then it s reasonable that interval constructor enclose datatypes with partial order. On the order hand, what we want is work with interval of any datatype like this we work with this datatype then. it s important to guarantee the properties of the datatype when maps to interval of this datatype. Thus, the interval constructor get a theory to parametrized interval type, i.e., a interval with generics parameters (for example rational, real, complex). Sometimes, the interval application in some algebras doesn t guarantee the mainutenance of their properties, for example, when we use interval of real, that satisfies the field properties, it doesn t guarantee the distributivity propertie. A form to surpass this problem Santiago introduced the local equality theory that weakened the notion of strong equality, and thus, allowing some properties are local keeped, what can be discard before. The interval arithmetic generalization aim to apply the interval constructor on ordered algebras weakened for local equality with the purpose of the keep their properties. How the intervals are important in applications with continuous data, it s interesting specify that theory using a specification language that supply a system development using intervals of form disciplined, trustworth and safe. Currently, the algebraic specification language, based in math models, have been use to that intention often. We choose CASL (Common Algebraic Specification Language) among others languages because CASL has several characteristics excellent to parametrized interval type, such as, provide parcialiy and parametrization

Antropologia das mediações: um estudo sobre trocas, tensões e hierarquias em Coqueiros, Vale do Ceará Mirim

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

A educação informal para o consumo infantil e juvenil na televisão e na mídia

The consumption has become a major pillar of modern capitalism and at the same time, one of the factors that relate to social inequality. Karl Marx developed the theory of historical materialism which maintains a history of society determined by class struggle and the! exploitation of man by man. Considered to be overtaken by those who believe that Marxism is synonymous with real socialism, the Marxist ideals seem more present than in the Western world which each individual takes the individualization (loss of sense of public and collective) and the alienation by the work. Weassumed we could work on these issues in student education, even in elementary school, through questioning of the consumer society, with the criticism of television and the media, the main promoter of the current sense of consumption, as an initial step that could lead to future autonomy of theindividual. The theory of ideology and ideas of Paulo Freire's liberating education theory permeated the experience that happened as a participant observation of groups in the discipline of sociology in the unit 2 of the Colégio Pedro II in Rio de Janeiro, the state capital, an institution under the direct administration Ministry of Education. Wehave found fertile ground in which the students were able to understand and question the meaning of advertising media

Política da literatura e suas faces na palavra muda de Manoel de Barros

Ce travail de thèse ici proposé a comme but de recherche la production litéraire du poète brésilien Manoel Wenceslau Leite Barros, Manoel de Barros, (1916 Cuiabá-MT) en l articulant avec la reflexion sur le concept de politique de l écrite proposé par le philosophe algérien-français Jacques Rancière (1940 Algiers Algérie). L hypothèse qui se presente est celle sur l écrite poétique de Manoel de Barros dont les ―marques du sensible‖ dans les expériences démocratiques sont perceptibles. Sa production inclue ce que se peut denominer d une micrologie poétique, une reconfiguration du ―partager‖, dans le sense de l élaboration pratiques de l égalité, des pratiques de redistribution et de circulation des voix, instauratrices de la constitution esthétiques des communautés différenciées, considérées comme alternatives, face au modèle de système canonique de la litérature. Au moment que sa fonctionnent comme des formes de subvertions, elles produisent des espaces ou marge d émancipation de l être : lecteur et écrivain, en déclanchant des nouvelles perspectives éthiques et esthétiques. De cette manière, l objectif qui se dessine est ce qui comprend comment se configure la proposition d une politique de l écrite de Manoel de Barros et la façon qu elle se place par rapport à une politique des arts. Pour cela, nous utiliseront comme base la pensée de Jacques Rancière qui se fait remarquer, les dernières années, pour entreprendre une refléxion systématique et lucide par rapport aux relations éxistantes entre esthétique et politique dans la société présente, alié à ce que se défine comme des manières et des formes de penser élaborées par le texte poétique (lui même) de Manoel de Barros et de manière incontinué dans ses entretiens-critiques, plubliées dans des journaux et revues, présentées en vidéos, et nous n oublierons pas non plus des contributions théoriques et des refléxions parvenues de la pensée contemporaine

Modelo de risco controlado por resseguro e desigualdades para a probabilidade de ruína

In the work reported here we present theoretical and numerical results about a Risk Model with Interest Rate and Proportional Reinsurance based on the article Inequalities for the ruin probability in a controlled discrete-time risk process by Ros ario Romera and Maikol Diasparra (see [5]). Recursive and integral equations as well as upper bounds for the Ruin Probability are given considering three di erent approaches, namely, classical Lundberg inequality, Inductive approach and Martingale approach. Density estimation techniques (non-parametrics) are used to derive upper bounds for the Ruin Probability and the algorithms used in the simulation are presented

Estimativa da profundidade do embasamento na bacia potiguar usando inversão gravimétrica

The gravity inversion method is a mathematic process that can be used to estimate the basement relief of a sedimentary basin. However, the inverse problem in potential-field methods has neither a unique nor a stable solution, so additional information (other than gravity measurements) must be supplied by the interpreter to transform this problem into a well-posed one. This dissertation presents the application of a gravity inversion method to estimate the basement relief of the onshore Potiguar Basin. The density contrast between sediments and basament is assumed to be known and constant. The proposed methodology consists of discretizing the sedimentary layer into a grid of rectangular juxtaposed prisms whose thicknesses correspond to the depth to basement which is the parameter to be estimated. To stabilize the inversion I introduce constraints in accordance with the known geologic information. The method minimizes an objective function of the model that requires not only the model to be smooth and close to the seismic-derived model, which is used as a reference model, but also to honor well-log constraints. The latter are introduced through the use of logarithmic barrier terms in the objective function. The inversion process was applied in order to simulate different phases during the exploration development of a basin. The methodology consisted in applying the gravity inversion in distinct scenarios: the first one used only gravity data and a plain reference model; the second scenario was divided in two cases, we incorporated either borehole logs information or seismic model into the process. Finally I incorporated the basement depth generated by seismic interpretation into the inversion as a reference model and imposed depth constraint from boreholes using the primal logarithmic barrier method. As a result, the estimation of the basement relief in every scenario has satisfactorily reproduced the basin framework, and the incorporation of the constraints led to improve depth basement definition. The joint use of surface gravity data, seismic imaging and borehole logging information makes the process more robust and allows an improvement in the estimate, providing a result closer to the actual basement relief. In addition, I would like to remark that the result obtained in the first scenario already has provided a very coherent basement relief when compared to the known basin framework. This is significant information, when comparing the differences in the costs and environment impact related to gravimetric and seismic surveys and also the well drillings

O espaço central das atenções: o corredor de integração da região metropolitana de Natal

This work considers the space study of the main road runner of integration of the Region Metropolitan of Natal (RMN) in formation, emphasizing its repercussion for the geographic context of the city, where we identify the positive and negative aspects of such space configuration, as for the aspects of the urban inaquality, economic centrality and of flows, promoted for the state and private capital (national and foreign). The linear convergence and polinucleately of geographic objects in that we identify as Central Space of Attentions (CSA), promoted, and still it promotes, important repercussion in the space estructuretion of the peripheral areas of the RMN, such as in the constitution of the "Capital Value of the Space". In this direction, to endorse the analysis of such reading, choose as cientific ballast the geographic theory, in a perspective dialectic, as well as we rescue contributions of the science of the administration, sociology, economy, amongst others. From the empirical research, subsidized with the application of forms together the entrepreneurs whom they possess investments in the CSA, as well as in the rescue of information you register in cadastre in the Junta Comercial do Estado do Rio Grande do Norte (JUNCERN) and telephonic list, we construct a proposal of reading of the current period of training of the process of space production to which is rank the CSA. The analysis of the data, under a comparative space angle, presents an important contribution to reevaluate the urban space of the RMN in its bigger aspect, exceeding the limits of the studied road corridor

As faces da exclusão social na comunidade África - Natal, RN

This dissertation deals with the study of the faces of social exclusion at present, through a spatial section constituted of a subnormal area (the Community Africa), which groups these aspects in a limited, but revealing, context regarding such problems. Through the following chapters, inequality, exclusion, segregation, the socioeconomics of the Community Africa, and the environmental impacts identified in this community are discussed. At the end of this piece of work, alternatives of possible solutions to the community area pointed, with also the discussion of propositions related to the questions concerning the mitigation of the most relevant problems

Acari-RN: da construção do território aos limites da pobreza

Acari-RN is one of the earliest municipalities in the region of Seridó Potiguar in rio Grande do Norte. In this municipality, two feelings coexist: power and loss. The former, justified by the process of occupation, which gave birth to its micro-region and the latter, marked by economic impoverishment, starting from the decade of 1970, with the decline of its main wealth: the cotton economy. From the association of these feelings, the motivation for the construction of this piece of work emerged. In it, poverty and inequality are discussed, in a dialect relation with the territory, through a theoretical-methodological reflection and from the analysis of the data collected in a field research. In order to valorize and enrich the theme and the study of the territory of Acari, it was necessary to compare it with the other municipalities that it generated: Currais Novos, Jardim do Seridó and Parelhas. Therefore, the use of the elements of a quantitative and qualitative research, applied in the study section, aimed at finding the poverty indicators, which make it difficult the development in Acari.

A reprodução do espaço da pequena produção rural familiar em Canguaretama/RN

This study aimed to explore the process of reproduction of space from the small family farm production in the municipality of Canguaretama, specifically focused on foodstuffs of plant origin, seeking to understand the changes in agrarian space canguaretamense and its impact on small family farms the last 35 years. Since colonization, during the seventeenth century, the production of space agrarian Canguaretama was founded under a structure based on large ownership and cultivation of cane sugar. Secondly, it was being built a small space reserved for food production to meet both the consumption of property, but also for local marketing. In the centuries following the changes in the capitalist system imposed a new dynamic for small food production, mostly in the early twentieth century, with processing plants and mills in the area extending toward the cultivation of sugarcane. In the second half of that century, mainly in the 1980s, the cultivation of cane sugar was encouraged to produce alcohol, which led to a further expansion of sugar cane toward the areas targeted for the production of foodstuffs. Currently, the framework of small food production differs little from the period of colonization in relation to the difficulties faced by this segment of agriculture. Thus, we have a reality based on socio-spatial inequality, and the near absence of the Government, which requires urgent implementation of public policies for the production and organization of small producers into associations or cooperatives to improve the productivity and hence in their standards of living and their families

Pobreza e desigualdades socioterritorias: uma problematização acerca da perspectiva territorial nas politicas públicas sociais no município de Pau dos Ferros/RN

El presente trabajo se constituye en un estudio sobre la pobreza y las desigualdades socio territoriales en el Brasil, problematizando la perspectiva territorial de las políticas públicas sociales observando la distribución espacial del Índice de Desarrollo de las familias (IDF) en el municipio de Pau dos Ferros/RN, así como las principales políticas sociales, a ejemplo del Programa Bolsa Familia. En este sentido, el objetivo principal de esa disertación se dió en la tentativa de comprender la importancia de la lectura previa del territorio para la reflexión sobre la pobreza en su aspecto multidimensional y para la territorialización de las políticas Públicas sociales construidas en el intento de minimizar la problemática de la desigualdad social, observando la distribución espacial do IDF en el municipio de Pau dos Ferros/RN. A partir del objetivo general trazado, hicimos una revisión teórica sobre los temas, pobreza, desigualdades sociales y políticas públicas, en el primero caso atentando para el aspecto multidimensional de esta, abogando la importancia de analizarnos la pobreza no apenas por el nivel de rienda, pero considerando otras dimensiones que corroboran para la constitución del ser pobre, como habitaciones precarias, falta de saneamiento básico e infraestructura, el no acceso a la salud, la educación y los otros servicios que posibilitan el individuo vivir con el mejor dignidad. Comprendiendo la importancia del conocimiento previo del territorio para que ocurra las debidas reflexiones e intervenciones en la realidad territorial buscamos reflexionar acerca de ese concepto en sus nexos con la construcción e implementación de las políticas públicas sociales teniendo la Política Nacional de Asistencia Social (PNAS) como política esencial y también el el Programa Bolsa Familia (PBF), una vez que buscamos compreender su importancia a partir de la visión del sujeto, o sea las beneficiadas del PBF en el Municipio de Pau dos Ferros. Para tanto, hicimos entrevistas orales con las beneficiadas del PBF que fueron elegidas aislada a partir de los equipos del CRAS, además de la aplicación de cuestionarios semiesctructurados y abiertos con gestores y asistentes sociales del muninicipio.Buscamos además trabajar con algunos datos del CadÚnico para el município en estudio proponiendo analisar las condiciones sociales y económicas de las famílias cadastradas. Algunos resultados fueron posibles, a saber, es necesario interpretarse la pobreza a partir de varias dimensiones para no tener el riesgo de quedarnos solamente en la perspectiva financiera, o sea de la rienda, que mismo sirva para lo emergencial no es suficiente para transformar las condiciones de vida de las famílias; PNAS puede ser considerada como un avanzo de la política social en el Brasil una vez que posuye importancia fundamental en la familia. Sin embargo, es preciso avanzar en la interpretación del territorio que en la política y en el habla de los agentes sociales , es interpretación apenas como un recorte donde deberán ocurrir las acciones para minimizar la pobreza ; al fin, o PBF es un programa de urgencia moral una vez que combate lo mas emergencial que es el directo de sobrevivir , pero aun no conseguió transformar de una manera significativa la pobreza en el país