[pt] A primeira apresentação de um Cálculo de Seqüentes foi feita por Gerhard Gentzen na década de 1930. Neste tipo de sistema, a diferença entre as versões clássica e intuicionista radicardinalidade do sucedente. O sucedente múltiplo foi tradicionalmente considerado como o elemento que representava o aspecto clássico do sistema, enquanto os seqüentes intuicionistas podiam ter, no máximo, uma fórmula no sucedente. Nas décadas seguintes foram formulados diversos cálculos intuicionistas de sucedente múltiplo que atenuaram essa restrição forte na cardinalidade do sucedente. Na década de 1990, estudou-se a relação de conexão ou dependência entre as fórmulas visando assegurar o caráter intuicionista dos sistemas. Nós realizamos uma revisão dos sistemas de se seqüentes intuicionistas e algumas das suas aplicações. Apresentamos a versão do sistema FIL (feita para o caso proposicional por De Paiva e Pereira) para a lógica intuicionista de primeira ordem provando que o mesmo é correto, completo e satisfaz eliminação de corte. / [en] The first Sequent Calculus was presented by Gerhard Gentzen in the thirties. In this system, the difference between intuitionistic logic and classical logic is based on the cardinality of the succedent. Traditionally, the multiple succedent was considered the element that preserved the classical aspect of the system, while intuitionistic sequents have, at most, one formula in the succedent. In the following decades, several multiple succedent intuitionistic calculus were presented that diminish shed this st strong restriction in the cardinality of the su succedent. In the decade of 1990, this cardinality restriction was replaced by a dependency relation between the formula ocurrences in the antecedent and in the succedent of a sequent in order to ensure the intuitionistic character of the system. We make a revision of the intuitionistic systems and some of their applications. We present a version of the system FIL (accomplish shed for the propositional case by De Paiva and Pereira) for first-order logic proving that it is sound, complete and that it satisfies the cut-elimination theorem.

[pt] É um fato conhecido que provas clássicas podem ser demasiadamente grandes. Estudos em teoria da prova descobriram diferenças exponenciais entre provas normais (ou provas livres do corte) e suas respectivas provas não normais. Por outro lado, provadores automáticos de teorema usualmente se baseiam na construção de provas normais, livres de corte ou provas de corte atômico, pois tais procedimento envolvem menos escolhas. Provas de algumas tautologias são conhecidamente grandes quanto realizadas sem a regra do corte e curtas quando a utilizam. Queremos com este trabalho apresentar procedimentos para reduzir o tamanho de provas proposicionais. Neste sentido, apresentamos dois métodos. O primeiro, denominado método vertical, faz uso de axiomas de extensão e alguns casos é possível uma redução considerável no tamanho da prova. Apresentamos um procedimento que gera tais axiomas de extensão. O segundo, denominado método horizontal, adiciona fórmulas máximas por meio de unificação via substituição de variáveis proposicionais. Também apresentamos um método que gera tal unificação durante o processo de construção da prova. O primeiro método é aplicado a dedução natural enquanto o segundo à Dedução Natural e Cálculo de Seqüentes. As provas produzidas correspondem de certo modo a provas não normais (com a regra do corte). / [en] It is well-known that the size of propositional classical proofs can be huge. Proof theoretical studies discovered exponential gaps between normal or cut-free proofs and their respective non-normal proofs. The task of automatic theorem proving is, on the other hand, usually based on the construction of normal, cut-free or only-atomic-cuts proofs, since this procedure produces less alternative choices. There are familiar tautologies such that the cut-free proof is huge while the non-cut-free is small. The aim of this work is to reduce the weight of proposicional deductions. In this sense we present two methods. The fi first, namely vertical method, uses the extension axioms. We present a method that generates a such extension axiom. The second, namely horizontal method, adds suitable (propositional) unifi fications modulo variable substitutions.We also present a method that generates a such unifi fication during the proving process. The proofs produced correspond in a certain way to non normal proofs (non cut-free proofs).