Made available in DSpace on 2014-12-17T15:12:12Z (GMT). No. of bitstreams: 1 DavidGC_DISSERT.pdf: 766947 bytes, checksum: f1a6301612dd36741701f971f1734291 (MD5) Previous issue date: 2010-01-15 / Formalization of logical systems in natural deduction brings many metatheoretical advantages, which Normalization proof is always highlighted. Modal logic systems, until very recently, were not routinely formalized in natural deduction, though some formulations and Normalization proofs are known. This work is a presentation of some important known systems of modal logic in natural deduction, and some Normalization procedures for them, but it is also and mainly a presentation of a hierarchy of modal logic systems in natural deduction, from K until S5, together with an outline of a Normalization proof for the system K, which is a model for Normalization in other systems / A formaliza??o de sistemas de l?gica em dedu??o natural traz muitas vantagens meta-teor?ticas, das quais ? sempre destacada a prova de normaliza??o. Os sistemas de l?gica modal at? bem recentemente n?o eram costumeiramente tratados pelo vi?s da dedu??o natural, contudo algumas formula??es, provas de normaliza??o e tentativas de provas surgiram. Esse trabalho ? uma apresenta??o de alguns sistemas importantes de l?gica modal em dedu??o natural j? existentes, e de alguns procedimentos de normaliza??o para eles, mas ? tamb?m, e principalmente, a apresenta??o de uma hierarquia de sistemas de l?gica modal em Dedu??o Natural do sistema K ao sistema S5 e um esquema da prova de normaliza??o do sistema K, que ? modelo para a normaliza??o nos outros sistemas