Reconstruímos a Teoria da Escolha Pública explicitando seus pressupostos sobre a natureza do objeto, do conhecimento e dos valores e sua lógica de operação, ou seja, seu método de solução de problemas. Mostramos com essa teoria que podemos entender a política como um processo de pacificação pela troca, em vez de um processo de pacificação pelo poder. Temos então novas respostas para as perguntas fundamentais da Ciência Política: Como é possível emergir a cooperação pacífica e legítima entre indivíduos? Qual é a maneira de fazer com que diferentes interesses individuais sejam reconciliados? A Teoria sugere que a política pode ser um jogo de soma positiva, evitando deseconomias constitucionais, guiando-se pelo princípio da unanimidade. Mostraremos então os desenhos constitucionais como ambientes de interação entre indivíduos e poderemos predizer que regras engendrarão cooperação ou competição. / We do a reconstruction of the Public Choice Theory explaining their assumptions about the nature of the object, knowledge and values and logic of their operation, i.e. its method of solution of problems. We show that with this theory we can understand the politics as a process of pacification through trade-offs, instead of a peace process by means of power. Proceeding in this way we obtain new answers to fundamental questions of Political Science: How can emerge a peaceful and legitimate cooperation among individuals? What is the way to conciliate different individual interests? The theory suggests that politics can be a positive-sum game, avoiding constitutional diseconomies, and must be guided by the principle of unanimity. Then we show how the constitutional designs as interaction environments for individuals and so can predict what rules make cooperation or competition.

Made available in DSpace on 2014-12-17T13:57:10Z (GMT). No. of bitstreams: 1 JulianaMM_cap1_cap5.pdf: 5537131 bytes, checksum: 02fbf19992b55864367640039cddacc1 (MD5) Previous issue date: 2012-03-12 / The goal of the research was to investigate the energy performance of residential vertical buildings envelope in the hot and humid climate of Natal, capital of Rio Grande do Norte, based in the Technical Regulation of Quality for Energy Efficiency Level in Residential Buildings (RTQ -R), launched in 2010. The study pretends to contribute to the development of design strategies appropriate to the specific local climate and the increasing of energy efficiency level of the envelope. The methodological procedures included the survey in 22 (twenty two) residential buildings, the formulation of representative prototypes based on typological and constructives characters researched and the classification of the level of energy efficiency in the envelopment of these prototypes, using as a tool the prescriptive method of the RTQ-R and the parametric analyzes from assigning different values of the following variables: shape of the pavement type; distribution of housing compartments; orientation of the building; area and shading of openings; thermal transmittance, and solar absorptance of opaque materials of the frontage in order to evaluate the influence of these on the envelopment performance. The main results accomplished with this work includes the qualification of vertical residential buildings in Natal/RN; the verification of the adequacy of these buildings to local climate based from the diagnosis of the thermal energy of the envelopment performance, the identification of variables with more significant influence on the prescriptive methodology of RTQ-R and design solutions more favorable to obtain higher levels energy efficiency by this method. Finally, it was verified, that some of these solutions proved contradictory in relation to the recommendations contained in the theoretical approaches regarding environmental comfort in hot and humid weather, which indicates the need for improvement of the prescriptive method RTQ-R and further research on efficient design solutions / O objetivo desta pesquisa foi investigar o desempenho energ?tico da envolt?ria de edif?cios residenciais verticais no clima quente e ?mido de Natal, capital do estado do Rio Grande do Norte, ? luz do Regulamento T?cnico de Qualidade para o N?vel de Efici?ncia Energ?tica de Edifica??es Residenciais (RTQ-R), lan?ado em 2010. O trabalho procura contribuir para o desenvolvimento de estrat?gias projetuais adequadas ?s especificidades clim?ticas locais e ao aumento do n?vel de efici?ncia energ?tica da envolt?ria. Os procedimentos metodol?gicos inclu?ram o levantamento em 22 (vinte e dois) edif?cios residenciais, a formula??o de prot?tipos representativos com base em caracter?sticas tipol?gicas e construtivas levantadas e a classifica??o do n?vel de efici?ncia energ?tica (etiquetagem) da envolt?ria destes prot?tipos, utilizando como ferramenta o m?todo prescritivo do RTQ-R e an?lises param?tricas a partir da atribui??o de diferentes valores ?s seguintes vari?veis: forma do pavimento tipo; distribui??o dos ambientes na habita??o; orienta??o da edifica??o; ?rea e sombreamento das aberturas; transmit?ncia t?rmica; e, absort?ncia solar dos materiais opacos da fachada, a fim de avaliar a influ?ncia destes no desempenho da envolt?ria. Os principais resultados alcan?ados com a realiza??o deste trabalho compreenderam a qualifica??o dos edif?cios residenciais verticais em Natal/RN; a verifica??o da adequa??o destes edif?cios ? realidade clim?tica local a partir do diagn?stico do desempenho termo-energ?tico da envolt?ria; a identifica??o das vari?veis com influ?ncia mais significativa sobre a metodologia prescritiva do RTQ-R e de solu??es projetuais mais favor?veis ? obten??o de n?veis mais altos de efici?ncia energ?tica segundo este m?todo. Verificou-se, finalmente, que algumas destas solu??es mostraram-se contradit?rias em rela??o ?s recomenda??es consagradas nas abordagens te?ricas relativas ao conforto ambiental no clima quente e ?mido, o que indica a necessidade de aperfei?oamento do m?todo prescritivo do RTQ-R e o aprofundamento em pesquisas sobre solu??es projetuais eficientes

Made available in DSpace on 2014-12-17T14:27:22Z (GMT). No. of bitstreams: 1 CiceroMMF.pdf: 943759 bytes, checksum: a4d4b3d4603827397cb5504723a780b0 (MD5) Previous issue date: 2006-08-21 / This document approaches the formal and material limits of the constitucionalidade control for the Supreme Federal Court, iniating with the study of the Constitution, detaching its evolution, nature and meanings, passing for its historical evolution, offering still a unconstitutionality concept. Is work the principles as material Constitution, making the distinction entere principles and rules, detaching the characteristics of the principles constitutional, and the basic principle of the Constituition. It analyzes metodologics the historical parameters and of the brazilian system of constitutionality control and detaches the paper of the Supreme Federal Court as positive legislator. It observes the beddings of the constitutionality control and the legitimacy of the Supreme Federal Court. Is examines the performance of the Supreme Federal Court in face of the principle of the legal security. Is offers a vision on the experience of the control of constitutionality in other constries. It still approaches the control of constitutionality in Brazil, detaching the critical points of its formal and material limits. Is verifies the application of the principles constitutional for the Supreme Federal Court in the diffuse control and the intent control of constitutionality, as well as the performance of the Supreme Federal Court ahead of the unconstitutional omissions. It brings to the debate the new perspectives how much to the formal and material limits of the control of constitutionality for the Supreme Federal Court. Objective to elaborate considerations concerning the limits of the constitutional jurisdiction from the model of Constituition, the character politican of the difficulties with respect to the definition of its formal and material limits from the performance of the Supreme Federal Court / Este trabalho aborda os limites formais e materiais do controle de constitucionalidade pelo Supremo Tribunal Federal, iniciando com o estudo da Constitui??o, destacando sua evolu??o, natureza e significados, passando por sua evolu??o hist?rica, oferecendo ainda um conceito de inconstitucionalidade. Trabalha os princ?pios como Constitui??o material, fazendo a distin??o entre princ?pios e regras, destacando as caracter?sticas dos princ?pios constitucionais e os princ?pios fundamentais da Constitui??o. Analisa os par?metros hist?ricos e metodol?gicos do sistema brasileiro de controle de constitucionalidade e destaca o papel do Supremo Tribunal Federal como legislador positivo. Observa os fundamentos do controle de constitucionalidade e a legitimidade do Supremo Tribunal Federal. Examina a atua??o do Supremo Tribunal Federal em face do princ?pio da seguran?a jur?dica. Oferece uma vis?o sobre a experi?ncia do controle de constitucionalidade em outros pa?ses. Aborda ainda o controle de constitucionalidade no Brasil, destacando os pontos cr?ticos dos seus limites formais e materiais. Verifica a aplica??o dos princ?pios constitucionais pelo Supremo Tribunal Federal no controle difuso e no controle concentrado de constitucionalidade, bem como a atua??o do Supremo Tribunal Federal diante das omiss?es inconstitucionais. Traz ao debate as novas perspectivas quanto aos limites formais e materiais do controle de constitucionalidade pelo Supremo Tribunal Federal. Objetiva elaborar considera??es acerca dos limites da jurisdi??o constitucional a partir do modelo de Constitui??o, o car?ter pol?tico da jurisdi??o constitucional, e finaliza apontando as dificuldades para a defini??o dos seus limites formais e materiais a partir da atua??o do Supremo Tribunal Federal

Made available in DSpace on 2015-03-03T15:47:45Z (GMT). No. of bitstreams: 1 ValerioGMJpdf.pdf: 1265506 bytes, checksum: f1fe3ef975bfeb2fce1dad3319a33f34 (MD5) Previous issue date: 2009-09-09 / This work shows a project method proposed to design and build software components from the software functional m del up to assembly code level in a rigorous fashion. This method is based on the B method, which was developed with support and interest of British Petroleum (BP). One goal of this methodology is to contribute to solve an important problem, known as The Verifying Compiler. Besides, this work describes a formal model of Z80 microcontroller and a real system of petroleum area. To achieve this goal, the formal model of Z80 was developed and documented, as it is one key component for the verification upto the assembly level. In order to improve the mentioned methodology, it was applied on a petroleum production test system, which is presented in this work. Part of this technique is performed manually. However, almost of these activities can be automated by a specific compiler. To build such compiler, the formal modelling of microcontroller and modelling of production test system should provide relevant knowledge and experiences to the design of a new compiler. In ummary, this work should improve the viability of one of the most stringent criteria for formal verification: speeding up the verification process, reducing design time and increasing the quality and reliability of the product of the final software. All these qualities are very important for systems that involve serious risks or in need of a high confidence, which is very common in the petroleum industry / Este trabalho apresenta um m?todo de projeto proposta para veri ca??o formal do modelo funcional do software at? o n?vel da linguagem assembly. Esse m?todo ? fundamentada no m?todo B, o qual foi desenvolvido com o apoio e interesse da multinacional do setor de petr?leo e g?s British Petroleum (BP). A evolu??o dessa metodologia tem como objetivo contribuir na resposta de um importante problema, que pertence aos grandes desa os da computa??o, conhecido como The Verifying Compiler . Nesse contexto, o presente trabalho descreve um modelo formal do microcontrolador Z80 e um sistema real da ?rea de petr?leo. O modelo formal do Z80 foi desenvolvido e documentado, por ser um pr?-requisito para a veri ca??o at? n?vel de assembly. A m de validar e desenvolver a metodologia citada, ela foi aplicada em um sistema de teste de produ??o de po?os de petr?leo, o qual ? apresentado neste trabalho. Atualmente, algumas atividades s?o realizadas manualmente. No entanto, uma parte signifi cativa dessas atividades pode ser automatizada atrav?s de um compilador espec?fi co. Para esse m, a modelagem formal do microcontrolador e a modelagem do sistema de teste de produ??o fornecem conhecimentos e experi?ncias importantes para o projeto de um novo compilador. Em suma, esse trabalho deve melhorar a viabilidade de um dos mais rigorosos crit?rios de veri ca??o formal: acelerando o processo de verifica??o, reduzindo o tempo de projeto e aumentando a qualidade e con fian?a do produto de software final. Todas essas qualidades s?o bastante relevantes para sistemas que envolvem s?rios riscos ou exigem alta confian?a, os quais s?o muito comuns na ind?stria do petr?leo

Submitted by Automa??o e Estat?stica (sst@bczm.ufrn.br) on 2017-03-09T18:47:46Z No. of bitstreams: 1 MadielDeSouzaConservaFilho_TESE.pdf: 1314650 bytes, checksum: ea38672191d7c35f5274cb1360bcfef1 (MD5) / Approved for entry into archive by Arlan Eloi Leite Silva (eloihistoriador@yahoo.com.br) on 2017-03-10T21:13:38Z (GMT) No. of bitstreams: 1 MadielDeSouzaConservaFilho_TESE.pdf: 1314650 bytes, checksum: ea38672191d7c35f5274cb1360bcfef1 (MD5) / Made available in DSpace on 2017-03-10T21:13:38Z (GMT). No. of bitstreams: 1 MadielDeSouzaConservaFilho_TESE.pdf: 1314650 bytes, checksum: ea38672191d7c35f5274cb1360bcfef1 (MD5) Previous issue date: 2016-08-12 / O uso crescente de sistemas complexos exige cada vez mais um maior investimento de recursos no desenvolvimento de software para garantir a confiabilidade dos mesmos. Para lidar com esta complexidade, abordagens composicionais podem ser utilizadas no desenvolvimento de sistemas de software, possibilitando a integra??o e a reutiliza??o de componentes existentes. Entretanto, a fim de garantir o sucesso desta abordagem, ? essencial confiar no comportamento dos componentes e, al?m disso, nos sistemas que s?o desenvolvidos utilizando essa estrat?gia, uma vez que falhas podem ser introduzidas se a composi??o n?o assegurar propriedades importantes. Problemas podem surgir quando dois ou mais componentes s?o integrados pela primeira vez. Esta situa??o ? ainda mais relevante quando um grupo de componentes trabalha em conjunto a fim de executar determinadas tarefas, especialmente em aplica??es cr?ticas, onde podem surgir problemas cl?ssicos, como livelock. Esta tese de doutorado apresenta uma estrat?gia local para garantir aus?ncia de livelock, por constru??o, em sistemas s?ncronos modelados com a nota??o padr?o de CSP. A nossa t?cnica ? baseada na an?lise local das m?nimas sequ?ncias que levam o processo CSP ao seu estado inicial. O uso de t?cnicas locais evita a explos?o do espa?o de estados gerado pela integra??o dos componentes. A verifica??o destas condi??es locais utilizam metadados que permitem armazenar resultados parciais das verifica??es, reduzindo o esfor?o durante a an?lise. A abordagem proposta tamb?m pode ser aplicada para verificar aus?ncia de livelock em modelos que realizam comunica??es ass?ncronas. Neste caso, analisamos o modelo de componentes BR IC, cujo comportamento dos componentes ? representado por um processo CSP. A fim de realizar esta verifica??o, consideramos duas vers?es para BR IC: BR IC , o qual realiza composi??es ass?ncronas atrav?s de buffers finitos, e BR IC? no qual a assincronicidade ? realizada atrav?s de buffers infinitos. Estas duas abordagens foram analisadas porque a possibilidade de introduzir livelock em sistemas ass?ncronos depende diretamente da finitude do buffer. As t?cnicas propostas para garantir aus?ncia de livelock em CSP e BR IC foram avaliadas atrav?s de tr?s estudos de caso: o escalonador de Milner e duas varia??es do jantar dos fil?sofos. Uma vers?o apresenta um sistema livre de livelock, e a outra apresenta um sistema com livelock. Neste estudo, avaliamos a nossa abordagem em compara??o com outras duas t?cnicas para verifica??o de aus?ncia de livelock, a an?lise global tradicional do FDR e a an?lise est?tica de livelock do SLAP. Este estudo comparativo demonstra que a nossa estrat?gia pode ser aplicada como uma alternativa para a verifica??o de aus?ncia de livelock em grandes sistemas. / The use of increasingly complex applications is demanding a greater investment of resources in software development to ensure that applications are safe. For mastering this complexity, compositional approaches can be used in the development of software by integrating and reusing existing reliable components. The correct application of such strategies, however, relies on the trust in the behaviour of the components and in the emergent behaviour of the composed components because failures may arise if the composition does not preserve essential properties. Problems may be introduced when two or more error-free components are integrated for the first time. This concern is even more relevant when a group of components is put together in order to perform certain tasks, especially in safety-critical applications, during which classical problems can arise, such as livelock. In this thesis, we present a local strategy that guarantees, by construction, the absence of livelock in synchronous systems as modelled using the standard CSP notation. Our method is based solely on the local analysis of the minimum sequences that lead the CSP model back to its initial state. Locality provides an alternative to circumvent the state explosion generated by the interaction of components and allows us to identify livelock before composition. The verification of these conditions use metadata that allow us to record partial results of verification, decreasing the overall analysis effort. In addition, our work can also be applied to check livelock freedom in models that perform asynchronous communications. In this case, we carry out livelock analysis in the context of a component model, BR IC, whose behaviour of the components is described as a CSP process. Finally, we introduce three case studies to evaluate our livelock analysis technique in practice: the Milner?s scheduler and two variations of the dining philosophers, a livelock-free version and a version in which we have deliberately included livelock. For each case study, we also present a comparative analysis of the performance of our strategy with two other techniques for livelock freedom verification, the traditional global analysis of FDR and the static livelock analysis of SLAP. This comparative study demonstrates that our strategy can be used in practice and that it might be a useful alternative for establishing livelock freedom in large systems.

A evolução de sistemas de gerenciamento de tráfego aéreo é pesquisada para suportar o crescimento na demanda por transporte aéreo. Uma alternativa para essa evolução é o aumento no grau de automação. Os sistemas automatizados precisam ser tão seguros quanto os sistemas em operação atualmente. Com o uso de técnicas de especificação e verificação formal é possível avaliar os requisitos de sistemas. Neste trabalho, é proposto um ciclo de especificação formal, que consiste em um conjunto de diretrizes para aplicação de técnicas de métodos formais em requisitos escritos em linguagem natural. O resultado esperado da aplicação deste ciclo é um conjunto de requisitos escritos em linguagem natural verificados formalmente. O ciclo é composto pelas etapas: levantamento de requisitos do sistema e classificação em padrões de especificação; mapeamento dos requisitos para as linguagens de especificação formal LTL (Linear Temporal Logic) e CTL (Computation Tree Logic); verificação formal da especificação com o verificador NuSMV; ajustes na especificação baseada nos resultados da verificação; ajustes nos requisitos baseados nos ajustes na especificação. As diretrizes propostas são definidas com a análise da verificação formal do Automated Airspace Concept (AAC), padrões de especificação e diretrizes para uso do verificador NuSMV. Os resultados esperados são obtidos na aplicação do ciclo de especificação em dois estudos de caso. A principal contribuição do trabalho é o conjunto de diretrizes para elaboração de expressões escritas em linguagem de especificação formal baseadas em requisitos escritos em linguagem natural e que podem ser verificadas formalmente. / Air traffic management systems evolution is being researched to support air transportation demand growth. An evolution alternative is system automation degree increase. Automated systems need to be as safe as current operating systems. It is possible to analyze system requirements with the application of formal specification and formal verification techniques. In this work, a specification cycle is proposed. The specification cycle is a set of guidelines to use formal method techniques on requirements written in natural language. The specification cycle application expected result is a set of formally verified requirements written in natural language. This cycle is comprised of the following stages: system requirements elicitation and specification pattern classification; requirements mapping to LTL (Linear Temporal Logic) and CTL (Computation Tree Logic) formal specification languages; specification formal verification using the NuSMV verifier; formal specification adjustment based on verification results; requirements adjustment based on formal specification adjustment. The proposed guidelines are defined with the Automated Airspace Concept (AAC) formal verification analysis, specification patterns and guidelines for the NuSMV formal verifier use. The expected results are accomplished in the specification cycle application on two study cases. The main contribution of this work is the set of guidelines applied to formulate formally verifiable expressions specified in formal specification languages based on system requirements written in natural language.

O avanço tecnológico recente tem atraído tanto a comunidade acadêmica quanto o mercado para a investigação de novos métodos, técnicas e linguagens formais para a área de Projeto de Engenharia. A principal motivação é o atendimento à demanda para desenvolver produtos e sistemas cada vez mais completos e que satisfaçam as necessidades do usuário final. Necessidades estas que podem estar ligadas, por exemplo, à análise e reconhecimento de objetos que compõe uma imagem pela sua textura, um processo essencial na automação de uma enorme gama de aplicações como: visão robótica, monitoração industrial, sensoriamento remoto, segurança e diagnóstico médico assistido. Em vista da relevância das inúmeras aplicações envolvidas e pelo fato do domínio de aplicação ser muito próximo do contexto do desenvolvedor, é apresentada uma proposta de um processo de design baseado no Projeto Axiomático como sendo o mais indicado para esta situação. Especificamente, se espera que no estudo de caso da análise de textura haja uma convergência mais rápida para a solução - se esta existir. No estudo de caso, se desenvolve uma nova concepção de arquitetura de rede neural artificial (RNA), auto-organizável, com a estrutura espacial bidimensional da imagem de entrada preservada, tendo a extração e reconhecimento/classificação de textura em uma única fase de aprendizado. Um novo conceito para o paradigma da competição entre os neurônios também é estabelecida. O processo é original por permitir que o desenvolvedor assuma concomitantemente o papel do cliente no projeto, e especificamente por estabelecer o processo de sistematização e estruturação do raciocínio lógico do projetista para a solução do problema a ser desenvolvido e implementado em RNA. / The recent technological advance has attracted the industry and the academic community to research and propose methods, seek for new techniques, and formal languages for engineering design in order to respond to the growing demand for sophisticated product and systems that fully satisfy customers needs. It can be associated, for instance, with an application of object recognition using texture features, essential to a variety of applications domains, such as robotic vision, industrial inspection, remote sensing, security and medical image diagnosis. Considering the importance of the large number of applications mentioned before, and due to their characteristic where both application and developer domain are very close to each other, this work aims to present a design process based on ideas extracted from axiomatic design to accelerate the development for the classical approach to texture analysis. Thus, a case study is accomplished where a new conception of neural network architecture is specially designed for the following proposal: preserving the two-dimensional spatial structure of the input image, and performing texture feature extraction and classification within the same architecture. As a result, a new mechanism for neuronal competition is also developed as specific knowledge for the domain. In fact, the process proposed has some originality because it does take into account that the developer assumes also the customers role on the project, and establishes the systematization process and structure of logical reasoning of the developer in order to develop and implement the solution in neural network domain.

Orientador: Arnaldo Vieira Moura / Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Computação / Made available in DSpace on 2018-08-16T21:26:35Z (GMT). No. of bitstreams: 1 Pedrosa_LehiltonLelisChaves_M.pdf: 884292 bytes, checksum: e39efddad6809b28790b661469a5cfd2 (MD5) Previous issue date: 2010 / Resumo: Métodos formais são amplamente utilizados para modelar especificações e gerar casos de testes, imprescindíveis para validação de sistemas críticos. As Máquinas de Estados Finitos (MEFs) compõem um dos formalismos adotados, com várias aplicações em testes de sistemas aéreos e espaciais, além de sistemas médicos, entre vários outros. O objetivo de um método de geração automática de casos de testes é obter um conjunto de casos de testes, com o qual é possível verificar se uma dada implementação contém falhas. Um problema importante em métodos de geração de casos de teste com cobertura completa de falhas é o tamanho dos conjuntos de testes, que normalmente é exponencial no número de estados da MEF que está sendo testada. Para minimizar esse problema, diversas abordagens são adotadas, envolvendo melhorias nos métodos existentes, restrições do modelo de falhas e o uso de novas estratégias de teste. Esta dissertação estuda métodos automáticos para geração de casos de testes com cobertura completa de falhas e propõe dois novos métodos, que permitem reduzir o tamanho dos conjuntos de testes gerados. Primeiro, combinamos ideias do método Wp e do método G, visando usufruir as vantagens de ambos e obtendo um novo método, denominado Gp. Em seguida, descrevemos um novo modelo de falhas para sistemas compostos de vários subsistemas, possivelmente com um número alto de estados. Formalizamos tais sistemas, introduzindo o conceito de MEFs combinadas, e apresentamos um novo método de testes, denominado método C. Além disso, propomos uma abordagem de testes incremental, baseada no método C, que torna possível o teste de MEFs com um número arbitrário de estados. Estabelecemos comparações com abordagens tradicionais e mostramos que o uso da estratégia incremental pode gerar conjuntos de testes exponencialmente mais eficientes / Mestrado / Teoria da Computação / Mestre em Ciência da Computação

Orientador: Marcelo Esteban Coniglio / Dissertação (mestrado) - Universidade Estadual de Campinas, Instituto de Filosofia e Ciencias Humanas / Made available in DSpace on 2018-08-17T03:29:03Z (GMT). No. of bitstreams: 1 Rodrigues_TarcisioGenaro_M.pdf: 1141020 bytes, checksum: 59bb8a3ae7377c05cf6a8d8e6f7e45a5 (MD5) Previous issue date: 2010 / Resumo: A Programação Lógica nasce da interação entre a Lógica e os fundamentos da Ciência da Computação: teorias de primeira ordem podem ser interpretadas como programas de computador. A Programação Lógica tem sido extensamente utilizada em ramos da Inteligência Artificial tais como Representação do Conhecimento e Raciocínio de Senso Comum. Esta aproximação deu origem a uma extensa pesquisa com a intenção de definir sistemas de Programação Lógica paraconsistentes, isto é, sistemas nos quais seja possível manipular informação contraditória. Porém, todas as abordagens existentes carecem de uma fundamentação lógica claramente definida, como a encontrada na programação lógica clássica. A questão básica é saber quais são as lógicas paraconsistentes subjacentes a estas abordagens. A presente dissertação tem como objetivo estabelecer uma fundamentação lógica e conceitual clara e sólida para o desenvolvimento de sistemas bem fundados de Programação Lógica Paraconsistente. Nesse sentido, este trabalho pode ser considerado como a primeira (e bem sucedida) etapa de um ambicioso programa de pesquisa. Uma das teses principais da presente dissertação é que as Lógicas da Inconsistência Formal (LFI's), que abrangem uma enorme família de lógicas paraconsistentes, proporcionam tal base lógica. Como primeiro passo rumo à definição de uma programação lógica genuinamente paraconsistente, demonstramos nesta dissertação uma versão simplificada do Teorema de Herbrand para uma LFI de primeira ordem. Tal teorema garante a existência, em princípio, de métodos de dedução automática para as lógicas (quantificadas) em que o teorema vale. Um pré-requisito fundamental para a definição da programação lógica é justamente a existência de métodos de dedução automática. Adicionalmente, para a demonstração do Teorema de Herbrand, são formuladas aqui duas LFI's quantificadas através de sequentes, e para uma delas demonstramos o teorema da eliminação do corte. Apresentamos também, como requisito indispensável para os resultados acima mencionados, uma nova prova de correção e completude para LFI's quantificadas na qual mostramos a necessidade de exigir o Lema da Substituição para a sua semântica / Abstract: Logic Programming arises from the interaction between Logic and the Foundations of Computer Science: first-order theories can be seen as computer programs. Logic Programming have been broadly used in some branches of Artificial Intelligence such as Knowledge Representation and Commonsense Reasoning. From this, a wide research activity has been developed in order to define paraconsistent Logic Programming systems, that is, systems in which it is possible to deal with contradictory information. However, no such existing approaches has a clear logical basis. The basic question is to know what are the paraconsistent logics underlying such approaches. The present dissertation aims to establish a clear and solid conceptual and logical basis for developing well-founded systems of Paraconsistent Logic Programming. In that sense, this text can be considered as the first (and successful) stage of an ambitious research programme. One of the main thesis of the present dissertation is that the Logics of Formal Inconsistency (LFI's), which encompasses a broad family of paraconsistent logics, provide such a logical basis. As a first step towards the definition of genuine paraconsistent logic programming we shown, in this dissertation, a simplified version of the Herbrand Theorem for a first-order LFI. Such theorem guarantees the existence, in principle, of automated deduction methods for the (quantified) logics in which the theorem holds, a fundamental prerequisite for the definition of logic programming over such logics. Additionally, in order to prove the Herbrand Theorem we introduce sequent calculi for two quantified LFI's, and cut-elimination is proved for one of the systems. We also present, as an indispensable requisite for the above mentioned results, a new proof of soundness and completeness for first-order LFI's in which we show the necessity of requiring the Substitution Lemma for the respective semantics / Mestrado / Filosofia / Mestre em Filosofia

Analyzes in an open and exploratory as seniors who reside in long-stay institutions in the municipalities of Arapiraca-AL and Caruaru-PE represent old age and life institutionalized. Therefore, traces a characterization of the process of demographic transition and seeks to place the impact of this process on the expansion of demand for formal long-term care in Brazil and especially in cities where the institutions surveyed included. Observes how the process of demographic transition is accompanied by a decrease in the availability of family caregivers and how the expansion of demand for long-term care requires a redefinition of the distribution of roles among family, society and state in the provision of care. Discusses the approach of Norbert Elias about the process of concealment of death and dying that would have developed in northern European societies in the course of the civilizing process and seeks to show how dependent old age still produce feelings of shame and embarrassment that hinder identification with the old and the dying. Finally, assess how the subjects represent the old age and the life institutionalized and inquire about the possibility of reconciling the representations produced in the context of characterization of the dying of loneliness that is presented in the Elia’s work / FAPEAL - Fundação de Amparo à Pesquisa do Estado de Alagoas / Esse estudo analisa de forma aberta e exploratória como idosos que residem em instituições de longa permanência nos municípios de Arapiraca-Al e Caruaru-PE representam a velhice e a vida institucionalizada. Para tanto, traça uma caracterização do processo de transição demográfica e procura situar os impactos desse processo na ampliação da demanda por cuidados formais de longa duração no Brasil e em especial nas cidades onde figuram as instituições pesquisadas. Observa como o processo de transição demográfica é acompanhado de uma diminuição da disponibilidade de cuidadores familiares e como a ampliação da demanda por cuidados de longa duração exige uma redefinição da distribuição de papéis entre família, sociedade, mercado e Estado na oferta desses cuidados. Discorre sobre a abordagem eliasiana acerca do processo de ocultação da morte e dos moribundos que teria se desenvolvido nas sociedades norte europeias no curso do processo civilizador e procura indicar como a velhice dependente ainda produziria sentimentos de vergonha e embaraço que dificultariam a identificação com os velhos e os moribundos. Por fim, avalia como os sujeitos da pesquisa representaram a velhice e a vida institucionalizada e inquire sobre a possibilidade de compatibilizar as representações produzidas no quadro de caracterização da solidão dos moribundos que é apresentado na obra eliasiana.