Whereas early researchers in computability theory described effective computability in terms of such models as Turing machines, Markov algorithms, and register machines, a recent trend has been to use simple programming languages as computability models. A parallel development to this programming approach to computability theory is the current interest in systematic and scientific development and proof of programs. This paper investigates the feasibility of using formal proofs of programs in computability theory. After describing a framework for formal verification of programs written in a simple theoretical programming language, we discuss the proofs of several typical programs used in computability theory.

The method of Pseudo-Linear Identification (PLID) is presented as an explicitly linear approach to the joint state and parameter estimation problem. The convergence properties of the algorithm in the stochastic case are investigated through simulation and comparisons with popular methods are made. The method is then extended to allow the tracking of time-varying system parameters. An adaptive control structure based upon this Tracking–PLID algorithm is proposed which utilizes pole–placement state variable feedback via Ackermann's formula. The capabilities of this adaptive control scheme are demonstrated by application to a full-order nonlinear aircraft simulation model where significant improvement is shown over fixed-gain controllers in the face of rapid plant changes. / Master of Science

Submitted by Maike Costa (maiksebas@gmail.com) on 2016-08-10T14:17:41Z No. of bitstreams: 1 arquivo total.pdf: 975005 bytes, checksum: 6f8194b9c0cb9c0bbd07b1d2b0ba4b9e (MD5) / Made available in DSpace on 2016-08-10T14:17:41Z (GMT). No. of bitstreams: 1 arquivo total.pdf: 975005 bytes, checksum: 6f8194b9c0cb9c0bbd07b1d2b0ba4b9e (MD5) Previous issue date: 2016-06-21 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior - CAPES / The class of primitive recursive functions is not a formal version to the class of algorithmic functions, we study this special class of numerical functions due to the fact of that many of the functions known as algorithmic are primitive recursive. The approach on the class of primitive recursive functions aims to explore this special class of functions and from that, present solutions for the following problems: (1) given the class of primitive recursive derivations, is there an algorithm, that is, a mechanical procedure for recognizing primitive recursive derivations? (2) Is there a universal function for the class of primitive recursive functions? If so, is this function primitive recursive? (3) Are all the algorithmic functions primitive recursive? To provide solutions to these issues, we base on the hypothetical-deductive method and argue based on the works of Davis (1982), Mendelson (2009), Dias e Weber (2010), Rogers (1987), Soare (1987), Cooper (2004), among others. We present the theory of Turing machines which is a formal version to the intuitive notion of algorithm, and after that the famous Church-Turing tesis which identifies the class of algorithmic functions with the class of Turing-computable functions. We display the class of primitive recursive functions and show that it is a subclass of Turing-computable functions. Having explored the class of primitive recursive functions we proved as results that there is a recognizer algorithm to the class of primitive recursive derivations; that there is a universal function to the class of primitive recursive functions which does not belong to this class; and that not every algorithmic function is primitive recursive. / A classe das funções recursivas primitivas não constitui uma versão formal para a classe das funções algorítmicas, estudamos esta classe especial de funções numéricas devido ao fato de que muitas das funções conhecidas como algorítmicas são recursivas primitivas. A abordagem acerca da classe das funções recursivas primitivas tem como objetivo explorar esta classe especial de funções e, a partir disto, apresentar soluções para os seguintes problemas: (1) dada a classe das derivações recursivas primitivas, há um algoritmo, ou seja, um procedimento mecânico, para reconhecer derivações recursivas primitivas? (2) Existe uma função universal para a classe das funções recursivas primitivas? Se sim, essa função é recursiva primitiva? (3) Toda função algorítmica é recursiva primitiva? Para apresentar soluções para estas questões, nos pautamos no método hipotético-dedutivo e argumentamos com base nos manuais de Davis (1982), Mendelson (2009), Dias e Weber (2010), Rogers (1987), Soare (1987), Cooper (2004), entre outros. Apresentamos a teoria das máquinas de Turing, que constitui uma versão formal para a noção intuitiva de algoritmo, e, em seguida, a famosa tese de Church-Turing, a qual identifica a classe das funções algorítmicas com a classe das funções Turing-computáveis. Exibimos a classe das funções recursivas primitivas, e mostramos que a mesma constitui uma subclasse das funções Turing-computáveis. Tendo explorado a classe das funções recursivas primitivas, como resultados, provamos que existe um algoritmo reconhecedor para a classe das derivações recursivas primitivas; que existe uma função universal para a classe das funções recursivas primitivas a qual não pertence a esta classe; e que nem toda função algorítmica é recursiva primitiva.

Submitted by Maike Costa (maiksebas@gmail.com) on 2017-09-20T12:52:54Z No. of bitstreams: 1 arquivototal.pdf: 1155001 bytes, checksum: c813651173e6bf037a98328b32bc7d5a (MD5) / Made available in DSpace on 2017-09-20T12:52:54Z (GMT). No. of bitstreams: 1 arquivototal.pdf: 1155001 bytes, checksum: c813651173e6bf037a98328b32bc7d5a (MD5) Previous issue date: 2016-10-24 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior - CAPES / In the thirties of the last century, several formal versions for the intuitive notion of algorithmic function were offered. Among them, the version of the recursive functions and the version of the Turing-computable functions. Posteriorly, such versions were extended in order to also include the partial algorithmic functions, giving rise, in this way, to the version of the partial recursive functions and to the version of the partially Turing-computable functions. In this context, this research, located into Computability Theory domain and built in the light of theoretical assumptions of Davis (1982), Mendelson (2009), Dias & Weber (2010), Rogers (1987), Soare (1987), Cooper (2004), among others, is intended to rebuild the proof that the given formal versions referred to the intuitive notion of partial algorithmic function, despite being conceptually distinct, they are extensionally equivalents in the sense that they determine the same set of theoretical-numerical functions. As a part of this rebuilding, we shall prove, in na unprecedented way, using quintuples, that every partial recursive function is partially Turing-computable. In the literature, this theorem is proved by means of a set of quadruples. However, defining a lower cardinality set constructed by quintuples, it is possible to prove it in a smaller time interval, which representes a gain from the computational point of view. Besides presenting this alternative proof, posed by the Church-Turing thesis that the set of partial recursive functions includes all the partial algorithmic functions, we shall investigate if this set itself and its infinite subsets are or are not algorithmic. In this survey, we shall demonstrate, in arithmetical terms, with the aid of Rice‟s theorem, that although the set of partial recursive functions is algorithmic, all its subsets which are different from the empty set are not, among which are the set of recursive functions and the set of primitive recursive functions. / Na década de 30 do século passado, foram oferecidas várias versões formais para a noção intuitiva de função algorítmica. Dentre elas, a versão das funções recursivas e a versão das funções Turing-computáveis. Posteriormente, tais versões foram estendidas a fim de abranger também as funções parciais algorítmicas, dando origem, deste modo, à versão das funções parciais recursivas e à versão das funções parcialmente Turing-computáveis. Nesse contexto, esta pesquisa, situada dentro do domínio da Teoria da Computabilidade e construída à luz dos pressupostos teóricos de Davis (1982), Mendelson (2009), Dias e Weber (2010), Rogers (1987), Soare (1987), Cooper (2004), entre outros, destina-se a reconstruir a prova de que as referidas versões formais dadas para a noção intuitiva de função parcial algorítmica, apesar de conceitualmente distintas, são extensionalmente equivalentes no sentido de que elas determinam o mesmo conjunto de funções numéricas. Como parte desta reconstrução, provaremos, de modo inédito, mediante o uso de quíntuplas, que toda função parcial recursiva é parcialmente Turing-computável. Na literatura especializada, esse teorema é provado por meio de um conjunto de quádruplas. Porém, definindo um conjunto de menor cardinalidade constituído por quíntuplas, é possível prová-lo em um intervalo menor de tempo, o que representa um ganho do ponto de vista computacional. Além de apresentar essa prova alternativa, posto pela Tese de Church-Turing que o conjunto das funções parciais recursivas contém todas as funções parciais algorítmicas, investigaremos se ele próprio e os seus infinitos subconjuntos são ou não algorítmicos. Nesta investigação, demonstraremos, em termos aritméticos, com o auxílio do Teorema de Rice, que embora o conjunto das funções parciais recursivas seja algorítmico, todos os seus subconjuntos diferentes do conjunto vazio não o são, dentre os quais estão o conjunto das funções recursivas e o conjunto das funções recursivas primitivas.

In this work we present a proof that the Hilbert s Tenth Problem is unsolvable. This problem is to give a computing algorithm which will tell of a given polynomial Diophantine equation with integer coefficients whether or not it has a solution in integers. We start developing some topics of basic number theory, that will be useful at some time. In this part we prove only main results. After that, we study Diophantine equation as well as Diophantine functions. Then, we prove a serie of lemas that will be useful to proof that the exponential function is Diophantine. From there, we define the concept of recursive function and prove that a function is Diophantine if and only if it is recursive. Finally we prove the Universality Theorem. We use this last theorem to proof that the Hilbert s Problem is unsolvable. / Neste trabalho apresentamos uma demonstração da insolubilidade do Décimo Problema de Hilbert, que investiga a existência de um método para determinar se dada uma equação Diofantina qualquer podemos determinar se esta tem ou não uma solução. Começamos desenvolvendo alguns tópicos de teoria de números, que serão úteis em vários momentos, nesta parte demonstramos apenas os resultados principais. Em um segundo momento, passamos ao estudo das equações Diofantinas bem como das funções Diofantinas, que permeiam nossos resultados. Em seguida, demonstramos uma série de lemas que servem de base para mostrarmos que a função exponencial é Diofantina. A partir daı, passamos a definição do importante conceito de função recursiva e então demonstramos que uma função ser recursiva é equivalente a ser Diofantina. Finalmente, demonstramos o Teorema da Universalidade que servirá de base para a demonstração o da insolubilidade do Décimo Problema de Hilbert. / Mestre em Matemática

Indiana University-Purdue University Indianapolis (IUPUI) / Lithium ion (Li-ion) batteries have become integral parts of our lives; they are widely used in applications like handheld consumer products, automotive systems, and power tools among others. To extract maximum output from a Li-ion battery under optimal conditions it is imperative to have access to the state of the battery under every operating condition. Faults occurring in the battery when left unchecked can lead to irreversible, and under extreme conditions, catastrophic damage. In this thesis, an adaptive fault diagnosis technique is developed for Li-ion batteries. For the purpose of fault diagnosis the battery is modeled by using lumped electrical elements under the equivalent circuit paradigm. The model takes into account much of the electro-chemical phenomenon while keeping the computational effort at the minimum. The diagnosis process consists of multiple models representing the various conditions of the battery. A bank of observers is used to estimate the output of each model; the estimated output is compared with the measurement for generating residual signals. These residuals are then used in the multiple model adaptive estimation (MMAE) technique for generating probabilities and for detecting the signature faults. The effectiveness of the fault detection and identification process is also dependent on the model uncertainties caused by the battery modeling process. The diagnosis performance is compared for both the linear and nonlinear battery models. The non-linear battery model better captures the actual system dynamics and results in considerable improvement and hence robust battery fault diagnosis in real time. Furthermore, it is shown that the non-linear battery model enables precise battery condition monitoring in different degrees of over-discharge.