Made available in DSpace on 2015-04-14T14:33:30Z (GMT). No. of bitstreams: 1 416269.pdf: 182837 bytes, checksum: b16cf819605f100fbf7bfc0476dee074 (MD5) Previous issue date: 2009-03-23 / A presente disserta??o de mestrado inicia destacando a influ?ncia dos ideais do Estado Liberal sobre a jurisdi??o e sobre o ordenamento jur?dico brasileiro. Dentre outros aspectos, confere especial destaque: a) ? elei??o da legalidade como principal fundamento do Estado; b) ao dogma da intangibilidade da vontade humana; c) ? consagra??o da tutela indenizat?ria como ?nica resposta poss?vel; d) ? impessoalidade da presta??o jurisdicional. Analisa a repercuss?o desses ideais sobre o processo civil da ?poca, ressaltando os sintomas da crise do processo civil cl?ssico diretamente relacionados ao pensamento liberal, dentre outros: a) a insufici?ncia da tutela gerada pelo bin?mio conhecimento-execu??o; b) a aus?ncia de mecanismos aptos ? preven??o do il?cito; c) a aus?ncia de tutela apta ?s situa??es de urg?ncia; d) a uniformidade de procedimentos. A segunda parte do trabalho destaca o surgimento do Estado Social e a sua influ?ncia, juntamente com a Constitui??o de 1988, sobre a jurisdi??o e sobre o ordenamento jur?dico brasileiro. Exp?em-se, resumidamente, aspectos gerais da teoria dos direitos fundamentais ? vista da Constitui??o de 1988, propondo-se o reconhecimento do direito fundamental de todo e qualquer cidad?o ? presta??o jurisdicional efetiva e adequada (dever do Estado). Defende-se um novo conceito de jurisdi??o, respons?vel, al?m da declara??o do direito, pela sua efetiva??o no mundo dos fatos. D?-se relev?ncia ? chegada da tutela espec?fica das obriga??es n?o pecuni?rias (obriga??es de fazer, n?o fazer e dar) no ordenamento jur?dico brasileiro e a sua import?ncia como meio de concretiza??o do direito fundamental ? efetividade e adequa??o da presta??o jurisdicional. A terceira e ?ltima parte aborda, em toda a sua extens?o, o procedimento estabelecido pelos artigos 461 e 461-A do C?digo de Processo Civil Brasileiro, com especial ?nfase aos mecanismos sancionat?rios de conduta (coercitivos e sub-rogat?rios), voltados ? obten??o do resultado espec?fico da obriga??o reconhecida em decis?o final ou interlocut?ria.

Made available in DSpace on 2015-04-14T14:33:28Z (GMT). No. of bitstreams: 1 412936.pdf: 115922 bytes, checksum: 877db91fd30f26fda7ef81553a9cacb6 (MD5) Previous issue date: 2009-12-17 / O trabalho versa sobre a multa coercitiva, expressamente prevista nos artigos 461 e 461-A, do C?digo de Processo Civil, e pretende verificar a utilidade do instituto na presta??o de uma tutela jurisdicional efetiva. Para tanto, a execu??o por coer??o patrimonial ? pesquisada em fontes doutrin?rias, nacionais e estrangeiras, e jurisprudenciais. Neste percurso, a pesquisa tangencia as bases te?ricas da astreinte no direito estrangeiro e no direito brasileiro. Ent?o, ? esbo?ado um delineamento da raz?o para a exist?ncia do instituto com a sua caracteriza??o, desde a defini??o de sua natureza jur?dica at? a sua exigibilidade. No decorrer, a an?lise recai sobre quest?es divergentes na doutrina e na jurisprud?ncia. A conclus?o ? que, conforme os preceitos constitucionais, a coer??o patrimonial, prevista nos artigos referidos, tem como finalidade a busca do cumprimento dos provimentos judiciais e, assim, a obten??o da almejada efetividade do processo.

Submitted by Caroline Xavier (caroline.xavier@pucrs.br) on 2017-06-30T17:26:35Z No. of bitstreams: 1 TES_ROGERIO_SANTOS_RAMME_PARCIAL.pdf: 184649 bytes, checksum: bbdf793d455af326dbc06d96035cfd28 (MD5) / Approved for entry into archive by Caroline Xavier (caroline.xavier@pucrs.br) on 2017-06-30T17:26:43Z (GMT) No. of bitstreams: 1 TES_ROGERIO_SANTOS_RAMME_PARCIAL.pdf: 184649 bytes, checksum: bbdf793d455af326dbc06d96035cfd28 (MD5) / Made available in DSpace on 2017-06-30T17:26:49Z (GMT). No. of bitstreams: 1 TES_ROGERIO_SANTOS_RAMME_PARCIAL.pdf: 184649 bytes, checksum: bbdf793d455af326dbc06d96035cfd28 (MD5) Previous issue date: 2017-03-23 / Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior - CAPES / The aim of this thesis is to identify the normative dimensions of the fundamental duty of individuals towards the ecological balance of the environment, identifying the nature of the obligations arising from that obligation. The link between the object of the constitutional protection of the environment and the concept of ecosystem services is evidenced, which makes it possible to reinterpret the content of the obligations imposed on individuals by virtue of this fundamental duty. Although the fundamental ecological duty has content associated with the fundamental right to the environment, invests individuals in autonomous subjective positions, which will constitute obligations of conduct with positive or negative content, aimed at the protection of ecosystem services. Another important point of the research is to understand the conceptual distinction between ecosystem services and environmental services. The positive obligations stemming from the fundamental ecological duty have the identical object of what is being called environmental services. One of the viable paths to the realization of these obligations is the incentive. In this context, the protector-receiver principle is identified as a normative source that bases the consolidation of a promotional legal system, complementary to the rules of command and control. The concrete instrumentalization of the protectorrecipient principle, especially in countries of intense social inequality, should be thought of as an instrument of environmental justice. Thus serving not only as a source of income for the poorest who engage in environmental services, but also as a way of valuing the habits and cultures of traditional peoples and communities, which, without gaining anything in return, contribute to the generation of ecosystem services. / A presente tese objetiva identificar as dimens?es normativas do dever fundamental dos particulares para com o equil?brio ecol?gico do ambiente, identificando a natureza das obriga??es que decorrem desse dever. Evidencia-se a vincula??o existente entre o objeto da prote??o constitucional do ambiente ao conceito de servi?os ecossist?micos, o que permite reinterpretar o conte?do das obriga??es que se imp?em aos particulares por for?a desse dever fundamental. O dever fundamental ecol?gico, muito embora possua conte?do associado ao direito fundamental ao ambiente investe os indiv?duos em posi??es subjetivas aut?nomas, que v?o se constituir em obriga??es de conduta com conte?do positivo ou negativo, voltadas ? prote??o dos servi?os ecossist?micos. Outro ponto importante da pesquisa ? a distin??o conceitual entre servi?os ecossist?micos e servi?os ambientais. As obriga??es de cunho positivo que decorrem do dever fundamental ecol?gico, tem o id?ntico objeto daquilo que se est? a denominar por servi?os ambientais. Um dos caminhos vi?veis para a concretiza??o dessas obriga??es ? o do incentivo. Nesse contexto, se identifica o princ?pio do protetor-recebedor como fonte normativa que fundamenta a consolida??o de um sistema jur?dico promocional, complementar ?s normas de comando e controle. A instrumentaliza??o concreta do princ?pio do protetor-recebedor, sobretudo em pa?ses de intensa desigualdade social, n?o s? pode como deve ser pensado tamb?m como um instrumento de justi?a ambiental, servindo n?o apenas como uma fonte de renda para os mais carentes que se empenhem em servi?os ambientais, mas tamb?m como forma de valoriza??o dos h?bitos e culturas de povos e comunidades tradicionais, que, sem ganhar nada em troca, contribuem com a gera??o de servi?os ecossist?micos.

Submitted by Automa??o e Estat?stica (sst@bczm.ufrn.br) on 2016-08-26T23:09:02Z No. of bitstreams: 1 VitorAlcantaraDeAlmeida_DISSERT.pdf: 2275305 bytes, checksum: 861287dd67240f715c731a69f2fa5aec (MD5) / Approved for entry into archive by Arlan Eloi Leite Silva (eloihistoriador@yahoo.com.br) on 2016-08-30T23:32:12Z (GMT) No. of bitstreams: 1 VitorAlcantaraDeAlmeida_DISSERT.pdf: 2275305 bytes, checksum: 861287dd67240f715c731a69f2fa5aec (MD5) / Made available in DSpace on 2016-08-30T23:32:12Z (GMT). No. of bitstreams: 1 VitorAlcantaraDeAlmeida_DISSERT.pdf: 2275305 bytes, checksum: 861287dd67240f715c731a69f2fa5aec (MD5) Previous issue date: 2016-04-29 / Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior (CAPES) / A presente disserta??o descreve uma extens?o para a plataforma Frama-C e o plugin WP:o WPTrans. Essa extens?o permite a manipula??o, atrav?s de regras de infer?ncia, dasobriga??es de prova geradas pelo WP, com a possibilidade das mesmas serem enviadas,em qualquer etapa da modifica??o, a solucionadores SMT e assistentes de prova. Algumasobriga??es de prova podem ser validadas automaticamente, enquanto outras s?o muitocomplexas para os solucionadores SMT, exigindo uma prova manual pelo desenvolvedor,atrav?s dos assistentes de prova. Contudo, a segunda abordagem geralmente requer dousu?rio uma experi?ncia significativa em estrat?gias de prova. Alguns assistentes oferecemcomunica??o com provadores autom?ticos, entretanto, esta liga??o pode ser complexaou incompleta, restando ao usu?rio apenas a prova manual. O objetivo deste plugin ? interligaros dois tipos de ferramentas de modo preciso e completo, com uma linguagemsimples para a manipula??o. Assim, o usu?rio pode simplificar suficientemente as obriga??es deprova para que possam ser validadas por qualquer outro solucionador SMT.N?o obstante, a extens?o ? interligada diretamente ao WP, facilitando a instala??o doplugin no Frama-C. Esta extens?o tamb?m ? uma porta de entrada para outras poss?veisfuncionalidades, sendo as mesmas discutidas neste documento. / The platform Frama-C is a tool dedicated to analysis of source code of software written in C, with the possible types of analysis provided by plugins attached to the platform. One of its plugins is WP, used for deductive veri cation of C code with ACSL, a formal speci cation language. This dissertation describes the extension of this plugin, named WPTrans. This extension allows generated proof obligations from WP to be manipulated through inference rules and sent, at any stage of the proof, to automatic (mainly SMT solvers) and interactive theorem provers. Some proof obligations may be proved automatically, while others can be too complex to be solved by automatic theorem provers, requiring the users of Frama-C and WP to handle them manually. This approach usually requires a signi cant experience in proof strategies. Some interactive theorem provers provide communication with automatic provers. However, this connection can be complex and incomplete, leaving the user with the manual proof option only. The strength of WPTrans is to combine the features of automatic and interactive theorem provers in a precise and complete way, with a simple manipulation language. Thus, the user can simplify the proof obligations enough in order for its proof to be concluded with an SMT solver, letting the proof be partially manual and partially automatic. Nevertheless, the plugin is directly linked do WP, facilitating the installation of the extension in Frama-C. This tool is also a gateway to other possible features, which we discuss herein.

Submitted by Automa??o e Estat?stica (sst@bczm.ufrn.br) on 2016-02-22T21:43:01Z No. of bitstreams: 1 PauloEwertonGomesFragoso_DISSERT.pdf: 1631728 bytes, checksum: 56a10da50e4f607b55bac9c065912a21 (MD5) / Approved for entry into archive by Arlan Eloi Leite Silva (eloihistoriador@yahoo.com.br) on 2016-02-23T23:34:33Z (GMT) No. of bitstreams: 1 PauloEwertonGomesFragoso_DISSERT.pdf: 1631728 bytes, checksum: 56a10da50e4f607b55bac9c065912a21 (MD5) / Made available in DSpace on 2016-02-23T23:34:33Z (GMT). No. of bitstreams: 1 PauloEwertonGomesFragoso_DISSERT.pdf: 1631728 bytes, checksum: 56a10da50e4f607b55bac9c065912a21 (MD5) Previous issue date: 2015-03-09 / Event-B ? um m?todo formal de modelagem e verifica??o de sistemas de transi??o discretos. O desenvolvimento com Event-B produz obriga??es de prova que devem ser verificadas, isto ?, ter sua validade verificada para manter a consist?ncia dos modelos produzidos. Solucionadores de Satisfatibilidade M?dulo Teoria s?o provadores autom?ticos de teoremas usados para verificar a satisfatibilidade de f?rmulas l?gicas considerando uma teoria (ou combina??o de teorias) subjacente. Solucionadores SMT n?o apenas lidam com f?rmulas extensas em l?gica de primeira ordem, como tamb?m podem gerar modelos e provas, bem como identificar subconjuntos insatisfat?veis de hip?teses (n?cleos insatisfat?veis). O suporte ferramental para Event-B ? provido pela Plataforma Rodin: um IDE extens?vel, baseado no framework Eclipse, que combina funcionalidades de modelagem e prova. Um plug-in SMT para Rodin tem sido desenvolvido com o objetivo de integrar ? plataforma t?cnicas alternativas e eficientes de verifica??o. Neste trabalho foi implementada uma s?rie de complementos ao plug-in para solucionadores SMT em Rodin, a saber, melhorias na interface do usu?rio para quando obriga??es de prova s?o reportadas como inv?lidas pelo plug-in. Adicionalmente, algumas caracter?sticas do plug-in, tais como suporte ? gera??o de provas e extra??o de n?cleo insatisfat?vel, foram modificadas de modo a tornaremse compat?veis com o padr?o SMT-LIB para solucionadores SMT. Realizaram-se testes utilizando obriga??es de prova aplic?veis para demonstrar as novas funcionalidades. As contribui??es descritas podem, potencialmente, afetar a produtividade de forma positiva. / 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.

Made available in DSpace on 2015-04-14T14:33:36Z (GMT). No. of bitstreams: 1 423927.pdf: 192175 bytes, checksum: 8f170ee02e27b9d198b57fc9c3dcdd0a (MD5) Previous issue date: 2010-03-30 / O tema central do presente trabalho ? a an?lise do dever fundamental de solidariedade social com rela??o ao Direito Tribut?rio. Inicialmente, demonstrou-se a exist?ncia de um dever fundamental de solidariedade social extra?do, de forma impl?cita, do Artigo 3?, inciso I, da Constitui??o Federal, segundo o qual a Rep?blica Federativa do Brasil constitui-se em um Estado Democr?tico de Direito, tendo como objetivo fundamental construir uma sociedade livre, justa e solid?ria. Ap?s, com base na doutrina nacional e estrangeira, identificou-se que a justifica??o para a institui??o de tributos n?o decorre de um Poder de Imp?rio, mas encontra fundamento na realiza??o dos direitos fundamentais, legitimado pelo dever fundamental de solidariedade social, advindo do fato de o contribuinte pertencer a uma sociedade organizada, em que todos t?m o dever de concorrer para as despesas p?blicas. Apurou-se que o dever fundamental de solidariedade social em rela??o aos tributos ? interpretado de forma diversa, dependendo da exist?ncia ou n?o de destina??o espec?fica aos recursos arrecadados com a sua institui??o. No caso dos impostos diretos, em que h? veda??o de destina??o espec?fica, a teor do Artigo 167, IV, da Constitui??o Federal de 1988, o dever fundamental de solidariedade social est? associado ao fato de o cidad?o pertencer a uma sociedade, tendo o dever de contribuir para todos os gastos p?blicos, respeitada a sua capacidade contributiva. Entretanto, com rela??o ?s contribui??es, em que h? previs?o de destina??o dos recursos arrecadados para um determinado grupo, aplica-se o dever fundamental de solidariedade social de grupo, que tem como base o fato de o contribuinte integrar o grupo eleito como respons?vel pelo pagamento da contribui??o, revertendo-se essa arrecada??o em benef?cio desse grupo. Assim, h? uma redistribui??o interna de recursos ?nica ressalva ?s contribui??es de Seguridade Social, que, por serem destinadas a toda a sociedade, ser?o, igualmente, financiadas por todos, na forma do Artigo 195, da Constitui??o Federal de 1988. Aplica-se, neste caso, o dever fundamental de solidariedade geral.

Made available in DSpace on 2015-04-14T14:33:52Z (GMT). No. of bitstreams: 1 437996.pdf: 163674 bytes, checksum: d05ddc21b2f151b8f11dd6ad528b9b0a (MD5) Previous issue date: 2012-03-13 / The present study has as its central theme the social role of taxation in the Democratic State of Law. Initially, a historical overview on the fundamentals of taxation has been presented, showing the evolution which took place throughout the different state models experienced. Then, some ethical features related to the tax activity have been pointed, specially the notions of fiscal justice and the redistribution of wealth, which must work as fundamentals for taxation. Afterwards, the evolution of the legal-tax thinking has been shown, this thinking has been considering taxation not as an end in itself anymore, based on the State sovereign power, but by the approach of its relation with the fundamental rights, increasingly more evident. After having presented general aspects relating to the principle of social role, the possibility of its application, also in the tax area, has been identified, taking into consideration the power taxation plays in society. In this sense, it has been shown that the tax activity plays an important role in the promotion and financing of the fundamental rights, being appropriate the implementation of mechanisms that favor the practice of this social role of taxation, such as the taking of extrafiscal measures. Subsequently, it has been found that in the Democratic State of Law, the payment of taxes represents a citizen true fundamental duty, which must contribute to the maintenance of the society he / she constitutes, based, among other factors, on the idea of social solidarity, constitutionally foreseen among the fundamental aims of the Federative Republic of Brazil. Concerning the social solidarity, it has been pointed out that, as a rule, it is applied to the extrafiscal taxes according to principle, which may trigger their decrease or increase; as to the fiscal taxes, the social solidarity is seen mostly through the principle of the contributive capacity; as to contributions, the group solidarity fundamental duty is applied , except for the contributions to the Social Security , in which the general social solidarity fundamental duty is applied. Through the analysis of concrete cases, it has been verified that the Brazilian High Courts have been adopting the notion of social solidarity in the tax area, helping the understanding that taxation plays a social role to be applied. / O presente estudo possui como tema central a fun??o social da tributa??o no Estado Democr?tico de Direito. Inicialmente, foi apresentado um panorama hist?rico acerca dos fundamentos da tributa??o, demonstrando-se a evolu??o ocorrida ao longo dos diferentes modelos estatais vivenciados. Ap?s, foram apontados alguns aspectos ?ticos envolvidos na atividade tribut?ria, em especial as no??es de justi?a fiscal e redistribui??o de riquezas, que devem servir como fundamentos para a tributa??o. Em seguida, demonstrou-se a evolu??o do pensamento jur?dico-tribut?rio, que vem considerando a tributa??o n?o mais como um fim em si mesma, com base no poder soberano do Estado, mas sim pelo enfoque de sua rela??o com os direitos fundamentais, cada vez mais evidente. Ap?s serem apresentados aspectos gerais relativos ao princ?pio da fun??o social, foi identificada a possibilidade de sua aplica??o tamb?m na seara tribut?ria, tendo em vista o alcance que a tributa??o possui na sociedade. Nesse sentido, demonstrou-se que a atividade tribut?ria possui um relevante papel na promo??o e financiamento dos direitos fundamentais, sendo cab?vel a implanta??o de mecanismos que privilegiam o exerc?cio dessa fun??o social da tributa??o, tais como a ado??o de medidas extrafiscais. Na sequ?ncia, apurou-se que no Estado Democr?tico de Direito o pagamento de tributos representa verdadeiro dever fundamental do cidad?o, que deve contribuir para a manuten??o da sociedade que comp?e, com base, entre outros fatores, na id?ia de solidariedade social, prevista constitucionalmente entre os objetivos fundamentais da Rep?blica Federativa do Brasil. Acerca da solidariedade social, destacou-se que, em regra, esta ? aplicada aos tributos extrafiscais na forma de princ?pio, o que pode ensejar a minora??o ou a majora??o dos mesmos; j? quanto aos tributos fiscais, manifesta-se sobretudo por meio do princ?pio da capacidade contributiva; no tocante ?s contribui??es, utiliza-se o dever fundamental de solidariedade de grupo, com exce??o das contribui??es para a Seguridade Social, ?s quais se aplica o dever fundamental de solidariedade social geral. Por meio da an?lise de casos concretos, verificou-se que os Tribunais Superiores brasileiros v?m adotando a no??o de solidariedade social na seara tribut?ria, contribuindo para o entendimento de que a tributa??o possui uma fun??o social a ser exercida.

Made available in DSpace on 2014-12-17T15:47:48Z (GMT). No. of bitstreams: 1 ClaudiaFCKT.pdf: 525104 bytes, checksum: 174fb60f1cf9ebfc609d837f2787b6b1 (MD5) Previous issue date: 2007-07-27 / 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