Compartimentação política do território: uma análise do processo no Curimataú oriental Paraibano

During the 1980‟s, the Brazilian State has undergone a process of redemocratization, causing a profund change in the political and institutional organization of the country. That reorientation of the Brazilian federative structure had as normative framework the enactment of the federal Constitution of 1988, occuring after its enactment a considerable political opening under the cloak of new democratic arrangements of tax and fiscal decentralization, which generated a new federative order, especially with regard to municipalities. Such institutions contributed to the creation of several new municipalities, involving, directly, changes in the structure of national territory, driven by the political context. This case was notoriouns in the 1990s, increased in the country's municipal mesh and spread all over the states of the federation. The Paraíba State was integrated in this context, creating in this period, 52 new municipalities. In the perspective, it will seek to understand the purpose that sustained this process of fragmentation of Paraíba state territory. For this purpose was made use of several bibliographies, secondary data, documentary sources and research in locus of the municipalities of Casserengue and Riachão, located in the Paraíba‟s Curimataú Oriental microregion, which were selected as a focus for specific analysis of the event. It is understood, however, that the production of municipalities, includes several intentions through political appropriation of the territory, although, being permeated by the Institutional

Contribuições para o processo de verificação de satisfatibilidade módulo teoria em Event-B

Event-B is a formal method for modeling and verification of discrete transition systems. Event-B development yields proof obligations that must be verified (i.e. proved valid) in order to keep the produced models consistent. Satisfiability Modulo Theory solvers are automated theorem provers used to verify the satisfiability of logic formulas considering a background theory (or combination of theories). SMT solvers not only handle large firstorder formulas, but can also generate models and proofs, as well as identify unsatisfiable subsets of hypotheses (unsat-cores). Tool support for Event-B is provided by the Rodin platform: an extensible Eclipse based IDE that combines modeling and proving features. A SMT plug-in for Rodin has been developed intending to integrate alternative, efficient verification techniques to the platform. We implemented a series of complements to the SMT solver plug-in for Rodin, namely improvements to the user interface for when proof obligations are reported as invalid by the plug-in. Additionally, we modified some of the plug-in features, such as support for proof generation and unsat-core extraction, to comply with the SMT-LIB standard for SMT solvers. We undertook tests using applicable proof obligations to demonstrate the new features. The contributions described can potentially affect productivity in a positive manner.