CAVALCANTE, Alexandre Silva. Sistemas esquemáticos de dedução natural: um estudo prova-teórico. 2010. 201 f. Tese (Doutorado em ciência da computação)- Universidade Federal do Ceará, Fortaleza-CE, 2010. / Submitted by Elineudson Ribeiro (elineudsonr@gmail.com) on 2016-07-12T19:23:49Z No. of bitstreams: 1 2010_tese_ascavalcante.pdf: 842091 bytes, checksum: 559c5a97b93d42e7b0bb2d0c9b1d1520 (MD5) / Approved for entry into archive by Rocilda Sales (rocilda@ufc.br) on 2016-07-25T11:32:56Z (GMT) No. of bitstreams: 1 2010_tese_ascavalcante.pdf: 842091 bytes, checksum: 559c5a97b93d42e7b0bb2d0c9b1d1520 (MD5) / Made available in DSpace on 2016-07-25T11:32:56Z (GMT). No. of bitstreams: 1 2010_tese_ascavalcante.pdf: 842091 bytes, checksum: 559c5a97b93d42e7b0bb2d0c9b1d1520 (MD5) Previous issue date: 2010 / The term Theory Test was introduced by Hilbert to identify the study of formal proofs. Research in this area can be classified into: a) Proof Theory of reductive or interpretational, whose goal is to demonstrate, among other things, the consistency of mathematics using only methods finitistas, b) Structural Proof Theory, where the structural characteristics of the formal proofs are investigated by means of deductive systems as Natural Deduction and Sequent Calculus. Prawitz through Theory Proof set a Theory of Meaning for constants logics and proposed schematic introduction rules and elimination to characterize the propositional connectives. Schroeder-Heister settings Prawitz extended and formalized the use of rules as hypotheses, making possible the use of separate calculations for assumptions of calculations for logical constants. We are not interested in the investigation of schematic rules to give meaning to the logical constants. We intend to actually set schematic standardization procedures, based on such schematic rules? Attic, in order to identify sufficient conditions for a system to be normalizável. These results are relevant to the Abstract Theory of Evidence, a term used to identify the study of the conditions abstract and general to the proof-theoretical analysis of formal systems. Abstract Theory of Evidence do not study specific logical calculations, but families of calculations instances of rules schematic. Our proposal is therefore based on rules schematic rules can be instantiated for concrete, in particular, by introducing rules modal operators. We prove also theorems Normalizaçãoo Weak and Strong systems defined in schematic funçãoo schematic of our rules, we obtain sufficient conditions for a system instance is normalizável these rules, we define a procedure that normalizes deductions concrete evidence and compare our standards with evidence schematic standards for systems defined in the literature. / O termo Teoria da Prova foi introduzido por Hilbert para identificar o estudo sobre provas formais. Pesquisas nessa área podem ser classificadas em: a) Teoria da Prova Redutiva ou Interpretacional, cujo objetivo é demonstrar, entre outras coisas, a consistência da matemática utilizando somente métodos finitistas, e b) Teoria da Prova Estrutural, onde características estruturais das provas formais são investigadas por meio de sistemas dedutivos como Dedução Natural e Cálculo de Sequentes. Prawitz, por meio da Teoria da Prova, definiu uma Teoria dos Significados para constantes logicas e propôs regras esquemáticas de introdução e de eliminação para caracterizar os conectivos proposicionais. Schroeder-Heister estendeu as definições de Prawitz e formalizou o uso de regras como hipóteses, tornando possível a utilização de cálculos para suposições separados de cálculos para constantes lógicas. Não estamos interessados na investigação de regras esquemáticas para dar significado a constantes lógicas. Pretendemos, na verdade, definir procedimentos de normalização esquemáticos, baseados em tais regras esquemáticas, com objetivo de identificar condições suficientes para um sistema ser normalizável. Tais resultados são pertinentes à Teoria Abstrata da Prova, termo usado para identificar o estudo das condições abstratas e gerais para a análise prova-teórica de sistemas formais. Teoria Abstrata da Prova não estuda cálculos lógicos específicos, mas famílias de cálculos instâncias de regras esquemáticas. A nossa proposta, portanto, baseia-se em regras esquemáticas que podem ser instanciadas por regras concretas, em particular, por regras que introduzem operadores modais. Provamos, também, Teoremas de Normalização Fraca e Forte para sistemas esquemáticos definidos em função de nossas regras esquemáticas, obtemos condições suficientes para que um sistema instância destas regras seja normalizável, definimos um procedimento que normaliza deduções concretas e comparamos nossas provas de normalização esquemática com provas de normalização para sistemas definidos na literatura.