[pt] Dedução Natural para a lógica intuicionista tem sido relacionada à Teoria das Categorias através do que agora é conhecido por Lógica Categórica. Essa relação é fortemente baseada no isomorfismo de Curry-Howard entre Dedução Natural e (lambda)-Cálculo Tipado. Esta dissertação descreve alguns aspectos dessa relação com o objetivo de propor uma visão 2-categórica da Lógica Categórica. Mostramos que mesmo numa visão 2-cateórica algumas desvantagens conhecidas na Teoria das Categorias continuam valendo. Concluímos essa dissertação discutindo as vantagens de uma visão 2-categórica a partir de premissas mais fracas. / [en] Natural Deduction for intuitionistic logic has been related to Category Theory by what now is known as Categorical Logic. This relationship is strongly based on the Curry-Howard Isomorphism between Natural Deduction and typed (lambda)-Calculus. This dissertation describes some aspects of these relationship with the aim of proposing a 2-categorical view of categorical logic. We show that even under this 2-categorical view some of the drawbacks already known in ordinary Category Theory remain holding. We conclude this dissertation discussing the advantages of 2-categorical view under some weaker assumptions.

[pt] Garantir que programas são implementados de forma a cumprir uma especificação é uma questão fundamental em computação, por isso, têm sido propostos vários métodos que almejam provar a correção dos programas. Este trabalho apresenta um método, baseado no isomorfismo de Curry-Howard, que extrai conteúdos computacionais de provas intuicionistas, conhecido como síntese construtiva ou proofs-as-programs. É proposto um processo de síntese construtiva de programas, onde a extração do conteúdo computacional gera um programa em linguagem imperativa a partir de uma prova em lógica intuicionista poli-sortida, cujos axiomas definem os tipos abstratos de dados, sendo utilizado como sistema dedutivo a Dedução Natural. Também é apresentada uma prova de correção, bem como uma prova de completude do método atráves do uso de um sistema com regra ômega (computacional) para a aritmética de Heyting, concluindo com uma demonstração da relação entre o uso da indução finita no lugar da regra ômega computacional no processo de síntese. / [en] One of the main problems in computer science is to assure that programs are implemented in such a way that they satisfy a given specification. There are many studies about methods to prove correctness of programs. This work presents a method, belonging to the constructive synthesis or proofs-as-programs paradigm, that comes from the Curry- Howard isomorphism and extracts the computational contents of intuitionist proofs. The synthesis process proposed produces a program in an imperative language from a proof in many-sorted intuitionist logic, where the axioms define the abstract data types using Natural Deduction as deductive system. It is proved the correctness, as well as the completeness of the method regarding the Heyting arithmetic with ômega-rule(in its computational version). A discussion about the use of the finitary induction instead of computational ômega-rule concludes the work.

[pt] Apresentamos uma lógica para a compreensão de condicionais a partir da proximidade (PUC-Logic) que unifica as lógicas Contrafactual e Deôntica propostas por David Lewis. Propomos também um sistema de dedução natural (PUC-ND) associado a essa nova lógica. Esse sistema de inferência é correto, completo, normalizável e decidível. A completude relativa para as lógicas V e CO é apresentada para dar ênfase à abordagem unificada sobre o trabalho de Lewis. Depois disso, apresentamos uma perspectiva construtivista para mostrar que a abstração contrafactual de Lewis não exige a regra do absurdo clássico. / [en] We present a logic for Proximity-based Understanding of Conditionals (PUC-Logic) that unifies the Counterfactual and Deontic logics proposed by David Lewis. We also propose a natural deduction system (PUC-ND) associated to this new logic. This inference system is proven to be sound, complete, normalizing and decidable. The relative completeness for the V and CO logics is shown to emphasize the unified approach over the work of Lewis. We, then, present a constructive approach to counterfactuals to show that the Lewis counterfactual abstraction does not require the classical absurd rule.

[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).

[pt] Segerberg apresentou uma prova geral da completude para lógicas proposicionais. Para tal, um sistema de dedução foi definido de forma que suas regras sejam regras para um operador booleano arbitrário para uma dada lógica proposicional. Cada regra desse sistema corresponde a uma linha na tabela de verdade desse operador. Na primeira parte desse trabalho, mostramos uma extensão da ideia de Segerberg para lógicas proposicionais finito-valoradas e para lógicas não-determinísticas. Mantemos a ideia de definir um sistema de dedução cujas regras correspondam a linhas de tabelas verdade, mas ao invés de termos um tipo de regra para cada valor de verdade da lógica correspondente, usamos uma representação bivalente que usa a técnica de fórmulas separadoras definidas por Carlos Caleiro e João Marcos. O sistema definido possui tantas regras que pode ser difícil trabalhar com elas. Acreditamos que um sistema de cálculo de sequentes definido de forma análoga poderia ser mais intuitivo. Motivados por essa observação, a segunda parte dessa tese é dedicada à definição de uma tradução entre cálculo de sequentes e dedução natural, onde procuramos definir uma bijeção melhor do que as já existentes. / [en] Segerberg presented a general completeness proof for propositional logics. For this purpose, a Natural Deduction system was defined in a way that its rules were rules for an arbitrary boolean operator in a given propositional logic. Each of those rules corresponds to a row on the operator s truth-table. In the first part of this thesis we extend Segerbergs idea to finite-valued propositional logic and to non-deterministic logic. We maintain the idea of defining a deductive system whose rules correspond to rows of truth-tables, but instead of having n types of rules (one for each truth-value), we use a bivalent representation that makes use of the technique of separating formulas as defined by Carlos Caleiro and João Marcos. The system defined has so many rules it might be laborious to work with it. We believe that a sequent calculus system defined in a similar way would be more intuitive. Motivated by this observation, in the second part of this thesis we work out translations between Sequent Calculus and Natural Deduction, searching for a better bijective relationship than those already existing.

[pt] A teoria da prova tradicional da lógica proposicional trata provas cujos tamanhos podem ser demasiado grandes. Estudos teóricos de prova descobriram diferenças exponenciais entre provas normais ou livres de corte e suas respectivas provas não-normais. Assim, o uso de grafos-de-prova, ao invés de árvores ou listas, para representar provas está se tornando mais popular entre teóricos da prova. Os grafos-de-prova servem como uma forma de proporcionar uma melhor simetria para a semântica de provas e uma maneira de estudar a complexidade das provas proposicionais. O objetivo deste trabalho é reduzir o peso/tamanho de deduções. Apresentamos formalismos de grafos de prova que visam capturar a estrutura lógica de uma dedução e uma forma de facilitar a visualização das propriedades. A vantagem destes formalismos é que as fórmulas e sub-deduções em dedução natural, preservadas na estrutura de grafo, podem ser compartilhadas eliminando sub-deduções desnecessárias resultando na prova reduzida. Neste trabalho, damos uma definição precisa de grafos de prova para a lógica puramente implicacional, logo estendemos esse resultado para a lógica proposicional completa e mostramos como reduzir (eliminando fórmulas máximas) essas representações de tal forma que um teorema de normalização pode ser provado através da contagem do número de fórmulas máximas na derivação original. A normalização forte será uma consequência direta desta normalização, uma vez que qualquer redução diminui as medidas correspondentes da complexidade da derivação. Continuando com o nosso objetivo de estudar a complexidade das provas, a abordagem atual também fornece representações de grafo para lógica de primeira ordem, a inferência profunda e lógica bi-intuitionista. / [en] Traditional proof theory of Propositional Logic deals with proofs which size can be huge. Proof theoretical studies discovered exponential gaps between normal or cut free proofs and their respective non-normal proofs. Thus, the use of proof-graphs, instead of trees or lists, for representing proofs is getting popular among proof-theoreticians. Proof-graphs serve as a way to provide a better symmetry to the semantics of proofs and a way to study complexity of propositional proofs and to provide more efficient theorem provers, concerning size of propositional proofs. The aim of this work is to reduce the weight/size of deductions. We present formalisms of proof-graphs that are intended to capture the logical structure of a deduction and a way to facilitate the visualization. The advantage of these formalisms is that formulas and subdeductions in Natural Deduction, preserved in the graph structure, can be shared deleting unnecessary sub-deductions resulting in the reduced proof. In this work, we give a precise definition of proof-graphs for purely implicational logic, then we extend this result to full propositional logic and show how to reduce (eliminating maximal formulas) these representations such that a normalization theorem can be proved by counting the number of maximal formulas in the original derivation. The strong normalization will be a direct consequence of such normalization, since that any reduction decreases the corresponding measures of derivation complexity. Continuing with our aim of studying the complexity of proofs, the current approach also give graph representations for first order logic, deep inference and bi-intuitionistic logic.

[pt] Existem diferentes estilos de cálculos dedutivos, usados para derivar os teoremas de uma lógica. Os mais habituais são os sistemas axiomáticos; mas, do ponto de vista da teoria da prova, os sistemas em dedução natural parecem ser mais interessantes. Essa é a motivação que leva ao desenvolvimento de técnicas que visam a facilitar a transformação de um cálculo dedutivo para o estilo em dedução natural. Esse trabalho se concentra no aspecto de modelar regras para os quantificadores da linguagem considerada e, para isso, faz uso de rótulos. Após uma apresentação intuitiva da técnica desenvolvida, passa-se à exposição de sistemas lógicos tratados pelo método: lógica de ultrafiltros, lógica de filtros, CTL, lógica de Keisler e CTL*. Em cada caso, analisam-se aspectos de teoria da prova. / [en] There are many kinds of deductive calculus. The axiomatic ones are the more usual. However, from the point of view of proof theory, Natural Deduction systems seem to be more interesting. This is the motivation for developping a technique that aims to ease the transformation from deductive calculus to Natural Deduction style. This work concentrates on the aspect of modeling the rules for the quantifiers of the logic considered, and for this purpose labels are used. After an intuitive presentation of the technique developped, some logical systems are treated by the method: ultrafilter logic, filter logic, CTL, Keisler`s logic and CTL*. For each one of them proof-theoretical aspects are analysed.

[pt] Neste trabalho propomos um framework lógico para sistemas de Dedução Natural rotulados. Sua meta-linguagem é baseada numa generalização dos esquemas de regras propostos por Prawitz, e o uso de rótulos permite a definição de lógicas intencionais como lógicas modais e de descrição, bem como a definição uniforme de quantificadores como o para um número não-renumerável de indivíduos vale a propriedade P (lógica de Keisler), ou para quase todos os indivíduos vale P (lógica de ultra-filtros), sem mencionar os quantificadores padrões de lógica de primeira-ordem. Mostramos também a implementação deste framework em um assistente de prova virtual disponível livremente na web, e comparamos a definição de sistemas lógicos nele com o mesmo feito em outros assistentes — Agda, Isabelle, Lean, Metamath. Como subproduto deste experimento comparativo, também contribuímos uma prova formal em Lean do postulado de Zolt em três dimensões usando o sistema Zp proposto por Giovaninni et al. / [en] We propose a Logical Framework for labelled Natural Deduction systems. Its meta-language is based on a generalization of the rule schemas proposed by Prawitz, and the use of labels allows the definition of intentional logics, such as Modal Logic and Description Logic, as well as some quantifiers, such as Keisler s for non-denumerable-many individuals property P, or for almost all individuals P holds, or generally P holds, not to mention standard first-order logic quantifiers, all in a uniform way. We also show an implementation of this framework as a freely-available web-based proof assistant. We then compare the definition of logical systems in our implementation and in other proof assistants — Agda, Isabelle, Lean, Metamath. As a sub-product of this comparison experiment, we contribute a formal proof (in Lean) of De Zolt s postulate for three dimensions, using the Zp system proposed by Giovaninni et al.

[pt] A lógica descritiva intuicionista iALC foi criada para modelar e raciocinar sobre o domínio de Leis baseada na Jurisprudência Kelseniana [1]. No decorrer da década anterior, essa lógica foi usada de diversas maneiras para modelar normas ou formalizar raciocínio jurídico [2, 3, 4, 5, 6, 7, 8, 9, 10]. Neste trabalho pretendemos complementar trabalhos anteriores ralizados com essa lógica ao preencher algumas lacunas encontradas enquanto trabalhando com ela. A primeira lacuna ocorre por iALC não ter um modo intuitivo de explicar raciocínio nela realizado para pessoas fora do domínio da Lógica. Ela tem um Cálculo de Sequentes (CS) [6] correto e completo (com respeito a modelos conceituais intuitionistas [3]) que tem sido menos usado que o desejado, e isso se dá em grande parte devido à maneira pouco intuitiva com que CS representa provas. Apresentamos um sistema de Dedução Natural (DN) correto e completo e com (quasi-)normalização para compensar por essa dificuldade em explicar CS para não-lógicos, especialmente os do domínio legal, essenciais para nossa pesquisa. Normalização completa não é possível devido a um tipo de derivação - tirando essa exceção, o resto do sistema gera derivações uniformes. A segunda lacuna envolve não poder lidar com raciocínio não-monotônico (RNM). Em geral, utiliza-se raciocínio monotônico, no qual, se é possível concluir algo de um conjunto de premissas, não há como acrescentar outra premissa de modo a evitar a conclusão prévia. Isso não é o caso em um julgamento legal, por exemplo, no qual lados opostos buscam convencer um juiz ou júri de consequências opostas ao adicionar premissas diferentes ao caso em questão. Propomos uma investigação de caráter exploratório em busca de uma extensão de iALC para lidar com RNM a fim de representar raciocínio jurídico em outras facetas da Lei como o processo judicial, que é não-monotônico por natureza. Apresentamos propriedades desejadas e uma possível aplicação de um sistema assim via um estudo de caso. Detalhamos mais a motivação tanto para o sistema de DN quanto a extensão de RNM, assim como as decisões tomadas ao criar cada um. / [en] The intuitionistic description logic iALC was created to model and reason over the domain of Law based on Kelsenian Jurisprudence [1]. Over the past decade, this logic has been used in several ways to either model norms or formalise legal reasoning [2, 3, 4, 5, 6, 7, 8, 9, 10]. In this work we intend to complement previous research done with this logic by filling some gaps found while working with it. The first gap occurs in iALC needing an intuitive way to explain reasoning for non-logicians. It has a sound and complete (concerning intuitionistic conceptual models [3]) Sequent Calculus (SC) [6] that has seen less usage than expected due to its non-intuitive way of presenting a proof. We present a (quasi-)normalising, sound and complete (w.r.t. TBox validity for intuitionistic conceptual models) Natural Deduction (ND) System to cover this difficulty in explaining SC to non-logicians, especially those in the domain of Law, which are essential to us. We do not achieve full normalisation due to a kind of derivation which cannot be normalised - aside from this exception, the rest of the system can provide uniform derivations. The second gap is being unable to deal with non-monotonic reasoning (NMR). Usually, one considers monotonic reasoning, in which, if one can conclude something from a set of premises, there is no way to add another premise to avoid said conclusion. This is not the case in a court of law, for instance, in which different parties aim to convince a judge or jury of opposite consequences by adding different premises to the case itself. We provide an exploratory investigation of an extension of iALC to deal with NMR to represent legal reasoning in aspects of the Law, such as the judicial process, which is non-monotonic by nature. We present desirable properties and a possible application of such a system via a case study. We explain further the motivation for both the ND system and the NMR extension and the decisions taken for both.