CoordenaÃÃo de AperfeiÃoamento de Pessoal de NÃvel Superior / VÃrios problemas computÃveis podem ser resolvidos de maneira mais eficiente ou mais natural atravÃs de algoritmos probabilÃsticos, o que mostra que o uso de tais algoritmos à bastante relevante em computaÃÃo. Entretanto, os algoritmos probabilÃsticos podem retornar uma resposta errada com uma certa probabilidade. Observe, ainda que o uso de algoritmos probabilÃsticos nÃo resolve problemas nÃo computÃveis. A Complexidade Computacional caracteriza a complexidade de um problema a partir da quantidade de recursos computacionais, como espaÃo e tempo, para resolvÃ-lo. Problemas que tem a mesma complexidade compÃem uma classe. As classes de complexidade computacional sÃo relacionadas atravÃs de uma hierarquia. A Complexidade Descritiva usa lÃgicas para expressar os problemas e capturar classes de complexidade computacional no sentido de expressar todos, e apenas, os problemas desta classe. Dessa forma, a complexidade de um problema nÃo depende de fatores fÃsicos, como tempo e espaÃo, mas apenas da expressividade da lÃgica que o define. Resultados importantes da Ãrea mostraram que vÃrias classes de complexidade computacional podem ser caracterizadas por lÃgicas. Por exemplo, a classe NP foi mostrada equivalente à classe dos problemas expressos pelo fragmento existencial da LÃgica de Segunda Ordem. Este estreito relacionamento entre tais Ãreas permite que alguns resultados da Ãrea de LÃgica sejam transferidos para a de Complexidade Computacional e vice-versa. Apesar da importÃncia de algoritmos probabilÃsticos e da Complexidade Descritiva, existem poucos resultados de caracterizaÃÃo, por lÃgicas, das classes de complexidade computacional probabilÃsticas. Neste trabalho, buscamos mostrar caracterizaÃÃes para cada uma das classes de complexidade probabilÃsticas de tempo polinomial. Nos nossos resultados, utilizamos quantificadores generalizados de segunda ordem para simular a aceitaÃÃo das mÃquinas nÃo-determinÃsticas dessas classes. Achamos caracterizaÃÃes lÃgicas na literatura apenas para as classes PP e BPP. No primeiro caso, a lÃgica utilizada era a de primeira ordem adicionada de um quantificador maioria de segunda ordem. Com a abordagem criada neste trabalho, conseguimos obter uma prova alternativa para a caracterizaÃÃo de PP. Com essa mesma metodologia, tambÃm conseguimos caracterizar a classe ⊕P atravÃs de uma lÃgica com um quantificador de paridade. No caso de BPP, existia um resultado que utilizava uma lÃgica com semÃntica probabilÃstica. Usando nossa abordagem de quantificadores generalizados, conseguimos obter uma caracterizaÃÃo alternativa para essa classe. Com o mesmo mÃtodo, conseguimos caracterizar as classes probabilÃsticas semÃnticas RP, coRP, ZPP e a classe semÃntica NP∩coNP. Por fim, mostramos uma aplicaÃÃo dos resultados de Complexidade Descritiva na criaÃÃo de algoritmos atravÃs de uma especificaÃÃo lÃgica. / Many computable problems can be solved more efficiently or in a more natural way through probabilistic algorithms, which shows that the use of such algorithms is quite relevant in Computer Science. However, probabilistic algorithms may return a wrong answer with a certain probability. Also, the use of probabilistic algorithms does not solve problems that are not computable. In Computational Complexity, the complexity of a problem is characterized based on the amount of computational resources, such as space and time, needed to solve it. Problems that have the same complexity compose the same class. The computational complexity classes are related by a hierarchy. In Descriptive Complexity, a logic is used to express problems and capture computational complexity classes in order to express all and only the problems of this class. Thus, the complexity of a problem does not depend on physical factors, such as time and space, but only on the expressiveness of the logic that defines it. Important results of the area states that several classes of computational complexity can be characterized by a logic. For example, the class NP has been shown equivalent to the class of problems expressed by the existential fragment of Second-Order Logic. This close relationship between these areas allows some results about Logics to be transferred to Computational Complexity and vice versa. Despite of the importance of probabilistic algorithms and of Descriptive Complexity, there are few results on the characterization, by a logic, of probabilistic computational complexity classes. In this work, we show characterizations for each of the polinomial time probabilistic complexity classes. In our results, we use second-order generalized quantifiers to simulate the acceptance of the nondeterministic machines of these classes. We found Logical characterizations in the literature only for classes PP and BPP. In the first case, the logic employed was the first-order added by a quantifier most of second-order. With the approach established in this work, we obtain an alternative proof for the characterization of PP. With the same methodology, we also characterize the class ⊕P through a logic with a second-order parity quantifier. In the case of BPP , there was a result that used a logic with probabilistic semantics. Using our approach of generalized quantifiers, we obtain an alternative characterization for this class. With the same method, we were able to characterize the probabilistic semantic classes RP, coRP, ZPP and the semantic class NP ∩ coNP. Finally, we show an application of Descriptive Complexity results in the creation of algorithms from a logic specification.

Conselho Nacional de Desenvolvimento CientÃfico e TecnolÃgico / Este trabalho à um estudo sobre as origens da LÃgica MatemÃtica e os limites da sua aplicabilidade ao desenvolvimento formal da MatemÃtica. Primeiramente, à apresentada a teoria aritmÃtica de Dedekind, a primeira teoria a fornecer uma definiÃÃo precisa para os nÃmeros naturais e com base nela demonstrar todos os fatos comumente conhecidos a seu respeito. à tambÃm apresentada a axiomatizaÃÃo da AritmÃtica feita por Peano, que de certa forma simplificou a teoria de Dedekind. Em seguida, à apresentada a ome{german}{Begriffsschrift} de Frege, a linguagem formal que deu origem à LÃgica moderna, e nela sÃo representadas as definiÃÃes bÃsicas de Frege a respeito da noÃÃo de nÃmero. Posteriormente, à apresentado um resumo de questÃes importantes em fundamentos da MatemÃtica durante as primeiras trÃs dÃcadas do sÃculo XX, iniciando com os paradoxos na Teoria dos Conjuntos e terminando com a doutrina formalista de Hilbert. Por fim, sÃo apresentados, em linhas gerais, os teoremas de incompletude de GÃdel e o conceito de computabilidade de Turing, que apresentaram respostas precisas Ãs duas mais importantes questÃes do programa de Hilbert, a saber, uma prova direta de consistÃncia para a AritmÃtica e o problema da decisÃo, respectivamente. / This work is a study about the origins of Mathematical Logic and the limits of its applicability to the formal development of Mathematics. Firstly, Dedekindâs arithmetical theory is presented, which was the first theory to provide a precise definition for natural numbers and to demonstrate relying on it all facts commonly known about them. Peanoâs axiomatization for Arithmetic is also presented, which in a sense simplified Dedekindâs theory. Then, Fregeâs Begriffsschrift is presented, the formal language from which modern Logic originated, and in it are represented Fregeâs basic definitions concerning the notion of number. Afterwards, a summary of important topics on the foundations of Mathematics from the first three decades of the twentieth century is presented, beginning with the paradoxes in Set Theory and ending with Hilbertâs formalist doctrine. At last, are presented, in general terms, GÃdelâs incompleteness. theorems and Turingâs computability concept, which provided precise answers to the two most important points in Hilbertâs program, to wit, a direct proof of consistency for Arithmetic and the decision problem, respectively. Keywords: 1. Mathematical Logic 2. Foundations of Mathematics 3. GÃdelâs incompleteness theorems

The topic of this thesis lies in the intersection between proof theory and algebraic logic. The main object of discussion, constructive reasoning, was introduced at the beginning of the 20th century by Brouwer, who followed Kant’s explanation of human intuition of spacial forms and time points: these are constructed step by step in a finite process by certain rules, mimicking constructions with straightedge and compass and the construction of natural numbers, respectively. The aim of the present thesis is to show how classical reasoning, which admits some forms of indirect reasoning, can be made more constructive. The central tool that we are using are induction principles, methods that capture infinite collections of objects by considering their process of generation instead of the whole class. We start by studying the interplay between certain structures that satisfy induction and the calculi for some non-classical logics. We then use inductive methods to prove a few conservation theorems, which contribute to answering the question of which parts of classical logic and mathematics can be made constructive.

In this thesis we study the concept of well quasi-order, originally developed in order theory but nowadays transversal to many areas, in the over-all context of proof theory - more precisely, in reverse mathematics and constructive mathematics. Reversed mathematics, proposed by Harvey Friedman, aims to classify the strength of mathematical theorems by identifying the required axioms. In this framework, we focus on two classical results relative to well quasi-orders: Kruskal’s theorem and Higman’s lemma. Concerning the former, we compute the proof-theoretic ordinals of two different versions establishing their non equivalence. Regarding the latter, we study, over the base theory RCA0, the relations between Higman’s original achievements and some versions of Kruskal’s theorem. For what concerns constructive mathematics, which goes back to Brouwer’s reflections and rejects the law of excluded middle in favour of more perspicuous reasoning principles, we scrutinize the main definitions of well quasi-order establishing their constructive nature; moreover, a new constructive proof of Higman’s lemma is proposed paving the way for a systematic analysis of well quasi-orders within constructive means. On top of all this we consider a peculiar phenomenon in proof theory, namely phase transitions in provability. Building upon previous results about provability in Peano Arithmetic, we locate the threshold separating provability and unprovability for statements regarding Goodstein sequences, Hydra games and Ackermannian functions. / In questa tesi studiamo il concetto di well quasi-order, originariamente sviluppato nella teoria degli ordini ma oggi trasversale a molti ambiti, nel contesto generale della teoria della dimostrazione - più precisamente, in reverse mathematics e matematica costruttiva. La reverse mathematics, proposta da Harvey Friedman, mira a classificare la forza dei teoremi matematici individuando gli assiomi richiesti. In questo contesto, ci concentriamo su due risultati classici relativi ai well quasiorder: il teorema di Kruskal e il lemma di Higman. Per quanto riguarda il primo, abbiamo calcolato gli ordinali proof-teoretici di due diverse versioni stabilendone la non equivalenza. Per quanto riguarda il secondo, studiamo, sopra la teoria di base RCA0, le relazioni tra i risultati originali di Higman e alcuni versioni del teorema di Kruskal. Per quanto riguarda la matematica costruttiva, che si rifà alle riflessioni di Brouwer e rifiuta la legge del terzo escluso a favore di principidi ragionamento più perspicui, esaminiamo attentamente le principali definizioni di well quasi-order stabilendone la natura costruttiva; inoltre, viene proposta una nuova dimostrazione costruttiva del lemma di Higman aprendo la strada per una sistematica analisi dei well quasi-order all’interno di metodi costruttivi. Oltre a questo consideriamo un fenomeno peculiare nella teoria della dimostrazione, vale a dire le transizioni di fase nella dimostrabilità. Basandoci su risultati precedenti sulla dimostrabilità nell’aritmetica di Peano, abbiamo individuato la soglia che separa dimostrabilità e indimostrabilità per enunciati riguardanti sequenze di Goodstein, Hydra games e funzioni ackermanniane.

Submitted by Cássia Santos (cassia.bcufg@gmail.com) on 2014-09-18T15:33:16Z No. of bitstreams: 2 Dissertacao Yerko Contreras Rojas.pdf: 673331 bytes, checksum: 5359343f8c3a32e21369c3bc57917634 (MD5) license_rdf: 23148 bytes, checksum: 9da0b6dfac957114c6a7714714b86306 (MD5) / Approved for entry into archive by Luciana Ferreira (lucgeral@gmail.com) on 2014-09-18T15:43:59Z (GMT) No. of bitstreams: 2 Dissertacao Yerko Contreras Rojas.pdf: 673331 bytes, checksum: 5359343f8c3a32e21369c3bc57917634 (MD5) license_rdf: 23148 bytes, checksum: 9da0b6dfac957114c6a7714714b86306 (MD5) / Made available in DSpace on 2014-09-18T15:43:59Z (GMT). No. of bitstreams: 2 Dissertacao Yerko Contreras Rojas.pdf: 673331 bytes, checksum: 5359343f8c3a32e21369c3bc57917634 (MD5) license_rdf: 23148 bytes, checksum: 9da0b6dfac957114c6a7714714b86306 (MD5) Previous issue date: 2013-07-05 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior - CAPES / This document presents an approach and development of some of the results of Shumyatsky in [14, 15, 16, 17, 18], where he worked with automorphisms of order two in finite groups of odd order, mainly showing the influence that the structure of the centralizer has on that of Group. Let G be a group with odd order, and ϕ an automorphism on G, of order two, where G = [G,ϕ], and given a limitation in the order of the centralizer of ϕ regard to G, CG(ϕ), which induces a limitation in the order of derived group G′ of group G, and we also verified that G has a normal subgroup H that is ϕ-invariant, such that H′ ≤ Gϕ and its index [G : H] is bounded with the initial limitation. With the same hypothesis of the group G and with the same limitation of the order of the centralizer of the automorphism, let V a abelian p-group such that G⟨ϕ⟩ act faithful and irreductible on V, then there is a bounded constant k, limitated by a function depending only on the parameter m, where m is tha limitation in the order of CG(ϕ), and elements x1, ...xk ∈ G−ϕ such that V = ρϕx 1,...,xk(V−ϕ). / O trabalho baseia-se na apresentação e desenvolvimento de alguns resultados expostos por Shumyatsky em [14, 15, 16, 17, 18], onde trabalha com automorfismos de ordem dois em grupos de ordem ímpar, mostrando fundamentalmente a influência da estrutura do centralizador do automorfismo na estrutura do grupo. Seja G um grupo de ordem ímpar e ϕ um automorfismo de G, de ordem dois, tal que G = [G,ϕ], dada uma limitação na ordem do centralizador de ϕ em G, CG(ϕ), a mesma induz uma limitação na ordem do grupo derivado G′ do grupo G, além disso verificamos que G tem um subgrupo H normal ϕ-invariante, tal que H′ ≤ Gϕ e o índice [G : H] é limitado dependendo da limitação inicial de CG(ϕ). Nas mesmas hipóteses do grupo G e com a mesma limitação da ordem do centralizador do automorfismo, seja V um p-grupo abeliano, tal que G⟨ϕ⟩ age fiel e irredutivelmente sobre V, então existe uma constante k, limitada por uma função que depende só da limitação de CG(ϕ), e elementos x1, ...xk ∈ G−ϕ, tal que V = ρϕx 1,...,xk(V−ϕ).

Submitted by Luanna Matias (lua_matias@yahoo.com.br) on 2015-05-15T18:05:08Z No. of bitstreams: 2 Dissertação - Ricardo da Silva Santos - 2015.pdf: 789332 bytes, checksum: 923307ee147a03d1a874647f6dcf4c9e (MD5) license_rdf: 23148 bytes, checksum: 9da0b6dfac957114c6a7714714b86306 (MD5) / Approved for entry into archive by Luanna Matias (lua_matias@yahoo.com.br) on 2015-05-15T18:08:48Z (GMT) No. of bitstreams: 2 Dissertação - Ricardo da Silva Santos - 2015.pdf: 789332 bytes, checksum: 923307ee147a03d1a874647f6dcf4c9e (MD5) license_rdf: 23148 bytes, checksum: 9da0b6dfac957114c6a7714714b86306 (MD5) / Made available in DSpace on 2015-05-15T18:09:06Z (GMT). No. of bitstreams: 2 Dissertação - Ricardo da Silva Santos - 2015.pdf: 789332 bytes, checksum: 923307ee147a03d1a874647f6dcf4c9e (MD5) license_rdf: 23148 bytes, checksum: 9da0b6dfac957114c6a7714714b86306 (MD5) Previous issue date: 2015-03-27 / This work was divided into three chapters , the rst we have some basic de nitions for the study of di erential equations, and basic results as Euler's formula and Wronskian . In the second chapter, we talked about Di erential Equations of First Order Linear, and commenting on PVI, and the Theorem of Existence and Uniqueness for ODEs. In the third and main chapter, we work with resolution methods Di erential Equations. In particular, we present a unnusual in mathematics literature to solve Linear Di erential Equations, which is by Equation Characteristic. / Este trabalho foi dividido em 3 capítulos. No primeiro temos algumas de finições básicas para o estudo de Equações Diferenciais, e resultados básicos como a fórmula de Euler e Wronskiano. No segundo capítulo, falamos sobre Equações Diferenciais Lineares de Primeira Ordem, além de comentarmos sobre o que vem a ser Problema do Valor Inicial (PVI), e o Teorema da Existência e Unicidade para EDO's. No terceiro e principal capítulo, trabalhamos com métodos de resolução de uma Equação Diferencial Ordinária Com Coe ficentes Constantes. Em especial, apresenta-mos um método não tão usual na literatura Matemática pra resolver EDOs Lineares, que é através da Derivação da Equação Caraterística.

Submitted by Luciana Ferreira (lucgeral@gmail.com) on 2017-09-22T13:40:01Z No. of bitstreams: 2 Dissertação - Tulio Marcio Gentil dos Santos - 2017.pdf: 1903129 bytes, checksum: 68678e5a2933f0e40216c1e1181aa7bc (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) / Approved for entry into archive by Luciana Ferreira (lucgeral@gmail.com) on 2017-09-22T13:40:22Z (GMT) No. of bitstreams: 2 Dissertação - Tulio Marcio Gentil dos Santos - 2017.pdf: 1903129 bytes, checksum: 68678e5a2933f0e40216c1e1181aa7bc (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) / Made available in DSpace on 2017-09-22T13:40:22Z (GMT). No. of bitstreams: 2 Dissertação - Tulio Marcio Gentil dos Santos - 2017.pdf: 1903129 bytes, checksum: 68678e5a2933f0e40216c1e1181aa7bc (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Previous issue date: 2017-08-28 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior - CAPES / Let $F_d$ be the free group of rank $d$, freely generated by $\{y_1,...,y_d\}$, $\mathbb{D}F_d$ the group ring over an integral domain $\mathbb{D}$, $E_d$ subset of $F_d$ containing $\{y_1,...,y_d\}$, $p_s(x)=x^n+c_{s,n-1}x^{n-1}+...+c_{s,1}x+c_{s,0} \in \mathbb{D}[x]$ a monic polynomial and the quotient ring $$A(d,n,E_d)=\frac{\mathbb{D}F_d}{\langle p_s(s):s\in E_d \rangle_{ideal}}.$$ When $p_s(s)$ is cubic for all $s$, we construct a finite set $E_d$ such that $A(d,n,E_d)$ has finite rank over an extension of $\mathbb{D}$. In the case where all polynomials are equal to $(x-1)^3$ and $\mathbb{D}=\mathbb{Z}[\frac{1}{6}]$ we construct a finite subset $P_d$ of $F_d$ such that $A(d,3,P_d)$ has finite $\mathbb{D}$-rank and its augmentation ideal is nilponte. Furthermore $(x-1)^3$is satisfied by all elements in the image of $F_2$ in $A(2,3,P_2)$. / Sejam $F_d$ um grupo livre de posto $d$, livremente gerado por $\{y_1,...,y_d\}$, $\mathbb{D}F_d$ o anel de grupo sobre o domínio de integridade $\mathbb{D}$, $E_d$ subconjunto de $F_d$ contendo $\{y_1,...,y_d\}$, $p_s(x)=x^n+c_{s,n-1}x^{n-1}+...+c_{s,1}x+c_{s,0} \in \mathbb{D}[x]$ e o anel quociente $$A(d,n,E_d)=\frac{\mathbb{D}F_d}{\langle p_s(s):s\in E_d \rangle_{ideal}}.$$ Quando $p_s(s)$ é cúbico para todo $s$, construímos um conjunto finito $E_d$ tal que $A(d,n,E_d)$ tem posto finito sobre uma extensão de $\mathbb{D}$. No caso em que todos os polinômios são iguais a $(x-1)^3$ e $\mathbb{D}=\mathbb{Z}[\frac{1}{6}]$, construímos um subconjunto finito $P_d$ de $F_d$ tal que $A(d,3,P_d)$ tem $\mathbb{D}$-posto finito e seu ideal de aumento é nilpotente. Além disso $(x-1)^3$ é satisfeita por todos elementos na imagem de $F_2$ em $A(2,3,P_2)$.

Embedded systems are formed by hardware and software components that interact with the physical environment and thus may be modeled as Hybrid Systems. Due to the complexity the system,there is an increasing need of automatic techniques to support the design phase, ensuring that a system behaves as expected in all the possible operating conditions.In this thesis, we propose novel techniques for the verification and the validation of hybrid systems using Satisfiability Modulo Theories (SMT). SMT is an established technique that has been used successfully in many verification approaches, targeted for both hardware and software systems. The use of SMT to verify hybrid systems has been limited, due to the restricted support of complex continuous dynamics and the lack of scalability. The contribution of the thesis is twofold. First, we propose novel encoding techniques, which widen the applicability and improve the effectiveness of the SMT-based approaches. Second, we propose novel SMT-based algorithms that improve the performance of the existing state of the art approaches. In particular we show algorithms to solve problems such as invariant verification, scenario verification and parameter synthesis. The algorithms fully exploit the underlying structure of a network of hybrid systems and the functionalities of modern SMT-solvers. We show and discuss the effectiveness of the the proposed techniques when applied to benchmarks from the hybrid systems domain.

The main purpose of this thesis is to combine the categorical approach to logic given by the study of doctrines, with the universal algebraic techniques given by the theory of the pseudo-monads and pseudo-distributive laws. Every completions of doctrines is then formalized by a pseudo-monad, and then combinations of these are studied by the analysis of the pseudo-distributive laws. The starting point are the works of Maietti and Rosolini, in which they describe three completions for elementary doctrines: the first which adds full comprehensions, the second comprehensive diagonals, and the third quotients. Then we determine the existential completion of a primary doctrine, and we prove that the 2-monad obtained from it is lax-idempotent, and that the 2-category of existential doctrines is isomorphic to the 2-category of algebras for this 2-monad. We also show that the existential completion of an elementary doctrine is again elementary and we extend the notion of exact completion of an elementary existential doctrine to an arbitrary elementary doctrine. Finally we present the elementary completion for a primary doctrine whose base category has finite limits. In particular we prove that, using a general results about unification for first order languages, we can easily add finite limits to a syntactic category, and then apply the elementary completion for syntactic doctrines. We conclude with a complete description of elementary completion for primary doctrine whose base category is the free product completion of a discrete category, and we show that the 2-monad constructed from the 2-adjunction is lax-idempotent.

Autonomous systems must be able to detect and promptly react to faults. Fault Detection and Identification components (FDI) are in charge of detecting the occurrence of faults. The FDI depends on the concrete design of the system, needs to take into account how faults might interact, and can only have a partial view of the run-time state through sensors. For these reasons, the development of the FDI and certification of its correctness and quality are difficult tasks. This difficulty is compounded by the fact that current approaches for verification of the FDI rely on manual inspection and testing. Motivated by industrial case-studies from the European Space Agency, this thesis proposes a formal foundation for FDI design that covers specification, validation, verification, and synthesis. The Alarm Specification Language (ASLk) is introduced in order to formally capture a set of interesting and desirable properties of the FDI components. ASLk is equipped with a semantics based on Temporal Epistemic Logic, thus enabling reasoning about partially observable systems. Automated reasoning techniques can then be applied to perform validation, verification, and synthesis of the FDI. This formal process guarantees that the generated FDI satisfies the designer expectations. The problems deriving from this process were out of reach for existing model-checking techniques. Therefore, we develop novel and efficient techniques for model-checking temporal epistemic logic over infinite state systems.