[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] Considerando o aumento da participação da iniciativa privada em projetos e programas que buscam contribuir para a elevação do bem estar da sociedade, inclusive por meio de ações de marketing social, esta pesquisa teve como principal objetivo identificar, na perspectiva dos atores envolvidos, em especial o público-alvo, como a cocriação de valor é abordada (e se manifesta) nos programas de marketing social desenvolvidos por empresas no Brasil. Para tal, foi realizado um estudo multicasos que teve como objetos de estudo três iniciativas promovidas por uma empresa privada do segmento de bens de consumo, em parceria com outras organizações. Todas as iniciativas estudadas apresentam aspectos que as caracterizavam como ações de marketing social e abrangiam diferentes causas de interesse da sociedade: segregação de resíduos sólidos, cuidados com a saúde cardiovascular e hábitos de higiene junto ao público infantil, especialmente por meio da lavagem adequada das mãos. Os métodos para coleta de dados envolveram quarenta entrevistas pessoais, por telefone e por email, observação e consulta a arquivos e documentos diversos fornecidos por alguns dos entrevistados. A análise dos dados foi qualitativa, seguindo categorias pré-definidas a partir da revisão de literatura. Os resultados da pesquisa mostraram que as iniciativas estudadas foram desenvolvidas tendo por base diversos elementos da cocriação de valor, destacando-se, principalmente, o projeto voltado aos cuidados com a higiene das mãos. Especificamente em relação aos processos de descoberta, design e entrega de valor, as iniciativas estudadas, apesar de apresentarem elementos da cocriação de valor, o fazem predominantemente na etapa da entrega, sendo que os processos de descoberta de design parecem ter ocorrido apenas sob a responsabilidade das organizações envolvidas, sem evidências que sugerem a participação do público-alvo. Identificou-se que a abordagem mais evidente nas iniciativas estudadas é a downstream, mais voltada à mudança do comportamento individual. O presente trabalho colabora para preencher uma lacuna na literatura referente a marketing social e cocriação de valor, em especial no que tange ao estudo de ações desenvolvidas pela iniciativa privada. Além disso, os resultados da pesquisa, ao relatarem determinadas condições em que as iniciativas estudadas operam, também indicaram aspectos em que estas podem ter seus resultados potencializados, a partir da incorporação de mais princípios da cocriação de valor. / [en] Considering the increasingly interest of the business sector in projects and programs which seek to contribute to society s well-being, including actions of social marketing, this research s main objective was to identify, from the concerned parties perspective, specially the target audience, how the co-creation is approached (and manifested) in marketing social programs developed by enterprises in Brazil. Therefore, a multi-case study was developed, which had, as its objects of study, three initiatives from a private Brazilian company that operates in the convenience goods sector, in partnership with other organizations. All of the studied initiative show aspects that characterized them as social marketing actions and embraced a few different aspects of interest from society, among which were: segregation of solid residues, cardiovascular care and children s hygiene habits, especially through adequate hand washing. Methods for data collection include forty face to face, phone and e-mail interviews as well as observation procedures and research of many files and documents provided by a few of the respondents. The data analyses was qualitative, following preestablished trends, taking the literature review as a starting point. The results from the research pointed out that the studied initiatives were developed based on several elements of co-creation of value, specially the project aimed at adequate hand hygiene. Regarding the discovery, design and delivery of value processes specifically, it is noticeable that in the initiatives studied, value co-creation elements are predominantly in the delivery step, and the design discovery processes seem to have occurred only under the responsibility of the organizations involved, with no evidence to suggest the participation of the audience. It was identified that the most obvious approach of the studied initiatives is the downstream, more focused on individual behavior change. This work contributes to fill a gap in respect of social marketing literature and co-creation of value, especially in relation to the study of actions developed by the private sector. In addition, the research s results, when reporting certain conditions under which the studied initiatives operate, also indicated room for improvement in their results if more principles of co-creation of value were to be implemented.

[pt] A presente tese tem como objetivo desenvolver uma discussão acerca das condições de possibilidade da quantificação irrestrita e existência da generalidade absoluta. O trabalho é dividido em quatro etapas. No primeiro capítulo, realizo, no âmbito da teoria dos modelos e teoria dos conjuntos, uma revisão do que chamo de semântica padrão dos quantificadores. A ideia básica é mostrar como, em tal semântica, quantificações estão associadas a domínios entendidos como conjuntos. Ao longo da tese, ficará patente que a semântica padrão impõe obstáculos intransponíveis ao tratamento formal de quantificações irrestritas. No segundo capítulo, apresento uma seleção do que considero os argumentos mais relevantes contra quantificações irrestritas e nossa capacidade de lidar formalmente com o que chamamos de generalidade absoluta. Alguns desses argumentos estão baseados em resultados tais como os paradoxos que Russell e Cantor derivaram na teoria dos conjuntos. No terceiro capítulo, apresento, de modo análogo, uma lista de argumentos agrupados em linhas de estratégias para reabilitar a quantificação irrestrita contra seus críticos. Além disso, desenvolvo uma discussão sobre os aspectos metafísicos do debate sobre o discurso a respeito da generalidade absoluta e sua correlação com argumentos por regresso ao infinito. Por fim, no quarto e último capítulo, desenvolvo um esboço geral de uma proposta alternativa de tratamento da quantificação irrestrita que apele para uma teoria paraconsistente dos conjuntos. Nela, as contradições obtidas na semântica padrão podem ser admitidas controladamente possibilitando assim a obtenção de domínios absolutos para quantificações. Essa proposta envolve a defesa de um sistema formal que seja inconsistente, porém dedutivamente não trivial. Em linhas gerais, o presente trabalho está pautado no seguinte conjunto de teses: (i) existe uma estreita correlação entre os obstáculos impostos pela semântica padrão às quantificações irrestritas e a estrutura de argumentos por regresso ao infinito; (ii) a existência de uma generalidade absoluta é um fenômeno que se impõe às nossas mais intuitivas concepções de realidade e, portanto, não devemos descredenciar o discurso sobre tal generalidade em virtude de limitações de nossas linguagens formais; (iii) nós devemos escolher entre assumir a lógica clássica e abdicar do discurso sobre a generalidade absoluta ou manter nossa intuição mais básica descrita em (ii) e abrir espaço para um tratamento não clássico da questão; finalmente, (iv) minha sugestão no presente trabalho é que temos boas razões para nos aventurar nas paisagens descritas pelos sistemas não clássicos. / [en] In this doctoral dissertation, I tackle the issues of the conditions for the possibility of unrestricted quantification and of absolute generality. The text is framed as follows. The first chapter is devoted to reviewing what I call the standard semantics of quantifiers, within the realm of both model and set theories. In such semantics, the idea is, quantificational domains are conceived as sets. It will become clear along the way that, given this construal of quantificational domains, a formal treatment of unrestricted quantification faces insurmountable obstacles. The second chapter focuses on what I take to be the most relevant arguments against unrestricted quantification as well as against our ability to formally deal with so-called absolute generality. Some of them are based on results obtained by Russell and Cantor within set theory – the notorious Russell s paradox and Cantor s theorem. Analogously, in chapter three I review a number of grouped-into-strategic-lines arguments put forward to save unrestricted quantification against its critics. I also elaborate on the metaphysical aspects of the debate and its connections with infinite regress arguments. Lastly, in the fourth chapter I outline an alternative proposal based on paraconsistent set theory to deal with unrestricted quantification. On this approach, the contradictions found in standard semantics are admitted, yet in a controlled way, thus turning absolute quantificational domains available. The proposal is, basically, to allow the existence of inconsistent, yet deductively not trivial formal systems. The present work is broadly guided by the following set of claims: (i) there is a strong correlation between the obstacles set by standard semantics to unrestricted quantification and the structure of infinite regress arguments; (ii) absolute generality is a phenomenon that imposes itself upon our most intuitive conceptions of reality; accordingly, the limitations suffered by our formal languages ought not to lead us to bring such generality into disrepute; (iii) one must choose between adopting classical logic and renouncing to appeal to absolute generality or sticking to our most basic intuitions as described in (ii) and make room for a non-classical treatment of the issue; (iv) we have, after all, good reasons to venture into the landscapes described by the non-classical systems.

[pt] O Sistema elétrico brasileiro é baseado quase que integralmente em energia produzida por Usinas Hidroelétricas. Estas Máquinas Hidroelétricas possuem um comportamento diferenciado das máquinas turbo geradoras, cujo comportamento já foi identificado e classificado em pesquisas anteriores. Este trabalho investiga o uso de um Sistema baseado em Conhecimento para o diagnóstico precoce de falhas em Máquinas Hidrogeradoras, visando redução de custos advindos principalmente de paradas operacionais não necessárias na máquina para manutenção. O sistema foi criado com informação obtida a partir dos seguintes meios: sistemática de manutenção executada nas Usinas Hidroelétricas, através de entrevistas à equipe responsável pela manutenção da usina de Furnas (MG); da identificação do comportamento eletromecânico da máquina; e do estudo de casos. O Sistema é capaz de identificar, a partir dos sensores localizados nas máquinas, eventuais falhas, permitindo executar paradas programadas de maneira otimizada. Foi criado um protótipo de um sistema computacional baseado em Conhecimento implementando tal modelo de forma bem flexível. A modelagem criada, a implementação do protótipo computacional e, principalmente, a explicação do raciocínio empregado, agregado com a possibilidade da modificação do conhecimento através da aquisição automática, são contribuições inovadoras deste trabalho. É descrito o Domínio do Problema de diagnosticar falhas em Máquinas Hidrogeradoras, identificado durante análise das informações coletadas da equipe de manutenção na usina de Furnas e de especialistas no comportamento eletromecânico das máquinas. É descrito também o modelo simbólico criado, representativo do domínio, utilizando interface projetada, visando a implementação prática nas usinas. É apresentado uma solução de desacoplamento das informações advindas dos sensores eletromecânicos da máquina e o sistema, através de módulo baseado em Lógica Nebulosa (Fuzzy Logic) que converte as informações numéricas em informações simbólicas compreendidas pelo sistema de diagnóstico, permitindo o uso do sistema, sem alteração em máquinas que possuam características diversas. Finalmente, é apresentada a metodologia de testes adotada para validação do modelo implementado através da simulação de dados de vibração e oscilação, cujo relacionamento com eventuais falhas é parcialmente conhecido, assim como uma conclusão sobre a viabilidade e praticidade de um modelo simbólico na solução do diagnóstico das máquinas hidrogeradoras. Durante o desenvolvimento da tese verificou-se que o conhecimento sobre falhas em Máquinas Hidrogeradoras ainda não está consolidado e que então, um Sistema baseado em Conhecimento com aquisição de conhecimento automático mostra-se uma excelente ferramenta de modelagem para os especialistas. / [en] The Brazilian Electrical Energy supply is almost entirely based on the energy produced by the Hydroeletric Power Station Machines. These Hydroeletric Machines own particular behavior in comparison to the turbogenerator behavior. This work investigates the use of Knowledge based system Hydroeletric Machines fault diagnosis. The system was modeled using information obtained by: the maintenance s systematic executed Hydroeletric Power Stations, though Furnas (Minas Gerais) maintenance team interviews; the Machine electromechanical behavior; and a Case Based study. The system is able to identify, from machine located sensors data analysis, eventual faults, allowing the execution of programmed operational interrupts in the machine in a optimized manner. A computational prototype and, mainly, the interface explain engine in addition to the knowledge modification through acquisition, are the innovative contributions of this work. The machine fault diagnosis problem domain is described, identified in the information, collected from the maintenance team and the electromechanical behavior experts, analysis. It is also described the projected symbolic model, the domain representation, using graphical and friendly interface, aiming its practical implementation in real Power Stations. It is shown a sensor information detach solution, through a Fuzzy Logic based module which converts the numerical data in a symbolic one, known by the diagnosis system, allowing its use, without any modification, in a sort of different machines. Finally, it is shown the test methodology adopted for the prototype validation through oscillation data simulation, which relationship with machine faults is partially known, and the symbolic model praticality and feasibility in the Hidrogenerator Diagnosis solution. Through the thesis development, it was verified that the Hydrogenerator fault knowledge wasn t still consolidated. So, the Knowledge Based system with knowledge acquisition became an excelent modeling tool for the domain experts.

[pt] O tamanho das provas formais possui algumas importantes implicações teóricas na área da complexidade computacional. O problema de determinar se uma fórmula é uma tautologia da Lógica Proposicional Intuicionista e do fragmento puramente implicacional da Lógica Minimal (M(contém)) é PSPACE- Completo. Qualquer lógica proposicional com um sistema de dedução natural que satisfaça o princípio da subfórmula possui o problema de determinar tautologias em PSPACE. Saber se qualquer tautologia em M(contém) admite provas de tamanho polinomialmente limitado está relacionado com saber se NP = PSPACE. Técnicas de compressão de provas reportadas na literatura utilizam duas abordagens principais para comprimir provas: gerar provas já compactadas; comprimir uma prova já gerada. Proposta por Gordeev e Haeusler (6), a Compressão Horizontal é uma técnica de compressão de provas em dedução natural da M(contém) que utiliza grafos direcionados para representar as provas. Dada a prova de uma tautologia qualquer da M(contém), que pode possuir tamanho exponencial em relação ao tamanho da conclusão, o objetivo da Compressão Horizontal é que a prova resultante da compressão possua tamanho polinomialmente limitado em relação ao tamanho da conclusão. Nosso trabalho apresenta a primeira implementação da Compressão Horizontal, juntamente com os primeiros resultados da aplicação da técnica sobre provas de tautologias da M(contém), além disso, compara as taxas de compressão obtidas com técnicas tradicionais de compressão de dados. / [en] The size of formal proofs has some important theoretical implications in computational complexity theory. The problem of determining if some formula of Intuitionistic Propositional Logic and the purely implicational fragment of Minimal Logic (M(contains)) is a tautology is PSPACE-Complete. Any propositional logic with a natural deduction system that satisfies the sub- formula principle is PSPACE. To know if any tautology in M(contains) admits polynomially sized proof is related to whether NP = PSPACE. Proof compression techniques reported in literature use two main approaches to proof compressing: generating already compressed proofs; compressing an already generated proof. Proposed by Gordeev and Haeusler (6), the Horizontal Compression is a natural deduction proof compression technique that uses directed graphs to represent proofs. Given a tautology proof in M(contains), which may have an exponential size in relation to conclusion length, the goal of Horizontal Compression is that the compressed proof has a polynomially limited size in relation to conclusion length. Our work presents the first implementation of Horizontal Compression, together with the first results of the execution of the technique on proofs of M(contains) tautologies.

[pt] O termo jogo tem sido utilizado como uma metáfora, em várias áreas do conhecimento, para modelar e analisar situações onde agentes(jogadores) interagem em ambientes compartilhados para a realização de seus objetivos sejam eles individuais ou coletivos. Existem diversos modelos propostos para jogos por diferentes áreas do conhecimento, tais como matemática, ciência da computação, ciência política e social, entre outras. Dentre as diversas formas de modelar jogos examinamos a Teoria dos Jogos e as lógicas para jogos. Neste trabalho apresentamos uma lógica modal de primeira-ordem baseada na lógica CTL, chamada de Game Analysis nalysis Logic, para raciocinar sobre jogos. Relacionamos os principais modelos da Teoria dos Jogos (jogo estratégico, extensivo, e de coalizão) e seus principais conceitos de soluções(equilíbrio de Nash, equilíbrio de subjogo perfeito,e core) aos modelos de GAL e às fórmulas de GAL, respectivamente. Além disso, estudamos as alternativas de quantificação De Re e De Dicto no contexto dos jogos extensivos, caracterizando o conceito de equilíbrio de Nash e equilíbrio de subjogo perfeito de acordo com as alternativas de quantificação. Relacionamos as lógicas Alternating-time lternating-Tempomporal Logic (A ATL) TL) e Coalitional Game Logic (CGL) com a lógica GAL, demonstrando que ambas as lógicas são fragmentos da lógica GAL. Outro resultado deste trabalho é caracterizar uma classe de sistemas multi- agentes,que é baseada na arquitetura de agentes Belief-Desir Desire- Intention(BDI), para a qual existem jogos extensivos e vice-v versa. Como conseqüência, os critérios de racionalidade da Teoria dos Jogos podem ser aplicados diretamente para agentes BDI e vice-versa. Assim, a abordagem deste trabalho pode ser utilizada para analisar sistemas multi-agentes. Do ponto de vista prático, apresentamos um verificador de modelos para a lógica GAL. Diversos estudos de casos são realizados utilizando o verificador de modelos. / [en] Games are abstract models of decision-making in which decision-makers(players)interact in a shared environment to accomplish their goals. Several models have been proposed to analyze a wide variety of applications in many disciplines such as mathematics, computer science and even political and social sciences among others. In this work, we focus on Game Theory and Game Logics. We present a first-order modal logic based on CTL, namely Game Analysis Logic (GAL), to model and reason about out games. The standard models of Game Theory (strategic games, extensiv games and coalition games) as well as their solution concepts (Nash equilibrium, subgame perfect equilibrium and co re),respectively, are express as models dels of GAL and formulas of GAL. Moreover, we study the alternatives of De Re and De Dicto quantification in the context of extensive games. We also show that two of the most representative game logics, namely Alternating-time lternating-Temp empor oral Logic (A ATL) TL) and Coalitional Game Logic (CGL), are fragments of GAL. We also characterize haracterize a class of multi-agent systems, which is based on the architecture Belief-Desire- Intention (BDI), for which there is a somehow equivalent class of games and vice-versa. As a consequence, criteria of rationality for agents can be directly applied to players and vice-versa. Game analysis formal tools can be applied to MAS as well. From a practical poin of view, we provide and develop a model-checker for GAL. In addition, we perform case studies using our prototype.

[pt] Esta tese apresenta um novo cálculo de sequente, correto e completo para a Lógica Proposicional Minimal Implicacional (M →). LMT → destina-se a ser usado para a busca de provas em M →, em uma abordagem bottom-up. A Terminação do cálculo é garantida por uma estratégia de aplicação de regras que força uma maneira ordenada no procedimento de busca de provas de tal forma que todas as combinações possíveis são exploradas. Para uma fórmula inicial α, as provas em LMT→ têm um limite superior de |α|.2 |α|+1+2·log2|α|, que juntamente com a estratégia do sistema, garantem a decidibilidade do mesmo. As regras do sistema são concebidas para lidar com a necessidade de repetição de hipóteses e a natureza de perda de contexto da regra → esquerda , evitando a ocorrência de loops e o uso de backtracking. Portanto, a busca de prova em LMT → é determinística, sempre executando buscas no sentido forward. LMT → tem a propriedade de permitir a extração de contramodelos a partir de buscas de prova que falharam (bicompletude), isto é, a árvore de tentativa de prova de um ramo totalmente expandido produz um modelo de Kripke que falsifica a fórmula inicial. A geração de contra-modelo (usando a semântica Kripke) é obtida como consequência da completude do sistema. LMT→ é implementado como um provador de teoremas interativo baseado no cálculo proposto aqui. Comparamos nosso cálculo com outros sistemas dedutivos conhecidos para M →, especialmente com Tableaux no estilo Fitting, um método que também tem a propriedade de ser bicompleto. Também propomos aqui uma tradução de LMT → para o verificador de prova Dedukti como uma forma de avaliar a correção da implementação que desenvolvemos, no que diz respeito à especificação do sistema, além de torná-lo mais fácil de comparar com outros sistemas existentes. / [en] This thesis presents a new sequent calculus called LMT→ that has the properties to be terminating, sound and complete for Propositional Implicational Minimal Logic (M →). LMT→ is aimed to be used for proof search in M →, in a bottom-up approach. Termination of the calculus is guaranteed by a strategy of rule application that forces an ordered way to search for proofs such that all possible combinations are stressed. For an initial formula α, proofs in LMT→ has an upper bound of |α|.2 |α|+1+2·log2|α|, which together with the system strategy ensure decidability. System rules are conceived to deal with the necessity of hypothesis repetition and the contextsplitting nature of → left, avoiding the occurrence of loops and the usage of backtracking. Therefore, LMT→ steers the proof search always in a forward, deterministic manner. LMT→ has the property to allow extractability of counter-models from failed proof searches (bicompleteness), i.e., the attempt proof tree of an expanded branch produces a Kripke model that falsifies the initial formula. Counter-model generation (using Kripke semantics) is achieved as a consequence of the completeness of the system. LMT→ is implemented as an interactive theorem prover based on the calculus proposed here. We compare our calculus with other known deductive systems for M →, especially with Fitting s Tableaux, a method that also has the bicompleteness property. We also proposed here a translation of LMT→ to the Dedukti proof checker as a way to evaluate the correctness of the implementation regarding the system specification and to make our system easier to compare to others.

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

[pt] A lógica iALC é uma lógica de descrição de caráter intuicionista, criada para lidar com textos jurídicos como alternativa à mais comumente utilizada lógica deôntica, por conseguir contornar problemas que se encontra ao utilizar esta última. Nesta dissertação, introduzimos os principais conceitos que formam iALC, argumentamos sobre sua utilização em vez de demais lógicas para formalização de leis, implementamos suas provas de correção e completude no assistente de provas L(existe algum)(para cada)N, e apresentamos uma proposta de formalização de leis brasileiras em iALC. Além disso, mostramos um exemplo de aplicação desta formalização para resolução de questões de múltipla escolha da primeira fase do exame da OAB, que tem por objetivo avaliar a aptidão dos candidatos para a prática da advocacia no Brasil. São vistos três exemplos de questões, cujas características são discutidas e comparadas umas às outras. / [en] The logic iALC is a description logic with an intuitionistic aspect to it, created to deal with legal texts as an alternative to the more common deontic logic, by being able to avoid problems found when utilizing the latter. In this dissertation, we introduce the core concepts which form iALC, debate on its utilization instead of other logics for legal formalization, implement the soundness and completeness proofs for it in the proof assistant L(there is some)(for each)N, and present a proposal for formalization of Brazilian law in iALC. Furthermore, we show an example of application of this formalization in order to reason on multiple choice questions of the first part of the OAB Exam (the Brazilian national Bar exam), which aims to test candidates for their aptitude to practice the law in Brazil. We will show three examples, whose characteristics will be discussed and then compared to the others.

[pt] O trabalho se destina a elucidar os motivos pelos quais Kant postula, na Crítica da Razão Pura, a tese de que os juízos infinitos da forma S é não-P não se reduzem aos afirmativos da forma S é P e nem aos negativos da forma S não é P. A distinção não parece se sustentar na abordagem extensional que é própria da Lógica Geral, uma vez que a equivalência entre juízos infinitos e negativos se revela incontornável. O método adotado segue as advertências dadas pelo próprio Kant e consiste em localizar algum passo da argumentação desenvolvida na Dialética Transcendental onde esta forma judicativa desempenhe um papel exclusivo e imprescindível. Duas hipóteses são examinadas. A primeira é que os juízos infinitos têm papel essencial na formulação e na solução da Primeira Antinomia da Razão Pura. A segunda é que têm função na formulação do Princípio da Determinação Completa, o qual é suscitado a pretexto de se elucidar o Ideal Transcendental da Razão Pura. Esta segunda hipótese se mostrará de fato a solução do nosso problema, mas terá repercussões sérias na interpretação de toda Crítica da Razão Pura, sobretudo ao pressupor um aspecto intensional da predicação que, no geral, tem sido desconsiderado e, por vezes, até mesmo recusado pelo comentário da filosofia de Kant. / [en] The task of this work is explaining why Kant claims in Critique of Pure Reason that infinite judgments of the form S is not-P are not reducible to the affirmative ones of the form S is P nor to the negative ones of the form S is not P The distinction does not seem justifiable in the extensional approach that is proper of General Logic, since the equivalence between infinite and negative judgments ends up to be inevitable. We adopt a method that is suggested by Kant s advices, which consists in looking for some moment in the discussion of Transcendental Dialectic where this form of judgment plays an exclusive and indispensable role. Two hypotheses are examined. The first one is that infinite judgments have an essential role in the formulation and in the solution of the First Antinomy of Pure Reason. The second one is that they have function in the formulation of the Principle of Complete Determination, which is mentioned in order to explain the Transcendental Ideal of Pure Reason. Actually, this second hypothesis will show up as the solution for our problem, but also will have strong repercussions at the interpretation of the whole Critique of Pure Reason, especially for presupposing an intensional aspect of predication that generally has been ignored and sometimes denied by Kantian philosophy s commentators.