O presente trabalho possui preponderantemente a natureza de pesquisa teórica, sem, contudo, olvidar-se aspectos empíricos, documentais e históricos. As múltiplas naturezas decorrem da relevância dos fundamentos teóricos e do caráter imprescindível dos documentos existentes e da história por de trás das normas pertinentes. O objetivo desta pesquisa foi a busca de um critério jurídico que sirva como alternativa à solução ofertada pelo Tribunal Superior do Trabalho por meio da Súmula n.º 363 aos empregados que prestem trabalhos à Administração Pública à míngua de prévia aprovação em concurso público. Pretendeu-se demonstrar a necessidade de se diferenciar os trabalhadores que ignoram a prestação de trabalho para a Administração Pública daquelas que têm conhecimento da natureza jurídica de seu empregador em um cenário em que o concurso público é pressuposto formal sem o qual o ato jurídico que vincula os sujeitos da relação de emprego é invalido. Como referências teóricas foram utilizadas a teoria geral do Direito do Trabalho, em especial dos contratos de trabalho, a teoria geral dos atos jurídicos, nomeadamente as teorias da nulidade e da ineficácia, a ponderação de princípios, a harmonização de princípios, a boa-fé e, ainda, a teoria geral da prova em razão das repercussões processuais do estudo. Por fim, como resultado, demonstrou-se que a utilização da boa-fé como critério diferenciador da concessão de direitos aos empregados que trabalhem para a Administração Pública sem a prévia aprovação em concurso público proporciona harmonização entre o princípio do valor social do trabalho e os princípios regentes da Administração Pública. / This work has mainly the nature of theoretical research, without, however, forgetting is empirical aspects, and historical documentary. The multiple natures derive the relevance of the theoretical and the essential nature of existing documents and the story behind the relevant standards. The aim of this study was to search for a legal test that serves as an alternative to the solution offered by the Superior Labor Court by Precedent n. 363 employees who provide jobs to government starved prior approval in tender. It was intended to demonstrate the need to differentiate Worker who ignore the provision of work for the Public Administration of those who have knowledge of the legal nature of their employer in a scenario in which the tender is formal assumption without which the legal act that binds the subject of the employment relationship is invalid. Theoretical references were used the general theory of labor law, especially of labor contracts, the general theory of legal acts, including the theories of invalidity and ineffectiveness, the weighting of principles, harmonization of principles, good faith and also the general theory of proof because of the procedural implications of the study. Finally, as a result, it was shown that the use of good faith as a differentiating criterion for granting rights to employees who work for the Public Administration without prior approval in tender offers harmonization between the principle of the social value of work and governing principles of public administration.

Made available in DSpace on 2015-03-03T15:47:47Z (GMT). No. of bitstreams: 1 PatrickCAT_DISSERT.pdf: 4794202 bytes, checksum: 05088b21ff2be2b3c2ccec958e7e6b62 (MD5) Previous issue date: 2013-06-03 / Logic courses represent a pedagogical challenge and the recorded number of cases of failures and of discontinuity in them is often high. Amont other difficulties, students face a cognitive overload to understand logical concepts in a relevant way. On that track, computational tools for learning are resources that help both in alleviating the cognitive overload scenarios and in allowing for the practical experimenting with theoretical concepts. The present study proposes an interactive tutorial, namely the TryLogic, aimed at teaching to solve logical conjectures either by proofs or refutations. The tool was developed from the architecture of the tool TryOcaml, through support of the communication of the web interface ProofWeb in accessing the proof assistant Coq. The goals of TryLogic are: (1) presenting a set of lessons for applying heuristic strategies in solving problems set in Propositional Logic; (2) stepwise organizing the exposition of concepts related to Natural Deduction and to Propositional Semantics in sequential steps; (3) providing interactive tasks to the students. The present study also aims at: presenting our implementation of a formal system for refutation; describing the integration of our infrastructure with the Virtual Learning Environment Moodle through the IMS Learning Tools Interoperability specification; presenting the Conjecture Generator that works for the tasks involving proving and refuting; and, finally to evaluate the learning experience of Logic students through the application of the conjecture solving task associated to the use of the TryLogic / A disciplina de L?gica representa um desa o tanto para docentes como para discentes, o que em muitos casos resulta em reprova??es e desist?ncias. Dentre as dificuldades enfrentadas pelos alunos est? a sobrecarga da capacidade cognitiva para compreender os conceitos l?gicos de forma relevante. Neste sentido, as ferramentas computacionais de aprendizagem s?o recursos que auxiliam a redu??o de cen?rios de sobrecarga cognitiva, como tamb?m permitem a experi?ncia pr?tica de conceitos te?ricos. O presente trabalho prop?e uma tutorial interativo chamado TryLogic, visando ao ensino da tarefa de Demonstra??o ou Refuta??o (DxR) de conjecturas l?gicas. Trata-se de uma ferramenta desenvolvida a partir da arquitetura do TryOcaml atrav?s do suporte de comunica??o da interface web ProofWeb para acessar o assistente de demonstra??o de teoremas Coq. Os objetivos do TryLogic s?o: (1) Apresentar um conjunto de li??es para aplicar estrat?gias heur?sticas de an?lise de problemas em L?gica Proposicional; (2) Organizar em passo-a-passo a exposi ??o dos conte?dos de Dedu??o Natural e Sem?ntica Proposicional de forma sequencial; e (3) Fornecer aos alunos tarefas interativas. O presente trabalho prop?e tamb?m apresentar a nossa implementa??o de um sistema formal de refuta??o; descrever a integra??o de nossa infraestrutura com o Ambiente Virtual de Aprendizagem Moodle atrav?s da especi ca??o IMS Learning Tools Interoperability ; apresentar o Gerador de Conjecturas de tarefas de Demonstra??o e Refuta??o e, por m, avaliar a experi?ncia da aprendizagem de alunos de L?gica atrav?s da aplica??o da tarefa de DxR em associa??o ? utiliza??o do TryLogic

Tendo como premissas a conformação constitucional do Estado de Direito e das garantias processuais, este estudo pretende ser uma contribuição à dicsussão acerca da utilização da prova pericial, sua admissibilidade, valoração controle, no sistema processual brasileiro. O Estado Democrático de Direito impõe aos seus agentes a motivação, não somente das decisões judiciais, mas de todos os atos que tenham cunho decisório, e imponham alguma restrição, por menor que seja, à liberdade do indivíduo. Por sua vez, o contraditório, expressão do princípio político da participação democrática, afirma a necessidade de possibilitar a participação do indivíduo na formação de uma decisão que afete sua esfera de interesses. A orientação do processo como instrumento a serviço da realização da justiça, e da construção de decisões justas, pressupõe o correto acertamento da verdade fática. Isto impõe que seja adotada uma concepção do fenômeno probatório que a compreenda como um instrumento demonstrativo e epistemológico. Nessa perspectiva, a utilização da prova pericial, especialmente aquelas que se revestem de cunho científico, se mostra um eficaz meio da obtenção da verdade no processo, desde que, tais provas sejam relevantes e confiáveis, demonstrando a necessidade de seu controle. / Taking as premises the conformation of the constitutional rule of law and procedural safeguards, this study is a contribution to the dicsussion about the use of expert evidence, its admissibility, and valuation control, at the Brazilian procedural system. The Democratic State imposes on its agents the motivation, not only of judgments, but of all the acts that have decision-making matrix, and impose some restrictions, however small, in the freedom of the individual. In turn, the contradictory, expression of political principle of democratic participation, says the need to enable participation of the individual in forming a decision that affects their area of interest. The orientation of the process as a tool in the service of achieving justice, and the construction of fair decisions, presupposes a correct assertion of factual truth. This requires that adopted a conception of the phenomenon that the evidence as a tool to understand and epistemological statement. From this perspective, the use of expert testimony, especially those which are of a scientific nature, proves an effective means of obtaining the truth in the process, provided that such evidence is relevant and reliable, demonstrating the need for its control.

Entre as cinco provas da existência de Deus que Tomás de Aquino apresentou na Summa Theologiae, sobressai a chamada “primeira via”, considerada pelo autor como a “mais manifesta”. Esta dissertação formaliza-a em lógica quantificacional, explicitando cada uma das inferências a fim de julgar sua validade e correção. Depois de explicadas as teses metafísicas que constituem o cenário da discussão — como a doutrina aristotélica das quatro causas e as distinções entre substância e acidente, ato e potência —, são examinadas as objeções de Anthony Kenny (1969) e as sugestões interpretativas de John Wippel (2000) em defesa do raciocínio de Tomás. Mostra-se que a primeira parte, que procura demonstrar a irreflexividade do movimento, é um argumento válido, mas incorreto, por conter uma premissa falsa: aquela que afirma sem restrições a atualidade do movente. Já a segunda parte, o argumento contra o regresso infinito, contém uma ambiguidade que o deixa diante de duas alternativas: ou se trata de uma petição de princípio ou de uma falácia de equivocidade. Dado o fracasso material e formal da prova, é proposta finalmente uma abordagem não-dedutiva do problema. / Among the five proofs of God’s existence presented by Thomas Aquinas in his Summa Theologiae, the so-called "first way" stands out, for being considered by the author as the "most obvious" one. This dissertation formalizes it in quantificational logic, explaining each of the inferences in order to assess its validity and soundness. After explaining the metaphysical theses that provide the backdrop for the discussion — as the doctrine of the four Aristotelian causes and the distinctions between substance and accident, act and potency — it considers the objections of Anthony Kenny (1969) and interpretive suggestions of John Wippel (2000) in defense of Thomas’ reasoning. It is shown that the first part, which seeks to demonstrate the non-reflexivity of movement, is a valid argument, but unsound, because it contains a false premise: the one that states the mover’s actuality without restrictions. The second part, the argument against the infinite regress, contains an ambiguity that leaves you faced with two alternatives: either it begs the question or it is a fallacy of equivocation. Given the material and formal failure of the proof, a non-deductive approach to the problem is finally proposed.

En se fondant sur les travaux de Trimble et al., puis Hughes, on donne une notion de théorie symétrique monoïdale close (smc) et une construction explicite de la catégorie smc engendrée, formant ainsi une adjonction entre théories et catégories. On étudie les exemples du lambda-calcul pur linéaire, du lambda-calcul pur standard, puis des bigraphes de Milner. À chaque fois on donne une théorie smc et on compare la catégorie smc engendrée avec la présentation standard. Entre autres, dans les trois cas, on montre une équivalence entre les deux sur les termes clos. / From the work of Trimble et al. and Hughes, we define a notion of symmetric monoidal closed (smc) theory and give an explicit construction of the smc category generated by it. This construction yields a monadic adjunction between smc theories and smc categories. We study in our algebraic framework different models of programming languages: the linear λ-calculus, the pure λ-calculus and Milner's bigraphs. For each model, we give a smc theory and compare the generated smc category with the standard presentation. We show that, in each case, there is an equivalence on closed terms.

O presente trabalho cuida de investigar os principais aspectos da evolução histórica do instituto da prova, desde o antigo direito processual romano, passando pelo direito processual medieval, em especial, o direito lusitano, até o momento da última das três grandes Ordenações do Reino, as Filipinas, nos primórdios do século XVII. De início, a pesquisa aborda os vestígios da prova nos povos antigos e no processo civil romano, marcado pelo sistema processual das legis actiones. Posteriormente são analisadas as sucessivas modificações nos períodos subseqüentes (per formulas e extraordinaria cognitio, buscando identificar as mutações que a prova experimentou ao longo do tempo. Na seqüência, ultrapassando o período romano, chega-se ao período da Idade Média e da presença visigótica na Península Ibérica. Com o declínio do reino visigótico e ultrapassando o período da presença árabe, atenção especial será dada ao período da Reconquista, evidenciando o fenômeno da formação da nacionalidade portuguesa e seu antigo direito, de índole consuetudinária, bem representado no direito foraleiro, os Forais, e nas primeiras Leis Gerais. Após, investiga-se o sistema da prova previsto nos três grandes monumentos legislativos lusitanos, as Ordenações Afonsinas, Manuelinas e Filipinas. Trata-se, pois, de uma investigação na área da História do Processo Civil, com o objetivo de oferecer uma visão abrangente das origens do instituto da prova no moderno processo civil brasileiro, de longevas e inegáveis raízes lusitanas. / This study examines the key features of the historical evolution of the Evidence (Proof) under the Portuguese medieval law, from the emergence of ancient Roman civil procedure through the compiling of the last of the three great codifications (Ordenações Filipinas), in the early of 17th century. Reviewing the vestiges of legal practices concerning the evidence among the ancient peoples and mainly on the Roman civil procedure, marked by the procedural system of the legis actiones, next, the study analyses successive modifications to the evidence in the subsequent periods (per formulas e extraordinaria cognitio), and seeks to identify changes over time. The account then moves on from the Roman period to the Middle Age and the period of the Visigoth presence on the Iberian Peninsula.With the decline of the Visigoth kingdom and the period of Arab presence, special attention will be paid to the period of the Reconquest and the phenomenon of the formation of the Portuguese nationality and its ancient laws, based on custom and tradition, well represented by the Forais (ancient laws granted by the King) and the first general Laws (Leis Gerais). After, the study examines the evidence system in the three great Portuguese monumental legislative codifications (Ordenações Afonsinas, Ordenações Manuelinas e Ordenações Filipinas). The study is therefore concerned with the History of Civil Procedure, and its aim is to provide a sweeping overview of the genesis of the evidence in the modern Brazilian civil procedure, with its undeniable Portughese roots from distant past.

O tema \"segurança de fundações\" tem merecido especial atenção, tanto na lide acadêmica quanto na prática profissional, em virtude da necessidade de se buscar soluções cada vez mais otimizantes para a dicotomia custo versus segurança, soluções essas que diferem pela forma de tratamento das incertezas envolvidas no projeto e execução das fundações. As provas de carga sobre as fundações têm desempenhado papel central na redução dessas incertezas. Ultimamente, tem-se discutido muito, particularmente no âmbito da revisão da NBR 6122, o papel das provas de carga na redução das incertezas inerentes a qualquer obra de fundações. Se é ponto pacífico que as provas de carga devem reduzir as incertezas, já não há consenso quanto aos níveis dessa redução em função do tipo e da quantidade de provas de carga, nem tampouco como a variabilidade dos resultados das provas de carga efetuadas em dada obra influenciam no fator de segurança. Desta feita, o presente trabalho apresenta uma formulação consistente para combinação das previsões de capacidade de carga de estacas de deslocamento com as informações derivadas da realização de provas de carga estáticas conduzidas até a ruptura ou ensaios de carregamento dinâmico, propiciando a atualização racional dos indicadores de segurança, segundo os conceitos da inferência bayesiana. Os resultados permitem consignar que a inferência bayesiana se apresenta com grande vantagem em relação à inferência clássica, pois permite a incorporação das informações anteriores existentes, muitas vezes de caráter subjetivo, sendo menos dependente de amostragem. Além disso, a inferência bayesiana se mostrou um instrumento legítimo para a incorporação dos resultados de provas de carga, decorrendo em medidas de segurança fundamentadas e com paralelo na prática da engenharia de fundações. / The theme of \"foundations safety\" deserves special attention in theory and practice, due to the need to find optimized solutions, which balance cost and safety, solutions that differ in their method of uncertainty treatment. An important way of coping with these uncertainties is the proof pile load tests. Recently, the importance of proof load tests in the reduction of uncertainty has been widely discussed, mainly in the context of the NBR 6122 update. Despite their importance, there is no universally accepted standard regarding how the type and the number of proof load tests influence the safety factor. This work uses the bayesian inference concepts to present a consistent approach, which matches predictions of precast pile capacity with proof pile load tests results, thus providing a rational updating of safety indicators. The results of this study lead to the conclusion that bayesian inference methods have advantages compared with classical approaches. Since they allow the consideration of previous information, sometimes of a subjective nature, these methods do not require as large a sample as frequency approaches do. Furthermore, these methods have proved to be more robust than classical approaches whilst providing results which are consistent with current practice of foundation engineering.

Conselho Nacional de Desenvolvimento CientÃfico e TecnolÃgico / As estacas prÃ-fabricadas sÃo uma alternativa de fundaÃÃo indicada em situaÃÃes em que a vizinhanÃa nÃo apresenta restriÃÃes quanto a vibraÃÃes decorrentes de sua execuÃÃo. AlÃm disso, perfis de solos com baixa capacidade de suporte superficialmente e que se estende a maiores profundidades tambÃm apontam para a possibilidade de escolha dessa alternativa. Nestes casos, alÃm de outros, fundaÃÃes em estacas prÃ-fabricadas de concreto podem proporcionar fundaÃÃes tecnicamente possÃveis e economicamente mais atraente. Nesta dissertaÃÃo, à feito uma anÃlise da aplicabilidade dos principais mÃtodos de previsÃo de capacidade de carga e recalque de estacas prÃ-moldadas de concreto armado em perfis de solos granulares tÃpico dos encontrados comumente em Fortaleza. O objetivo deste trabalho à avaliar se previsÃes realizadas por mÃtodos semi-empÃricos de capacidade de carga e de recalque, realizados a partir de sondagens à percussÃo (SPT) e em perfis de solos granulares, sÃo concordantes tendo como referÃncia resultados de 7 provas de cargas estÃticas realizadas. AlÃm disso, pretende-se ainda avaliar se, provas de cargas interrompidas prematuramente sÃo capazes de serem extrapoladas de forma a proporcionar previsÃes da carga de ruptura concordantes. Para isso foram realizadas sondagens a percussÃo (SPT) e provas de cargas em alguns locais situados em Fortaleza. A seguir foram estimados os valores da capacidade de carga e do recalque de cada estaca ensaiada nas provas de carga, e para a carga de trabalho, atravÃs de mÃtodos semi-empÃricos, utilizando valores do Ãndice resistÃncia de sondagens à percussÃo (NSPT) corrigidos, e nÃo corrigidos, a partir da estimativa da eficiÃncia das sondagens utilizadas. As previsÃes realizadas a partir dos valores do Ãndice resistÃncia (NSPT) corrigidos proporcionaram estimativas da capacidade de carga e do recalque das estacas avaliadas mais concordantes. Os mÃtodos semi-empÃricos que apresentaram uma maior concordÃncia nas previsÃes das capacidades de carga foram o Aoki e Velloso (1975) e o Decourt e Quaresma (1982). Os mÃtodos semi-empÃricos que apresentaram uma maior concordÃncia nas previsÃes de recalque foram Bowles (1979) e Poulos & Davis (1980). / Prefabricated piles are a foundation of alternative indicated in situations where the neighborhood has no restrictions on the vibrations resulting from its implementation. In addition, soil profiles with low carrying capacity and surface extending deeper also indicate the choice of this alternative. In these cases and others, foundations Precast piles of concrete foundations can provide technically feasible and economically attractive. In this dissertation, it is made an analysis of the applicability of the main load capacity forecasting methods and repression of precast piles of reinforced concrete in typical granular soil profiles of commonly found in Fortaleza. The objective of this study is to evaluate whether predictions made by semi-empirical methods of load capacity and repression, carried out from polls to percussion (SPT) and granular soil profiles are consistent with reference to results of 7 load tests still performed. Furthermore, even if you want to evaluate whether evidence interrupted prematurely loads are able to be extrapolated to provide consistent breaking load forecasts. For that they were conducted polls percussion (SPT) and evidence of loads in some places situated in Fortaleza. The following were estimated values ​​of load capacity and settlement of each tested stake in load tests, and the workload, through semi-empirical methods, using values ​​of resistance index surveys to percussion (NSPT) corrected, and uncorrected, from the estimation of efficiency of used soundings. The predictions made from the values ​​of the resistance index (NSPT) provided fixed load capacity of estimates and the settlement of the piles evaluated more consistent. The semi-empirical methods that presented a greater agreement on forecasts of load capacities were Aoki and Velloso (1975) and Decourt and Lent (1982). The semi-empirical methods that showed a higher agreement in settlement predictions were Bowles (1979) and Poulos & Davis (1980).

Submitted by Fabio Sobreira Campos da Costa (fabio.sobreira@ufpe.br) on 2016-08-08T13:11:15Z No. of bitstreams: 2 license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) tese.pdf: 4855618 bytes, checksum: 717d268b142705bdc8ce106731a257db (MD5) / Made available in DSpace on 2016-08-08T13:11:15Z (GMT). No. of bitstreams: 2 license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) tese.pdf: 4855618 bytes, checksum: 717d268b142705bdc8ce106731a257db (MD5) Previous issue date: 2016-03-28 / CAPEs / Proof assistants are software-based tools that are used in the mechanization of proof construction and validation in mathematics and computer science, and also in certified program development. Different such tools are being increasingly used in order to accelerate and simplify proof checking, and the Coq proof assistant is one of the most known and used. Language and automata theory is a well-established area of mathematics, relevant to computer science foundations and information technology. In particular, context-free language theory is of fundamental importance in the analysis, design and implementation of computer programming languages. This work describes a formalization effort, using the Coq proof assistant, of fundamental results of the classical theory of context-free grammars and languages. These include closure properties (union, concatenation and Kleene star), grammar simplification (elimination of useless symbols, inaccessible symbols, empty rules and unit rules), the existence of a Chomsky Normal Form for context-free grammars and the Pumping Lemma for context-free languages. To achieve this, several steps had to be fulfilled, including (i) understanding of the characteristics, importance and benefits of mathematical formalization, specially in computer science, (ii) familiarization with the underlying mathematical theories used in proof assistants, (iii) familiarization with the Coq proof assistant, (iv) review of the strategies used in the informal proofs of the main results of the context-free language theory and finally (iv) selection and adequation of the representation and proof strategies adopted in order the achieve the desired objectives. The result is an important set of libraries covering the main results of context-free language theory, with more than 500 lemmas and theorems fully proved and checked. This is probably the most comprehensive formalization of the classical context-free language theory in the Coq proof assistant done to the present date, and includes the remarkable result that is the formalization of the Pumping Lemma for context-free languages. The perspectives for the further development of this work are diverse and can be grouped in three different areas: inclusion of new devices and results, code extraction and general enhancements of its libraries. / Assistentes de prova são ferramentas de software que são usadas na mecanização da construção e da validação de provas na matemática e na ciência da computação, e também no desenvolvimento de programas certificados. Diferentes ferramentas estão sendo usadas de forma cada vez mais frequente para acelerar e simplificar a verificação de provas, e o assistente de provas Coq é uma das mais conhecidas e utilizadas. A teoria de linguagens e de autômatos é uma área bem estabelecida da matemática, com relevância para os fundamentos da ciência da computação e a tecnologia da informação. Em particular, a teoria das linguagens livres de contexto é de fundamental importância na análise, no projeto e na implementação de linguagens de programação de computadores. Este trabalho descreve um esforço de formalização, usando o assistente de provas Coq, de resultados fundamentais da teoria clássica das gramáticas e linguagens livres de contexto. Estes incluem propriedades de fechamento (união, concatenação e estrela de Kleene), simplificação gramatical (eliminação de símbolos inúteis, de símbolos inacessíveis, de regras vazias e de regras unitárias), a existência da Forma Normal de Chomsky para gramáticas livres de contexto e o Lema do Bombeamento para linguagens livres de contexto. Para alcançar estes resultados, diversas etapas precisaram ser cumpridas, incluindo (i) o entendimento das características, da importância e dos benefícios da formalização matemática, especialmente na ciência da computação, (ii) a familiarização com as teorias matemáticas fundamentais utilizadas pelos assistentes de provas, (iii) a familiarização com o assistente de provas Coq, (iv) a revisão das estratégias usadas nas provas informais dos principais resultados da teoria das linguagens livres de contexto e, finalmente, (v) a seleção e adequação das estratégias de representação e prova adotadas para permitir o alcance dos resultados pretendidos. O resultado é um importante conjunto de bibliotecas cobrindo os principais resultados da teoria das linguagens livres de contexto, com mais de 500 lemas e teoremas totalmente provados e verificados. Esta é provavelmente a formalização mais abrangente da teoria clássica das linguagens livres de contexto jamais feita no assistente de provas Coq, e inclui o importante resultado que é a formalização do Lema do Bombeamento para linguagens livres de contexto. As perspectivas para novos desenvolvimentos a partir deste trabalho são diversas e podem ser agrupadas em três áreas diferentes: inclusão de novos dispositivos e resultados, extração de código e aprimoramentos gerais das suas bibliotecas.

Pesquisa que analisa questões técnicas, éticas e jurídicas relacionadas com o uso informatizado de dados genéticos na persecução criminal que suscitam a elaboração de regulamentações técnicas legais para o desejável equilíbrio entre garantias e direitos individuais e os de interesse coletivo relacionados com segurança pública. A automatização de dados de caráter pessoal tem trazido preocupações aos governantes de diversos países, levando-os a adotar medidas legais sobre o tema. Os avanços da genética e da informática possibilitaram a criação de bancos de dados de DNA voltados à identificação criminal que, por serem eficazes no combate à criminalidade, tornaram-se aspiração para muitos Estados, como é o caso brasileiro. Sem que se olvidem ou que se exaltem as potenciais benesses sociais, na criação de bancos de dados de DNA devem ser valorados outros aspectos que também permeiam a questão e que podem ferir suscetibilidades, direitos e garantias individuais. Dentre estes se destacam os de vieses técnicos e éticos concernentes à possibilidade de uso indevido de informações genômicas contidas na molécula de DNA, além dos aspectos jurídicos relacionados com garantias e direitos individuais e coletivos. A presente investigação estuda elementos técnicos relacionados com a análise de polimorfismos do DNA que autorizam seu uso como método de identificação humana, amplamente empregado na atualidade pela Medicina Legal e pela Criminalística para determinação de parentesco biológico e elucidação de crimes. São analisadas características estruturais e funcionais de bancos de dados genéticos e as principais questões técnicas, éticas e legais relacionadas com a coleta de materiais biológicos, com os cuidados de preservação e garantia de autenticidade, com a qualidade dos serviços laboratoriais usados para obtenção de perfis genéticos e com o valor probante da prova pericial formada. É avaliada a importância dos bancos de dados criminais de DNA para a investigação policial e para a persecução judicial, sopesando-se os interesses da segurança pública e os de preservação da privacidade dos sujeitos afetados. São também comparativamente examinados os principais dos bancos de dados de identificação genética criminal já em funcionamento no mundo e suas características atinentes aos sujeitos e tipos de delitos que neles são incluídos; o tempo de permanência dos dados; seu gerenciamento e o armazenamento de vestígios e de amostras-referência. São ainda apontados os parâmetros técnicos e legais mínimos a serem considerados para a criação e o estabelecimento de um banco de dados desse gênero. É estudada pormenorizadamente a proposta feita pela SENASP/MJ para a implantação de um banco nacional de perfis de DNA criminal no Brasil, aos moldes do consagrado CODIS norte-americano. Os resultados desta pesquisa sugerem que, ao se considerar que os direitos e garantias individuais não têm caráter absoluto frente a interesses públicos legítimos, a criação de um banco de dados criminais de DNA no Brasil é viável através da edição de uma lei estabelecedora dos limites das medidas restritivas das prerrogativas individuais e que regule minuciosamente seu funcionamento. / Research that analyses juridical, ethical and technical questions related to the digital use of genetic data at criminal prosecutions that engender the elaboration of legal and technical regulation to the desirable balance among individual rights and guarantees and those of collective interests related to public security. Personal data automation has brought concerns to several countries governments, leading them to adopt legal measures about the theme. Enhancements at genetics and information technology areas had made possible the creation of DNA databases related to criminal identification that, due to their efficacy at criminal combat, have become an aspiration to many States, such as Brazil. Without neither forgetting nor magnifying its potential social benefits, at DNAs database creation other aspects, that are also involved and that could hurt individual susceptibilities, rights and guarantees, should be valued. Among these, it should be emphasized those of technical and ethical concerns related to the improper use of DNAs genomic information, besides juridical aspects related to individual and collective rights and guarantees. The present investigation studies technical elements related to DNA polymorphisms analysis that allow its use as an Human Identification Method, largely employed nowadays at Criminalistics and Forensic Medicine to determine biological kinships and crime scene elucidations. We analyze genetic databases functional and structural characteristics, and the main legal, ethical and technical questions related to biological samples collection, to their preservation and authenticity guarantee, to the involved laboratories quality, and to the probative value of the formed forensic proof. Its also evaluated DNA criminal databases importance to police investigation and judicial prosecution, considering both the public security interest and the privacy preservation of the affected individuals. The main genetic identification databases already working around the world are also comparatively analyzed, as well as their characteristics, such as: what kinds of individuals and faults are included at database; for how long this data stays at the bank; how it is managed and how the storage of evidences and reference samples is done. We also point the minimum legal and technical parameters that should be considered to the creation and establishment of such a database. Its studied in details the SENASP/MJ proposal to implement a national bank of criminal DNA profiles in Brazil, similar to the American CODIS. The results of our study suggest that, considering that individual rights and guarantees dont have absolute character front legitimate public interests, the creation of a criminal DNA database in Brazil is practicable through the edition of some law that would establish the limits to individual prerogatives and also minutely regulate its operation.