[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] Atualmente, a maioria dos programas para computadores é obtida através da WEB. Como muitas vezes a procedência são fontes desconhecidas, é preciso se certificar de que o código se comporta como o esperado. A solução ideal seria verificar o código contra uma especificação de políticas de segurança ,contudo, isso pode consumir muito tempo.Uma outra alternativa é fazer com que o próprio código prove ser seguro. O conceito de proof-carryng code (PCC)é baseado nessa idéia : um programa carrega consigo uma prova de sua conformidade com certas políticas de segurança. Ou seja ,ele carrega uma prova a respeito de propriedades do próprio código. Portanto, os mesmos métodos froamsi usados para a verificação de programs podem se utilizados para esta tecnolgia. Considerando este fato,neste trabalho é estudado como cálculo de Hoare, em método formal para realizar a verificação de programas, aplicado a códigos-fonte escritos em uma linguagem de programação imperativa, pode ser útil á tecnica de PCC. Conseqüentemente, são pesquisados métodos para a geração de provas de correção de programas utilizando o método citado, para tornar possível a geração de provas de segurança para PCC utilizando o cálculo de Hoare. / [en] Nowdays most computer programs are obtained from the WEB. Since their source is usually unknown, it is necessary to be sure that the code of the program behaves as expected.The ideal solution would be verify the code against a specification of safety policies.However, this can take too much time.Another approach is making the code itself prove that it is safe. The concept os proof-carryng code (PCC) is based on this idea: a program carries a proof of its conformity with certain safety policies. That is , it carries a proof cencerning properties related to the code itself. Therefore, the same formal methods employed in formal verification of programs can be used in this tecnology. Due to this fact, in this work it is studied how Hoare logic applied to source codes written in an imperative programming language, which is a formal methods are researched to generate proofs of program correctness using the method explained, so that it can be possible to generate PCC safety programs with Hoare logic.

[pt] Este trabalho procura entender o que levou o Irã a passar de um papel de aliado ao de um inimigo dos Estados Unidos. Busca compreender como as hostilidades que passaram a existir somente entre Irã e Estados Unidos foram produzidas como uma ameaça para toda comunidade internacional. Na medida em que os Estados Unidos desempenham um papel de liderança nesta, um país que representa uma ameaça para os Estados Unidos passa a representar uma ameaça pública. O nacionalismo político Islâmico será apresentado como uma forma de resistência à lógica da modernidade. O ponto de ruptura entre estas nações ocorreu, segundo a visão norte-americana, no ano de 1979 com a chamada Revolução Iraniana – e, por conseguinte, com o sequestro da embaixada americana no Irã-, em contrapartida o momento de ruptura desta relação na visão iraniana se deu em 1953 com o Golpe de Estado que depôs o Primeiro-Ministro Muhammad Mossadeq. Também deve se levar em consideração que essa caracterização de um país como um todo, ou seja, sua política, religião, seus programas de desenvolvimento, etc como ameaçadores são um processo construtivo de valores. Este trabalho tenta desnaturalizar essa imagem ameaçadora que o Irã tem na comunidade internacional, que, cria as condições de possibilidade para práticas violentas dirigidas a esse Estado. Para isso, será utilizada a teoria pós-colonial, uma vez que os autores pós-coloniais acreditam que a dominação econômica do Ocidente sobre o Oriente, viabilizada principalmente pelo colonialismo, foi capaz de abarcar também a dominação cultural destes povos. / [en] This work seeks to understand what led Iran to move from a role of an ally to an enemy of the United States. Seeks to understand how the hostilities which now exist only between Iran and the United States were produced as a threat to all international community. To the extent that the United States play a leading role in this, a country that is a threat to the United States happens to represent a public menace. The Islamic political nationalism will be presented as a form of resistance to the logic of modernity. The breaking point occurred between these nations, according to the American view, in 1979 with the so-called Iranian Revolution - and therefore with the kidnapping of the American embassy in Iran , in return the time to break this relationship in Iranian view was in 1953 with the coup d état that deposed Prime Minister Muhammad Mossadeq. Should also take into consideration that this characterization of a country as a whole, their politics, religion, development programs, etc as threatening is a process of constructive values. This paper attempts to denaturalize this image "threatening" Iran has in the international community, which creates the conditions of possibility for violent actions directed to that State. This will be used to post-colonial theory, since postcolonial authors believe that the economic dominance of the West over the East, made possible mainly by colonialism, was able to encompass also the cultural domination of these peoples.

[pt] Esta dissertação tem por objetivo apresentar os resultados da pesquisa de mestrado em que se procurou evidenciar algumas características da relação de David Hume com a indução. Segundo a interpretação corrente, Hume é o responsável por mostrar que nossa razão não é capaz de justificar qualquer um de nossos raciocínios indutivos. O problema de Hume também se caracteriza por ser um problema acerca da racionalidade da ciência, pois se seu método principal, a indução, não pode receber suporte racional, parece lícito afirmar que o resultado de uma inferência indutiva é irracional. A fim de delinear o campo exato em que se insere a crítica humeana, este texto irá mostrar como Hume apresenta suas teorias acerca do raciocínio causal em seu Tratado da natureza humana, traçar as características exatas do raciocínio causal de Hume e confrontá-las com as formas de interpretação presentes em alguns de seus principais comentadores. Procuramos tornar claras as falhas apresentadas nestas interpretações. Em seguida trataremos de discutir algumas das mais celebradas interpretações da filosofia de Hume, centrando nossa análise nos textos de Mackie, Beauchamp e Mappes. O capítulo final tem por objetivo mostrar as características racionais que podem ser atribuídas aos raciocínios causais humeanos, salientando o caráter particular de suas inferências. Finalizando, mostraremos como a origem do princípio da cópia pode ser um exemplo do uso de inferências indutivas por parte de Hume, o que nos leva a considerações heterodoxas a respeito de sua visão a respeito da racionalidade. / [en] The aim of this work is to present the results of my master´s degree research, which tried to show some of the characteristics of David Hume´s approach to induction. According to the standard interpretation, Hume is responsible for showing that our reason is not able to justify any of our inductive reasonings. Hume´s problem also characterizes itself by being a problem about the rationality of science, for, since his main method, induction, cannot receive a rational foundation, it seems licit to assert that the result of any inductive inference is irrational. In order to precisely describe the Humean criticism I am going to show how Hume presents his theories concerning causal reasoning in this A Treatise of Human Nature, define the exact characteristics of causal reasoning according to him, and compare this analysis to those by some of his main critics. We shall try to bring to light the proposed inadequacy of the latter. Next we will discuss some of the most celebrated interpretations of Hume´s philosophy, specially those by of Mackie, Beauchamp and Mappes. The final chapter aims at showing the rational characteristics that can be assigned to Humean causal reasoning emphasizing the particular character of his inferences. Finally, we show how the origin of the copy principle can be an instance of the use of inductive inferences by Hume, which allows us to risk some heterodox hypotheses concerning his view of rationality.

[pt] Rótulos e bulas de agrotóxicos e afins são importantes instrumentos de comunicação entre as empresas que colocam esses produtos no mercado, os profissionais de saúde, os agricultores e os consumidores de produtos finais da cadeia agroalimentar. No sentido de minimizar possíveis riscos à saúde humana e ao meio ambiente, o emprego desses produtos deve ser realizado de forma adequada e segundo regulamentação em vigor. Com esse propósito, a Agência Nacional de Vigilância Sanitária (Anvisa) aprovou em meados de 2019 um novo marco regulatório para agrotóxicos, que incluiu a Resolução da Diretoria Colegiada - RDC número 296, de 29 de julho de 2019, dispondo sobre as informações toxicológicas para rótulos e bulas de agrotóxicos, afins e preservativos de madeira. Nesse contexto, o objetivo da dissertação é propor um conjunto de indicadores e métricas para monitorar e avaliar a regulamentação sobre rotulagem e bulas de agrotóxicos, afins e preservativos de madeira no Brasil, durante sua implementação. A pesquisa pode ser classificada como aplicada, metodológica e descritiva. Durante a fase aplicada propriamente dita, adotou-se a abordagem metodológica de construção de indicadores propostos pelo Ministério do Planejamento, Orçamento e Gestão, com incorporação de métodos multicritério de apoio à decisão, combinados com lógica fuzzy. Destacam-se como resultados: (i) o modelo lógico para proposição de indicadores para o monitoramento e avaliação da implementação da regulamentação em foco; (ii) a ferramenta fuzzy multicritério para seleção e hierarquização dos indicadores inicialmente propostos; e (iii) um conjunto consistente de indicadores hierarquizados por categoria de requisitos legais da RDC número 296/2019, a serem selecionados posteriormente pela Anvisa. / [en] Pesticide labeling and packaging leaflets are essential communication instruments between pesticide companies, health professionals, farmers, and consumers of final products in the agri-food chain. To minimize possible risks to human health and the environment, the use of these products must be carried out appropriately. With this purpose, the National Health Surveillance Agency (Anvisa) approved in mid-2019 a new regulatory framework for pesticides and wood preservatives, which included the Resolution of the Collegiate Board - RDC No. 296, of July 29, 2019, concerning toxicological information for labeling and packaging leaflets of these products. In this context, this dissertation aims to propose a set of indicators and respective metrics for monitoring and evaluating (ME) the regulation on pesticide and wood preservative labeling and packaging leaflets in Brazil during its implementation. This research can be classified as applied, methodological and descriptive. During the applied phase, the methodological approach proposed by the Ministry of Planning, Budget, and Management for building indicators was adopted, incorporating multicriteria methods of decision support combined with fuzzy logic. The main results are highlighted as follows: (i) a logic model to frame evaluation questions concerning the focused regulation; (ii) a fuzzy multicriteria tool for the ranking indicators associated with the evaluation questions; and (iii) a set of indicators ranked by category of legal requirements of RDC No. 296/2019 to be subsequently chosen by the Regulatory Agency.

[pt] Turbinas a gás são equipamentos muito complexos e caros. No caso de falha em uma turbina, há obviamente perdas diretas, mas as indiretas são normalmente muito maiores, uma vez que tal equipamento é crítico para a operação de instalações industriais, aviões e veículos pesados. Portanto, é fundamental que turbinas a gás sejam providas com um sistema eficiente de monitoramento e diagnóstico. Isto é especialmente relevante no Brasil, cuja frota de turbinas tem crescido muito nos últimos anos, devido, principalmente, ao aumento do número de usinas termelétricas e ao crescimento da aviação civil. Este trabalho propõe um Sistema de Inferência Fuzzy (SIF) com extração automática de regras para diagnóstico de desempenho de turbinas a gás aeronáuticas. O sistema proposto faz uso de uma abordagem residual – medições da turbina real são comparadas frente a uma referência de turbina saudável – para tratamento dos dados brutos de entrada para os módulos de detecção e isolamento, que, de forma hierárquica, são responsáveis por detectar e isolar falhas em nível de componentes, sensores e atuadores. Como dados reais de falhas em turbinas a gás são de difícil acesso e de obtenção cara, a metodologia é validada frente a uma base de dados de falhas simuladas por um software especialista. Os resultados mostram que o SIF é capaz de detectar e isolar corretamente falhas, além de fornecer interpretabilidade linguística, característica importante no processo de tomada de decisão no contexto de manutenção. / [en] A Gas turbine is a complex and expensive equipment. In case of a failure indirect losses are typically much larger than direct ones, since such equipment plays a critical role in the operation of industrial installations, aircrafts, and heavy vehicles. Therefore, it is vital that gas turbines be provided with an efficient monitoring and diagnostic system. This is especially relevant in Brazil, where the turbines fleet has risen substantially in recent years, mainly due to the increasing number of thermal power plants and to the growth of civil aviation. This work proposes a Fuzzy Inference System (FIS) with automatic rule extraction for gas path diagnosis. The proposed system makes use of a residual approach – gas path measurements are compared to a healthy engine reference – for preprocessing raw input data that are forwarded to the detection and isolation modules. These operate in a hierarchical manner and are responsible for fault detection and isolation in components, sensors and actuators. Since gas turbines failure data are difficult to access and expensive to obtain, the methodology is validated by using a database fault simulated by a specialist software. The results show that the SIF is able to correctly detect and isolate failures and to provide linguistic interpretability, which is an important feature in the decision-making process regarding maintenance.

In 2020 Parusiński and Rond proved that every algebraic set X ⊂ R^n is homeomorphic to an algebraic set X’ ⊂ R^n which is described globally (and also locally) by polynomial equations whose coefficients are real algebraic numbers. In general, the following problem was widely open: Open Problem. Is every real algebraic set homeomorphic to a real algebraic set defined by polynomial equations with rational coefficients? The aim of my PhD thesis is to provide classes of real algebraic sets that positively answer to above Open Problem. In Chapter 1 I introduce a new theory of real and complex algebraic geometry over subfields recently developed by Fernando and Ghiloni. In particular, the main notion to outline is the so called R|Q-regularity of points of a Q-algebraic set X ⊂ R^n. This definition suggests a natural notion of a Q-nonsingular Q-algebraic set X ⊂ R^n. The study of Q-nonsingular Q-algebraic sets is the main topic of Chapter 2. Then, in Chapter 3 I introduce Q-algebraic approximation techniques a là Akbulut-King developed in collaboration with Ghiloni and the main consequences we proved, that are, versions ‘over Q’ of the classical and the relative Nash-Tognoli theorems. Last results can be found in in Chapters 3 & 4, respectively. In particular, we obtained a positive answer to above Open Problem in the case of compact nonsingular algebraic sets. Then, after extending ‘over Q’ the Akbulut-King blowing down lemma, we are in position to give a complete positive answer to above Open Problem also in the case of compact algebraic sets with isolated singularities in Chapter 4. After algebraic Alexandroff compactification, we obtained a positive answer also in the case of non-compact algebraic sets with isolated singularities. Other related topics are investigated in Chapter 4 such as the existence of Q-nonsingular Q-algebraic models of Nash manifolds over every real closed field and an answer to the Q-algebrization problem for germs of an isolated algebraic singularity. Appendices A & B contain results on Nash approximation and an evenness criterion for the degree of global smoothings of subanalytic sets, respectively.

Very few standards exist for tting products to people. Footwear fit is a noteworthy example for consumer consideration when purchasing shoes. As a result, footwear manufacturing industry for achieving commercial success encountered the problem of developing right footwear which is fulfills consumer's requirement better than it's competeries. Mass customization starts with understanding individual customer's requirement and it finishes with fulllment process of satisfying the target customer with near mass production efficiency. Unlike any other consumer product, personalized footwear or the matching of footwear to feet is not easy if delivery of discomfort is predominantly caused by pressure induced by a shoe that has a design unsuitable for that particular shape of foot. Footwear fitter have been using manual measurement for a long time, but the combination of 3D scanning systems with mathematical technique makes possible the development of systems, which can help in the selection of good footwear for a given customer. This thesis, provides new approach for addressing the computerize footwear fit customization in industry problem. The design of new shoes starts with the design of the new shoe last. A shoe last is a wooden or metal model of human foot on which shoes are shaped. Despite the steady increase in accuracy, most available scanning techniques cause some deficiencies in the point cloud and a set of holes in the triangle meshes. Moreover, data resulting from 3D scanning are given in an arbitrary position and orientation in a 3D space. To apply sophisticated modeling operations on these data sets, substantial post-processing is usually required. We described a robust algorithm for filling holes in triangle mesh. First, the advance front mesh technique is used to generate a new triangular mesh to cover the hole. Next, the triangles in initial patch mesh is modified by estimating desirable normals instead of relocating them directly. Finally, the Poisson equation is applied to optimize the new mesh. After obtaining complete 3D model, the result data must be generated and aligned before taking this models for shape analysis such as measuring similarity between foot and shoe last data base for evaluating footwear it. Principle Component Analysis (PCA), aligns a model by considering its center of mass as the coordinate system origin, and its principle axes as the coordinate axes. The purpose of the PCA applied to a 3D model is to make the resulting shape independent to translation and rotation asmuch as possible. In analysis, we applied "weighted" PCA instead of applying the PCA in a classical way (sets of 3D point-clouds) for alignment of 3D models. This approach is based on establishing weights associated to center of gravity of triangles. When all of the models are aligned, an efficient algorithm to cut the model to several sections toward the heel and toe for extracting counters is used. Then the area of each contour is calculated and compared with equal sections in shoe last data base for finding best footwear fit within the shoe last data base.

[pt] O meu objetivo é investigar o colapso e abandono do Tractatus tomado como um projeto para desenvolver a atraente imagem de uma lógica completamente combinatória, sintática e neutra. Há neste projeto uma tensão insolúvel entre a imagem de uma lógica neutra e a demanda que ela deveria ser usada para analisar completamente os fatos do mundo. Há mais articulações lógicas que a lógica tractariana com suas tautologias, contradições e verafuncionalidade pode expressar. Assim eu lido aqui com quatro colapsos inevitáveis do Tractatus, nomeadamente: I) a composicionalidade; II a tabela de verdade, III) a Bildkonzeption; e IV) a Neutralidade da Lógica. Há também quatro pontos centrais que eu cubro com esta investigação: 1) Problemas com a expressao vero-funcional de cores e números, e sua relação com intuições funcionais e espaciais; 2) o papel central e limites da tabela de verdade como um sistema notacional privilegiado para revelar a essência da linguagem e para evitar absurdos; 3) a crítica da interpretação recorrente de isomorfismo entre proposições elementares e fatos atômicos no Tractatus; 4) o papel central de um holismo tractariano que forma o pano de fundo para inevitável colisão entre lógica e sua aplicação. Eu então evidencio o tipo de invasão de organizações e elementos empíricos no (alegado) domínio neutro da lógica. Lógica não poderia então tomar conta de si mesma. / [en] My aim is to investigate the collapse and abandonment of the Tractatus held as a project to develop the attractive picture of a logic completely combinatorial, syntactical and neutral. There is in this project an unsolvable tension between this image of a neutral logic and the demand that it must be used to completely analyze the facts in the world. There are more logical connections than the tractarian logic, with its tautologies, contradictions and truth-functionality, can express. Thereby I deal here with four unavoidable collapses of Tractatus maininterdependent pillars, namely: I) the Compositionality; II) the truth tables; III) the Bildkonzeption; and IV) the Neutrality of Logic. There are four central points that I cover respectively in this investigation: 1) Problems with a truth-functional expression of colors and numbers, and its relation with functional and spatial intuitions; 2) the central role and limits of the truth tables as a special notation to reveal the essence of the language and to avoid absurdities; 3) a criticism of the recurrent interpretation of an isomorphism between elementary propositions and atomic facts in the Tractatus; and 4) the central role of a tractarian holism which forms the background to the unavoidable collision between logic and its application. I highlight then the kind of conceptual invasion of empirical arrangements and elements in the (allegedly) neutral domain of logic. Logic could not at last take care of itself.

[pt] A dissertação tem como objetivo apresentar uma defesa do princípio de nãocontradição, uma defesa sustentada por dois argumentos. No primeiro argumento, coloca-se em destaque a relação entre a validade do princípio de não-contradição e a determinação do sentido das expressões linguísticas, em particular, a determinação do sentido dos termos gerais usados como predicados em frases singulares. Utilizar uma frase para dizer de um objeto que ele possui e, sob o mesmo aspecto, não possui uma mesma característica resultaria na indeterminação do sentido, a saber, que nada seria dado a entender pela frase. O segundo argumento pretende estabelecer uma relação entre uso de instâncias do princípio de não contradição e a capacidade de identificar objetos particulares. Para se referir determinadamente a um único particular, de tal maneira que seja possível pensar sobre este como sendo um sujeito de predicações, é preciso que se identifique esse particular através de um termo sortal e não simultaneamente através de um sortal oposto. Mais especificamente: tentar se referir a algo como sendo e não sendo de um certo tipo resultaria na indeterminação da referência, viz. não haveria identificação de um único objeto. / [en] The dissertation aims to present a defense of the principle of noncontradiction, a defense supported by two arguments. In the first argument, it is emphasized the relation between the validity of the principle of non-contradiction and the determination of the sense of linguistic expressions, in particular, the determination of the sense of general terms used as predicates in singular sentences. To say of an object that it has and, in the same respect, does not have a certain characteristic would result in the indetermination of sense, namely that nothing would be understood by the sentence. The second argument seeks to establish a relation between the use of instances of the principle of non-contradiction and the ability to identify particular objects. To refer specifically to a single individual, in such a way that it can be thought of as a subject of predication, it is necessary to identify this individual by means of a sortal term and not simultaneously through an opposite sortal. More precisely: trying to refer to a thing as being and not being of a certain sort would result in the indetermination of the reference, viz. no single object would be identified.