[pt] Neste trabalho investigou-se o emprego dos recentes algoritmos de minimização de funções não diferenciáveis para a resolução do problema da síntese de filtros digitais FIR de fase não linear. O problema desta síntese correspondente a um problema de Aproximações de Funções quando o domínio e o contradomínio da função são corpos diferentes, i.e. real e complexo respectivamente. Serão revistos definições e propriedades dos filtros FIR, as técnicas de síntese para o caso de resposta de fase linear e não linear, para a seguir, apresentar a teoria e implementação da Otimização de Funções não Diferenciáveis. Exemplos e extensões desta teoria também serão apresentados. / [en] This work will describes the use of the recent techniques of non smooth optimization to the synthesis of non-linear phase FIR filters. The problem of such synthesis corresponds to a problem of Approximation of Functions when the domain and the image sets of the function are different fields, i.e. real and complex respectively. A revision of the theory of FIR filters with a survey of the linear and non linear phase usual synthesis non-smooth optimization theory and implementation. Together with design examples will follow. An extension of these theories will be suggested.

[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] A história recente da Lógica Matemática foi marcada por alguns conflitos entre diferentes correntes filosóficas, cada uma buscando contextualizar a atividade matemática a partir de seu próprio prisma analítico e, por meio disso, tentando conquistar para si mesma o pódio fundacional das Ciências Formais Tais discussões, perenes o bastante para ainda quedarem sem solução, foram fortemente impactadas pela apropriação semântica de alguns resultados técnicos obtidos no campo da teoria da prova, o que redefiniu a relação existente entre as abordagens clássica e intuicionista na matemática. Neste contexto, a presente dissertação tem por finalidade realizar uma descrição da emergente literatura de propostas integrativas entre diferentes sistemas lógicos e matemáticos (apelidadas por Dag Prawitz de ecumenismo lógico), além de investigar alguns impactos que mudanças formais poderiam ocasionar nas concepções filosóficas de algumas teorias matemáticas. No capítulo introdutório, traçamos um panorama geral desta nova proposta ecumênica e analisamos com mais atenção o conflito entre as lógicas Clássica, Intuicionista e Minimal, considerado por muitos como um dos mais influentes na literatura contemporânea. No segundo capítulo, este trabalho fornece uma contribuição original para a literatura ao criar uma nova abordagem ecumênica, além de provar algumas equivalências no interior do sistema Clássico-Intuicionista recentemente criado por Prawitz e compará-lo com uma lógica que criamos usando esta nova abordagem. No terceiro capítulo, contribuímos tanto com a abordagem tradicional quanto com nossa abordagem original ao criar e comparar dua lógicas ecumênicas Minimal-Intuicionistas. Por fim, realizamos uma breve revisão do tímido estado da arte no último capítulo, oferecendo um novo esquema conceitual de interpretação dos sistemas ecumênicos e comentando alguns aspectos promissores do campo, que poderão vir a ser melhor trabalhados no futuro. / [en] The recent history of Mathematical Logic was marked by some conficts between different philosophical positions, each trying to contextualize mathematical activity from its own analytical viewpoint and, with this, trying to conquer the foundational podium of the formal sciences for itself. Such discussions, lasting enough to remain without a solution, were strongly impacted by the semantical appropriation of some technical results obtained in the field of proof theory, which redefined the relation between the classical and intuitionistic approaches to mathematics. In this context, the present dissertation aims to describe the emergent literature about the integration of different logical and mathematical systems (nicknamed logical ecumenism by Dag Prawitz), in addition to investigating some impacts that those formal changes could have on the philosophical conceptions of some mathematical theories. In the introductory chapter, we have outlined a general overview of this new ecumenical proposal and analysed in greater depht the conflicts between Classical, Intuitionistic and Minimal logic, considered by many as one of the most influent on the contemporary literature. In the second chapter, this work provides an original contribution to the literature by creating a new ecumenical approach, in addition to proving some equivalencies within Prawitz s recently created Classical-Intuitionist system, and compares it with the logical system we have created using this new approach. In the third chapter, we contribute both to the traditional approach and our original approach by creating and comparing two Minimal-Intuitionist ecumenical logics. Finally, we briefly review the timid state of the art in the last chapter, offering a new conceptual framework for interpreting ecumenical systems, as well as commenting on some promising aspects of the field, which may be better analyzed in the future.

[pt] Lógica Proposicional Dinâmica (PDL) é um sistema lógico multi-modal utilizada para especificar e verificar propriedades em programas sequenciais. Redes de Petri são um formalismo largamente utilizado na especificação de sistemas concorrentes e possuem uma interpretação gráfica bastante intuitiva. Neste trabalho apresentam-se extensões da Lógica Proposicional Dinâmica onde os programas são substituídos por Redes de Petri. Define-se uma codificação composicional para as Redes de Petri através de redes básicas, apresentando uma semântica composicional. Uma axiomatização é definida para a qual o sistema é provado ser correto, e completo em relação à semântica proposta. Três Lógicas Dinâmicas são apresentadas: uma para efetuar inferências sobre Redes de Petri Marcadas ordinárias e duas para inferências sobre Redes de Petri Estocásticas marcadas, possibilitando a modelagem de cenários mais complexos. Alguns sistemas dedutivos para essas lógicas são apresentados. A principal vantagem desta abordagem concerne em possibilitar efetuar inferências sobre Redes de Petri [Estocásticas] marcadas sem a necessidade de traduzí-las a outros formalismos. / [en] Propositional Dynamic Logic (PDL) is a multi-modal logic used for specifying and reasoning on sequential programs. Petri Net is a widely used formalism to specify and to analyze concurrent programs with a very intuitive graphical representation. In this work, we propose some extensions of Propositional Dynamic Logic for reasoning about Petri Nets. We define a compositional encoding of Petri Nets from basic nets as terms. Second, we use these terms as PDL programs and provide a compositional semantics to PDL Formulas. Then we present an axiomatization and prove completeness regarding our semantics. Three versions of Dynamic Logics to reasoning with Petri Nets are presented: one of them for ordinary Marked Petri Nets and two for Marked Stochastic Petri Nets yielding to the possibility of model more complex scenarios. Some deductive systems are presented. The main advantage of our approach is that we can reason about [Stochastic] Petri Nets using our Dynamic Logic and we do not need to translate it into other formalisms. Moreover our approach is compositional allowing for construction of complex nets using basic ones.

[pt] A dissertação consiste em uma reflexão sobre a noção de existência. É feita, de início, uma breve exposição a respeito do argumento ontológico de Santo Anselmo e o tipo de concepção de existência que ele demanda. A seguir, é empreendida uma breve investigação a respeito da visão de três pilares de nossa tradição filosófica a respeito da noção de existência: Hume, Kant e Frege. Suas concepções são estudadas, até certo ponto, em separado, a fim de que possam ser trazidos à luz seus principais aspectos e os contornos peculiares que conferem à noção de que pretendem dar conta. Posteriormente, são postas lado a lado em um cotejo de algumas de suas mais relevantes semelhanças e discrepâncias. A esse estudo, segue-se uma investigação crítica. Em primeiro lugar, é exposta a parte negativa desta: algumas observações a respeito de problemas envolvidos em cada um dos tipos de concepção da existência exemplificados nas partes precedentes, mescladas a reflexões a respeito da relação da existência com noções como quantificação e indivíduo, às quais dão ensejo. Em segundo lugar, sua parte positiva: com base nas observações já feitas, algumas sugestões de como dar conta de certos aspectos relevantes da noção de existência. A dissertação inclui ainda um apêndice em que se leva a cabo uma breve incursão no pensamento aristotélico. Mais precisamente, será investigada a relação entre a existência e a quantificação no contexto da teoria do quadrado das oposições, tal como formulada no célebre tratado De Interpretatione. / [en] The dissertation consists of a reflection on the notion of existence. At first, a brief exposition about St. Anselms ontological argument and the kind of conception of existence that it demands is made. After that, a brief investigation regarding the vision of the notion of existence of three main pillars of our philosophical tradition - Hume, Kant and Frege - is undertaken. To a certain extent, their conceptions are studied separately, so that the main aspects and peculiar outline that they convey to the notion of which they intend to give an account can be brought to light. Subsequently, these conceptions are put side by side in a comparison of some of their most relevant similarities and discrepancies. This study is followed by a critical investigation. First, its negative part is exposed: some observations regarding problems involved in each one of the kinds of conception of existence exemplified in the precedent parts, mixed with reflections on the relation between existence and notions such as that of individual and quantification to which they give rise. Secondly, its positive part: based on the observations already made, some suggestions on how to give an account of some relevant aspects of the notion of existence. The dissertation also contains an appendix in which a brief incursion in the aristotelian thought is undertaken. More specifically, it consists of an investigation regarding the relation between existence and quantification in the context of the theory of the square of oppositions as formulated in the famous treatise De Interpretatione.

[pt] A aplicação de linguagens declarativas baseadas na programação em lógica tem sido bastante difundida devido ao grande interesse hoje existente na área de Inteligência Artificial. Porém, o uso destas linguagens ainda não é muito evidente devido à restrições de desempenho, portabilidade, capacidade de integração com outras linguagens, etc. O presente trabalho contém a definição e implementação de uma extensão de programação em lógica para o C, denominada CLog, que têm como objetivo suprir as deficiências acima, permitindo, principalmente, a implementação de aplicações que apresentem características de programação em lógica integrada à programação imperativa em um mesmo ambiente de desenvolvimento. / [en] The use of declarative languages based in logic programming has been spread out due to the great interest in Artificial Intelligence. However, the use of these languages is not evident yet due to performance, portability, integration to other languages capability and other restrictions. This work contains the definition and implementation of a logic programming extension for C called Clog, which intends to cover the above deficiencies, allowing, mainly, the implementation of applications that have logic programming characteristics integrated to interative programming in the same development environment.

[pt] A primeira parte deste trabalho consiste num estudo das desigualdades lineares que aparecem na síntese de funções lógicas por single-threshold. São desenvolvidas condições necessárias e suficientes para existência de solução, e também estabelecidas condições para a redução das desigualdades. Na segunda parte é proposto um método para calcular uma solução ótima para o sistema, sob certas condições de projeto. Finalmentesão apresentados métodos para realiza, com multithreshold devices, funções lógicas não realizáveis por single-threshold devices. / [en] The first part of this thesis is a theoretical study of sets of inequalities that appear in the synthesis of logical sufficient conditions are developd for existence of solution of the inequalities. In the second part, a numerical method for calculating proposed. Following this development, logical functions that cannot be realized by a single-threshold device are studied. Using the conditions developed before for single- threshold, methods are presented for realization of these functions by multithreshold devices.

[pt] O objetivo desta dissertação é construir um tableaux linear intuicionista a partir de um cálculo de sequentes relevante clássico. Os passos principais dessa construção são: i) tradução das regras do cálculo dos sequentes relevante clássico para regras de tableaux (capítulo 3), usando a estratégia apresentada por D Agostino et al. em Tableau Methods for Substructural Logic. ii) construção de um tableaux linear clássico através da linearização do tableaux clássico relevante (capítulo 4). iii) apresentar um tableau intuicionista ao estilo Fitting, em que são adicionados rótulos T s e F s às fórmulas (capítulo 5). / [en] The main goal of this master tesis is intuitionistic linear tableaux from a relevant sequent calculus. The central steps are: i) Apply D Agostino et al. strategy to translate classical relevant sequent calculus rules to tableaux rules for classical relevant logic (Chapter 3). ii) Use Meyer et al. strategy to linearize the classical relevant tableaux (Chapter 4). iii) Build a new intuicionistic linear tableaux with Fitting labels.

[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] A Lógica é hoje em dia vista como uma ciência matemática fundamentalmente ligada à faculdade do entendimento, e pouco relacionada com nossa capacidade de imaginar ou conceber. Desta forma, sob a alcunha de psicologismo, costuma-se descartar qualquer associação da lógica à conceptividade ou à imaginação como espúria e mal colocada. Esta tese de doutorado tem como objetivo mostrar que, contrariamente ao que se costuma crer, há na lógica, tomada como uma ciência, um inegável emprego metodológico da faculdade da conceptividade ou da imaginação. Para mostrar isto, primeiramente examinamos sobre bases autônomas o princípio da conceptividade, segundo o qual a proposição p é concebível se e semente se p é possível. Investigamos as principais posições contemporâneas contra e a favor deste princípio e chegamos a uma versão qualificada do princípio, que defendemos ser livre de contraexemplos. Terá sido mostrado, portanto, que, sob certas condições, há uma relação essencial entre conceitos modais aléticos (possibilidade, necessidade, contingência, impossibilidade) e nossa faculdade de conceber ou imaginar: o que é concebível é possível - ainda que nem sempre o que é inconcebível seja impossível. Em seguida, mostramos como o princípio da conceptividade foi um instrumento insubstituível, nas mãos dos grandes pioneiros da lógica, em uma tarefa muito bem delimitada: a codificação de novas linguagens lógicas. Defendemos, por conseguinte, que Aristóteles, quando primeiramente codificou a lógica de proposições categóricas, e Frege, quando elaborou a lógica funcional e quantificada, foram obrigados a recorrer à conceptividade como parâmetro básico para examinar a correção expressiva da linguagem que estavam codificando e para aferir a validade lógica de diversas proposições e argumentos. Com vistas a tornar claro o lugar da noção de conceptividade dentro da lógica, examinamos a lógica e a epistemologia de Aristóteles e, sobretudo, de Frege, nas quais encontramos elementos concretos que apontam para o emprego desta noção dentro do contexto primitivo de codificação lógica a que nos reportamos. Enfatizamos que, no contexto em que estes autores se encontravam, não havia opções epistemológicas para examinar e avaliar sua lógica a não ser o recurso princípio da conceptividade. / [en] Logic is seen today as a mathematical science fundamentally linked to the faculty of understanding, unrelated to our capacity of imagining or conceiving. Under the label psychologism, one usually considers any association between logic and conceivability (or imagination) as spurious and misled. This doctoral thesis has as its goal showing that, contrarily to what is ordinarily thought, there is in logic, understood as a science, an undeniable methodological employment of the faculty of conceivability or imagination. In order to show this, we firstly examine the conceivability principle (the proposition p is conceivable if and only if p is possible) on autonomous basis. We examine the main contemporary positions against and in favor of this principle and come to a qualified version of the principle, which we purport to be free of counterexamples; it will have been shown, therefore, that, under certain circumstances, there is an essential relation between modal concepts (possibility, necessity, contingency, impossibility) and our faculty of conceiving or imagining: whatever is conceivable is possible - even though it is not always true that whatever is inconceivable is impossible. Secondly, we show how the conceivability principle was an irreplaceable tool in the hands of the great pioneers of logic, in a very well delimited task: codifying new logical languages. Therefore, we hold that Aristotle, as he firstly codified the logic of categorical propositions, and Frege, as he elaborated quantified functional logic, were bound to employ conceivability as a basic parameter so as to examine the expressive correctness of the language they were codifying and determine the validity of various propositions and arguments. In order to make clear the place of conceivability in logic, we examine Aristotle´s Frege´s logic and epistemology and find concrete elements indicating the employment of this notion in the primitive context of logical codification we have mentioned. We emphasize that, in the context in which these authors were working, there were no epistemological options other than the resource to the conceivability principle.