The thesis formulates and proves a witnessing theorem for SPV -provable formulas in the form ∀x∃yA(x, y) where A corresponds to a polynomial time decidable relation. By SPV we understand an extension of the theory TPV (the universal theory of N in the language representing polynomial algorithms) by additional axioms ensuring the existence of a minimum of a linear ordering defined by a polynomial time decidable relation on an initial segment. As these additional axioms are not universal sentences, the theory SPV requires nontrivial use of witnessing Herbrand's and KPT theorems which have direct application only for universal theories. Based on the proven witnessing theorem, we derive a NP search problem characterizing complexity of finding y for a given x such that A(x, y). A part of the thesis is dedicated to arguments supporting the conjecture that SPV is strictly stronger than TPV . 1

The federal communications commission (FCC) has predicted that, under the current regulatory environment, a spectrum shortage may be faced in the near future. This impending spectrum shortage is in part due to a rapidly increasing demand for wireless services and in part due to inefficient usage of currently licensed bands. A new paradigm pertaining to wireless spectrum allocation, known as cognitive radio (CR), has been proposed as a potential solution to this problem. This dissertation seeks to contribute to research in the field of CR through an investigation into the effect that a primary user (PU) channel occupancy model will have on the performance of a secondary user (SU) in a CR network. The model assumes that PU channel occupancy can be described as a binary process and a two state Hidden Markov Model (HMM) was thus chosen for this investigation. Traditional algorithms for training the model were compared with certain evolutionary-based training algorithms in terms of their resulting prediction accuracy and computational complexity. The performance of this model is important since it provides SUs with a basis for channel switching and future channel allocations. A CR simulation platform was developed and the results gained illustrated the effect that the model had on channel switching and the subsequently achievable performance of a SU operating within a CR network. Performance with regard to achievable SU data throughput, PU disruption rate and SU power consumption, were examined for both theoretical test data as well as data obtained from real world spectrum measurements (taken in Pretoria, South Africa). The results show that a trade-off exists between the achievable SU throughput and the average PU disruption rate. Significant SU performance improvements were observed when prediction modelling was employed and it was found that the performance and complexity of the model were influenced by the algorithm employed to train it. SU performance was also affected by the length of the quick sensing interval employed. Results obtained from measured occupancy data were comparable with those obtained from theoretical occupancy data with an average percentage similarity score of 96% for prediction accuracy (using the Viterbi training algorithm), 90% for SU throughput, 83% for SU power consumption and 71% for PU disruption rate. / Dissertation (MEng)--University of Pretoria, 2012. / Electrical, Electronic and Computer Engineering / unrestricted

[pt] Este trabalho é uma elaboração, com exemplos, e evolução do Algoritmo de Compressão Horizontal (HC) apresentado e seu Conjunto de Regras de Compressão. Este trabalho apresenta uma prova, feita no Provador Interativo de Teoremas Lean, de que o algoritmo HC pode obter uma Derivação Comprimida, representada por um Grafo Acíclico Dirigido, a partir de qualquer Derivação Tipo-Árvore em Dedução Natural para a Lógica Minimal Puramente Implicacional. Finalmente, a partir da Cobertura e Corretude do algoritmo HC, pode-se argumentar que NP = PSPACE. / [en] This work is an elaboration, with examples, and evolution of the presented Horizontal Compression Algorithm (HC) and its set of Compression Rules. This work argues a proof, done in the Lean Interactive Theorem Prover, that the HC algorithm can obtain a Compressed Derivation, represented by a Directed Acyclic Graph, from any Tree-Like Natural Deduction Derivation in Minimal Purely Implicational Logic. Finally, from the Coverage and Soundness of the HC algorithm, one can argue that NP = PSPACE.

Cette thèse s'intéresse à la conception et le développement des techniques de bioinfor- matique qui peuvent faciliter l'utilisation de l'approche metabarcoding pour mesurer la diversité d'espèces. Le metabarcoding peut être utilisé avec le séquencage haut débit pour l'identification d'espèces multiples à partir d'un seul échantillon environnemental. La véritable force du metabarcoding réside dans l'utilisation de barcode marqueurs choisi pour une étude particulière et l'identification d'espèces ou des taxons peut être réalisé avec des marqueurs soigneusement conçu. Avec l'avancement des techniques haut débit de séquençage, une énorme quantité des données de séquences est produit qui contient un nombres substantiel des mutations. Ces mutations posent un grand problème pour les estimations correctes de la biodiversité et pour le d'assignation de taxon. Les trois problèmes majeurs dans le domaine de la bioinformatique que j'ai abordés dans cette thèse sont: i) évaluer la qualité d'une barcode marker , ii) concevoir des nouveaux région barcode et iii) d'analyser les données de séquençage pour traiter les erreurs et éliminer le bruit en séquences. Pour évaluer la qualité d'un barcode marker, on a développé deux mesures quantita- tive,formelle: la couverture (Bc) et la spécificité (Bs). La couverture donne une mesure de universalité d'une pairs de primer pour amplifier un large nombre de taxa, alors que la spécificité donne une mesure de capacité à discriminer entre les différents taxons. Ces mesures sont très utiles pour le classement des barcode marker et pour sélectionner les meilleurs markers. Pour trouver des nouveaux région barcode notamment pour les applications metabarcod- ing, j'ai développé un logiciel, ecoPrimers3. Basé sur ces deux mesures de qualité et de l'information taxinomique intégré, ecoPrimers nous permet de concevoir barcode markers pour n'importe quel niveau taxonomique . En plus, avec un grand nombre de paramètres réglables il nous permet de contrôler les propriétés des amorces. Enfin, grâce a des algorithmes efficaces et programmé en langage C, ecoPrimers est suffisamment efficace pour traiter des grosses bases de données, y compris génomes bactériens entièrement séquencés. Enfin pour traiter des erreurs présentes dans les données de séquencage , nous avons analysé un ensemble simple d'échantillons de PCR obtenus à partir de l'analyse du régime alimentaire de Snow Leopard. En mesurant les corrélations entre les différents paramètres des erreurs, nous avons observé que la plupart des erreurs sont produites pendant l'amplification par PCR. Pour détecter ces erreurs, nous avons développé un algorithme utilisant les graphes, qui peuvent différencier les vrai séquences des erreurs induites par PCR. Les résultats obtenus à partir de cet algorithme a montré que les données de-bruitée a donnent une estimation réaliste de la diversité des espèces étudiées dans les Alpes françaises. / This thesis is concerned with the design and development of bioinformatics techniques that can facilitate the use of metabarcoding approach for measuring species diversity. Metabarcoding coupled with next generation sequencing techniques have a strong po- tential for multiple species identification from a single environmental sample. The real strength of metabarcoding resides in the use of barcode markers chosen for a particular study. The identification at species or higher level taxa can be achieved with carefully designed barcode markers. Moreover with the advent of high throughput sequencing techniques huge amount of sequence data is being produced that contains a substantial level of mutations. These mutations pose a problem for the correct estimates of biodi- versity and for the taxon assignation process. Thus the three major challenges that we addressed in this thesis are: evaluating the quality of a barcode region, designing new barcodes and dealing with errors occurring during different steps of an experiment. To assess the quality of a barcode region we have developed two formal quantitative mea- sures called barcode coverage (Bc) and barcode specificity (Bs). Barcode coverage is concerned with the property of a barcode to amplify a broad range of taxa, whereas barcode specificity deals with its ability to discriminate between different taxa. These measures are extremely useful especially for ranking different barcodes and selecting the best markers. To deal with the challenge of designing new barcodes for metabarcoding applications we have developed an efficient software called ecoPrimers. Based on the above two quality measures and with integrated taxonomic information, ecoPrimers1 enables us to design primers and their corresponding barcode markers for any taxonomic level. Moreover with a large number of tunable parameters it allows us to control the properties of primers. Finally, based on efficient algorithms and implemented in C language, ecoPrimers is efficient enough to deal with large data bases including fully sequenced bacterial genomes. Finally to deal with errors present in DNA sequence data, we have analyzed a simple set of PCR samples obtained from the diet analysis of snow leopard. We grouped closely related sequences and by measuring the correlation between different parameters of mutations, we have shown that most of the errors were introduced during PCR amplification. In order to deal with such errors, we have further developed an algorithm using graphs approach, that can differentiate true sequences from PCR induced errors. The results obtained from this algorithm showed that de-noised data gave a realistic estimate of species diversity studied in French Alpes. This algorithm is implemented in program obiclean.

The diploma thesis deals with the use of a simulation model for the development of an automatic algorithm for the creation of a routing table and route evaluation in a transport system. It includes a search of modeling and simulation issues and state-space search issues with an analysis of available search methods. The simulation model of the transport system is created in the software Tecnomatix Plant Simulation, where an algorithm for automatic creation of routing tables for routing and evaluation of routes according to static criteria is subsequently developed and tested. The work presents a proposal for the principle of the algorithm for evaluating the routes of the transport system, including dynamic criteria and their optimization.