Cette thèse s'intéresse à la démonstration automatique de la validité de formules mathématiques issues de la preuve de programmes. Elle se focalise tout particulièrement sur la Satisfiabilité Modulo Théories (SMT): un jeune domaine de recherche qui a connu de grands progrès durant la dernière décennie. Les démonstrateurs de cette famille ont des applications diverses dans la conception de microprocesseurs, la preuve de programmes, le model-checking, etc.Les démonstrateurs SMT offrent un bon compromis entre l'expressivité et l'efficacité. Ils reposent sur une coopération étroite d'un solveur SAT avec une combinaison de procédures de décision pour des théories spécifiques comme la théorie de l'égalité libre avec des symboles non interprétés, l'arithmétique linéaire sur les entiers et les rationnels, et la théorie des tableaux.L'objectif de cette thèse est d'améliorer l'efficacité et l'expressivité du démonstrateur SMT Alt-Ergo. Pour cela, nous proposons une nouvelle procédure de décision pour la théorie de l'arithmétique linéaire sur les entiers. Cette procédure est inspirée par la méthode de Fourier-Motzkin, mais elle utilise un simplexe sur les rationnels pour effectuer les calculs en pratique. Nous proposons également un nouveau mécanisme de combinaison, capable de raisonner dans l'union de la théorie de l'égalité libre, la théorie AC des symboles associatifs et commutatifs et une théorie arbitraire deShostak. Ce mécanisme est une extension modulaire et non intrusive de la procédure de completion close modulo AC avec la théorie de Shostak. Aussi, nous avons étendu Alt-Ergo avec des procédures de décision existantes pour y intégrer d'autres théories intéressantes comme la théorie de types de données énumérés et la théorie des tableaux. Enfin, nous avons exploré des techniques de simplification de formules en amont et l'amélioration de son solveur SAT. / This thesis tackles the problem of automatically proving the validity of mathematical formulas generated by program verification tools. In particular, it focuses on Satisfiability Modulo Theories (SMT): a young research topic that has seen great advances during the last decade. The solvers of this family have various applications in hardware design, program verification, model checking, etc.SMT solvers offer a good compromise between expressiveness and efficiency. They rely on a tight cooperation between a SAT solver and a combination of decision procedures for specific theories, such as the free theory of equality with uninterpreted symbols, linear arithmetic over integers and rationals, or the theory of arrays.This thesis aims at improving the efficiency and the expressiveness of the Alt-Ergo SMT solver. For that, we designed a new decision procedure for the theory of linear integer arithmetic. This procedure is inspired by Fourier-Motzkin's method, but it uses a rational simplex to perform computations in practice. We have also designed a new combination framework, capable of reasoning in the union of the free theory of equality, the AC theory of associative and commutativesymbols, and an arbitrary signature-disjoint Shostak theory. This framework is a modular and non-intrusive extension of the ground AC completion procedure with the given Shostak theory. In addition, we have extended Alt-Ergo with existing decision procedures to integrate additional interesting theories, such as the theory of enumerated data types and the theory of arrays. Finally, we have explored preprocessing techniques for formulas simplification as well as the enhancement of Alt-Ergo's SAT solver.

This thesis deals with smooth discretization schemes and inverse problems, the former used in efficient yet accurate numerical solutions to forward models required in turn to solve inverse problems. The aims of the thesis include, (i) development of a stabilization techniques for a class of forward problems plagued by unphysical oscillations in the response due to the presence of jumps/shocks/high gradients, (ii) development of a smooth hybrid discretization scheme that combines certain useful features of Finite Element (FE) and Mesh-Free (MF) methods and alleviates certain destabilizing factors encountered in the construction of shape functions using the polynomial reproduction method and, (iii) a first of its kind attempt at the joint inversion of both static and dynamic source parameters of the 2004 Sumatra-Andaman earthquake using tsunami sea level anomaly data. Following the introduction in Chapter 1 that motivates and puts in perspective the work done in later chapters, the main body of the thesis may be viewed as having two parts, viz., the first part constituting the development and use of smooth discretization schemes in the possible presence of destabilizing factors (Chapters 2 and 3) and the second part involving solution to the inverse problem of tsunami source recovery (Chapter 4). In the context of stability requirements in numerical solutions of practical forward problems, Chapter 2 develops a new stabilization scheme. It is based on a stochastic representation of the discretized field variables, with a view to reduce or even eliminate unphysical oscillations in the MF numerical simulations of systems developing shocks or exhibiting localized bands of extreme plastic deformation in the response. The origin of the stabilization scheme may be traced to nonlinear stochastic filtering and, consistent with a class of such filters, gain-based additive correction terms are applied to the simulated solution of the system, herein achieved through the Element-Free Galerkin (EFG) method, in order to impose a set of constraints that help arresting the spurious oscillations. The method is numerically illustrated through its application to a gradient plasticity model whose response is often characterized by a developing shear band as the external load is gradually increased. The potential of the method in stabilized yet accurate numerical simulations of such systems involving extreme gradient variations in the response is thus brought forth. Chapter 3 develops the MF-based discretization motif by balancing this with the widespread adoption of the FE method. Thus it concentrates on developing a 'hybrid' scheme that aims at the amelioration of certain destabilizing algorithmic issues arising from the necessary condition of moment matrix invertibility en route to the generation of smooth shape functions. It sets forth the hybrid discretization scheme utilizing bivariate simplex splines as kernels in a polynomial reproducing approach adopted over a conventional FE-like domain discretization based on Delaunay triangulation. Careful construction of the simplex spline knotset ensures the success of the polynomial reproduction procedure at all points in the domain of interest, a significant advancement over its precursor, the DMS-FEM. The shape functions in the proposed method inherit the global continuity ( C p 1 ) and local supports of the simplex splines of degree p . In the proposed scheme, the triangles comprising the domain discretization also serve as background cells for numerical integration which here are near-aligned to the supports of the shape functions (and their intersections), thus considerably ameliorating an oft-cited source of inaccuracy in the numerical integration of MF-based weak forms. Numerical experiments establish that the proposed method can work with lower order quadrature rules for accurate evaluation of integrals in the Galerkin weak form, a feature desiderated in solving nonlinear inverse problems that demand cost-effective solvers for the forward models. Numerical demonstrations of optimal convergence rates for a few test cases are given and the hybrid method is also implemented to compute crack-tip fields in a gradient-enhanced elasticity model. Chapter 4 attempts at the joint inversion of earthquake source parameters for the 2004 Sumatra-Andaman event from the tsunami sea level anomaly signals available from satellite altimetry. Usual inversion for earthquake source parameters incorporates subjective elements, e.g. a priori constraints, posing and parameterization, trial-and-error waveform fitting etc. Noisy and possibly insufficient data leads to stability and non-uniqueness issues in common deterministic inversions. A rational accounting of both issues favours a stochastic framework which is employed here, leading naturally to a quantification of the commonly overlooked aspects of uncertainty in the solution. Confluence of some features endows the satellite altimetry for the 2004 Sumatra-Andaman tsunami event with unprecedented value for the inversion of source parameters for the entire rupture duration. A nonlinear joint inversion of the slips, rupture velocities and rise times with minimal a priori constraints is undertaken. Large and hitherto unreported variances in the parameters despite a persistently good waveform fit suggest large propagation of uncertainties and hence the pressing need for better physical models to account for the defect dynamics and massive sediment piles. Chapter 5 concludes the work with pertinent comments on the results obtained and suggestions for future exploration of some of the schemes developed here.

A couple of discretization schemes, based on an FE-like tessellation of the domain and polynomial reproducing, globally smooth shape functions, are considered and numerically explored to a limited extent. The first one among these is an existing scheme, the smooth DMS-FEM, that employs Delaunay triangulation or tetrahedralization (as approximate) towards discretizing the domain geometry employs triangular (tetrahedral) B-splines as kernel functions en route to the construction of polynomial reproducing functional approximations. In order to verify the numerical accuracy of the smooth DMS-FEM vis-à-vis the conventional FEM, a Mindlin-Reissner plate bending problem is numerically solved. Thanks to the higher order continuity in the functional approximant and the consequent removal of the jump terms in the weak form across inter-triangular boundaries, the numerical accuracy via the DMS-FEM approximation is observed to be higher than that corresponding to the conventional FEM. This advantage notwithstanding, evaluations of DMS-FEM based shape functions encounter singularity issues on the triangle vertices as well as over the element edges. This shortcoming is presently overcome through a new proposal that replaces the triangular B-splines by simplex splines, constructed over polygonal domains, as the kernel functions in the polynomial reproduction scheme. Following a detailed presentation of the issues related to its computational implementation, the new method is numerically explored with the results attesting to a higher attainable numerical accuracy in comparison with the DMS-FEM.

Abstract Glucocorticoids are the most important and widely used treatment modality in dermatology. A large variety of topical as well as systemic preparations is available. Most patients treated with glucocorticoids respond quickly to the treatment, but some are considered insensitive or even resistant to glucocorticoid therapy. Currently, there is no known measurable variable, through which the response can be predicted. Glucocorticoids mediate their actions through glucocorticoid receptors (GR). Several isoforms of GR exist, but the α (GRα) and β (GRβ) isoforms are clinically the most important. Based on previous studies, it has been proposed that the abundance of GR isoforms or the GRβ: GRα –ratio could affect individual responsiveness to corticosteroid treatment. In particular, up-regulation of GRβ expression has been shown to be linked to resistance to corticosteroid treatment. This thesis comprises three sub-studies. Firstly, we wanted to determine whether GRα and GRβ are expressed in inflammatory skin diseases. Secondly, we examined if the expression is altered by corticosteroid treatment in eczema atopicum, bullous pemphigoid and psoriasis. Finally, we measured the effects of a topical vitamin D3 analogue (calcipotriol) combined with betamethasone compared with betamethasone monotherapy on inflammatory biomarkers of psoriasis. Our studies provide detailed novel data about the expression of GRα and GRβ. GRα and GRβ were shown to be expressed in the blood lymphocytes and lesional skin of patients with eczema atopicum, bullous pemphigoid and psoriasis, as well as in the skin of patients with eczema nummulare, lichen simplex chronicus and lichen ruber planus. Systemic corticosteroid treatment was shown to affect the expression of GRα and GRβ in eczema atopicum and bullous pemphigoid, but the inconsistent variation in their expression between patients prevented us from drawing firm conclusions. Neither GRα nor GRβ as a single marker were found to be a suitable predictor of corticosteroid responsiveness. Clinical and laboratory analyses showed that topical treatment of psoriasis with calcipotriol/betamethasone combination ointment is more beneficial measured by both than betamethasone monotherapy. / Tiivistelmä Glukokortikoideja (”kortisoni”) käytetään tulehduksellisten ihotautien hoidossa paikallisesti tai systeemisenä lääkkeenä. Suurin osa potilaista reagoi hoitoon nopeasti, mutta osalla hoitovaste on heikompi tai ilmenee hitaasti. Tällä hetkellä ei tunneta keinoja ennustaa luotettavasti kortisonihoidon vastetta. Glukokortikoidit vaikuttavat elimistössä glukokortikoidireseptorien (GR) kautta. Glukokortikoidireseptorista tunnetaan useita alatyyppejä, joista tärkeimmät ovat α (GRα) ja β (GRβ). Aiemman tiedon pohjalta on pidetty mahdollisena, että GR-alatyyppien suhteella tai määrällä on merkitystä kortisonivasteen syntymisessä. Erityisesti on arveltu, että ylimäärä GRβ:aa voisi estää kortisonihoidon vaikutusta. Tässä väitöskirjassa tavoitteena on ollut selvittää, tapahtuuko GR-alatyyppien ilmenemisessä muutoksia tulehduksellisia ihosairauksia sairastavilla potilailla sekä tutkia, miten kortisonihoito vaikuttaa GR-tasoihin atooppista ihottumaa, pemfigoidia ja psoriaasia sairastavilla potilailla. Lisäksi olemme verranneet paikallishoitoa pelkällä kortisonivoiteella D-vitamiinijohdos kalsipotriolin ja kortisonin yhdistelmähoitoon psoriaatikoilla. Tutkimus on antanut uutta yksityiskohtaista tietoa GRα:n ja GRβ:n esiintymisestä ihossa ja tulehdussoluissa ihosairauksia sairastavilla potilailla. Tutkimustulosten perusteella voidaan todeta, että GRα ja GRβ esiintyvät atooppista ihottumaa, pemfigoidia ja psoriaasia sairastavien potilaiden ihossa ja veren tulehdussoluissa sekä nummulaari-ihottumaa, neurodermatiittia ja punajäkälää sairastavien potilaiden ihossa. Suun kautta annettu kortisonihoito vaikuttaa GRα- ja GRβ–lähetti-RNA:n ilmenemiseen, mutta potilaskohtaiset erot ovat suuret, eikä kumpikaan, GRα tai GRβ, sovellu yksinään ennustamaan kortisonihoidon vastetta. Paikallisella kortisonihoidolla D-vitamiinijohdos kalsipotrioliin yhdistettynä on suotuisampi vaikutus psoriaasin tulehduksellisiin välittäjäaineisiin ja tulehdussoluihin kuin pelkällä paikallisella kortisonihoidolla.

No description available.

This work is about position prediction in network, it is focused to find Landmark closest to the Host in the network (with lowest distance vector). The algorithm is based on GNP system. In terms of GNP system simulation was selected method for mathematical part of position prediction. The method was Simplex Downhill. The designed algorithm was implemented in Java. In the first step chose Host continent by meassuring the distance vector. In next step is selected nearest part in the continent. In conclusion estimate Host its position and then closest Landmark. Results from this work is important for designing TTP protocol. The verdict is that the GNP can be used for TTP, but Landmarks must be located in uniform density.

Department of Microbiology / PhD (Microbiology) / Human herpes virus type 8 (HHV-8), also known as Kaposi’s sarcoma associated herpes virus (KSHV), is the etiologic agent of Kaposi’s sarcoma (KS), and AIDS related Kaposi’s sarcoma (AIDS-KS). HHV-8 which is a member of the Herpesviridae family, exhibits extensive genetic diversity globally. In endemic regions, infection with HHV-8 occurs very early on in life, which is an indication of both environmental and vertical routes of transmission. The advent of HIV leads to the classification of an AIDS-KS defining condition in HIV infections. This suggests that in regions where HIV and HHV-8 are endemic, KS may become common in a mature HIV epidemic. Just like the prevalence of HIV in Northern South Africa is generally high as in most regions of the country, as the HIV epidemic matures in South Africa, it is important to understand the burden and distribution of HHV-8 infection, and the likely genotypes infecting the population. The main objective of the thesis was to establish the epidemiology and infecting genotypes of HHV-8 in Northern South Africa (Limpopo Province), where no data exists. First, a systematic review of the literature was carried out for the entire African continent to determine the seroprevalence and genotype distribution of HHV-8 in all African countries (n=53). In this review, Sudan and South Sudan were considered as one country. Articles were searched using the PRISMA guideline and exported using an article grid. More than two-thirds (64%) of the studies reported on seroprevalence, 29.3% on genotypes; and 9.5% were on both seroprevalence and genotypes. About 45% (24/53) of the African countries had data on HHV-8 seroprevalence exclusively, and more than half (53%) had data on either seroprevalence or genotypes. Almost half (47%) of the countries had no data on HHV-8 infection. There was high heterogeneity in the types of tests and interpretation algorithms used in determining HHV-8 seropositivity across the different studies. Generally, seroprevalence ranged from 2.0% in a group of young children in Eritrea to 100% in a small group of individuals with KS in the Central Africa Republic and a larger group of KS in individuals in Morocco. Approximately, 16% of all the studies reported on children. The difference in seroprevalence across the African region was not significant (95% CI, X2 =0.86; p =0.35), although specifically, a relatively significant ETTA MASHU ELIZABETH, PHD IN MICROBIOLOGY|UNIVERSITY OF VENDA, 2019|VIII level of infection was observed in HIV-infected children. About 38% of the countries had data on K1 genotypes A, A5, B, C, F and Z which occurred at frequencies of 5.3%, 26.3%, 42.1%, 18.4%, 5.3% and 2.6% respectively. Twenty-three percent of the countries had data for K15 genotypes, whereas genotypes P, M and N occurred at frequencies of 52.2%, 39.1% and 8.7% respectively. Data on HHV-8 inter-genotype recombinant is scanty. Our finding suggests that HHV-8 is endemic on the entire African continent, and in HIV endemic regions, but there is need for a harmonized testing protocol for better understanding of HHV-8 seropositivity. HHV-8 genotype A5 and B for K1 gene and genotype P and M for K15 gene are the most predominant genotypes in Africa. The review, for the first time, has provided information on HHV-8 burden on the entire African continent, and suggests that vaccine development efforts for Africa should focus on genotypes B and P. The second component of the investigation focused on the burden of HHV-8 in an HIV population in Northern South Africa (Limpopo Province). Plasma from 3501 HIV infected individuals from 5 districts in Limpopo Province were assessed for antibodies to both the lytic antigen (ORFK8.1) and the latent antigen (ORF73). The distribution of infection was analyzed based on demographic, socioeconomic, and immunological parameters. Statistical inferences for significant differences were determined by Chisquare at a confidence interval of 95%. P-values less than 0.05 were considered significant. About 19.0% of the study population was positive for antibodies to either the lytic or latent antigens or both. Prevalence of antibodies to the lytic antigen was significantly higher than prevalence of antibodies to the latent antigen (17.3% vs 4.1%; p=0.0001). Significant differences were observed for age groups, racial population groups, districts and year of sample collection (p=<0.0001, p=<0.0001, p=<0.0001 and p=0.0385) respectively. Associations were found between both antigens in comparison to the different variables such as age group, racial population groups and districts (R2 value ranging between 0.886 and 1.0). The burden of HHV-8 has now been established for the first time in Northern South Africa. The third aspect of the investigation was a meta-analysis of HHV-8 seroprevalence in Southern Africa in order to understand the impact of geographical location (urban vs rural) on infection. The analysis revealed a significant association between urban settings and HHV-8 infection (p=0.0001). ETTA MASHU ELIZABETH, PHD IN MICROBIOLOGY|UNIVERSITY OF VENDA, 2019|IX The fourth component of the thesis examined the detection of HHV-8 antigen through polymerase chain reaction (PCR) in 534 participants in HIV infected and HIV noninfected populations. A selection of mouthwash DNA samples were subjected to Next Generation Sequencing (NGS) for subsequent genotype inference. Mouth wash samples were obtained from each consenting individual before eating or smoking, and their DNA was purified. A 233bp fragment of the ORF26 gene of HHV-8 was amplified by PCR. HHV-8 was detected in 150 of the 534 participants (28.1%). A significant difference in detection was observed for gender, HIV status, district and the level of education (p=0,0003; p=0.0094; p=0.0002 and p=0.0095) respectively. Consensus sequences were derived from NGS reads for 13 samples. The genotyping results revealed that genotype Q, B, E and N are the genotypes predominant in the study population. As such no mixed infections were detected. Therefore, from the investigations foregoing have demonstrated for the first time the following: (1) HHV-8 is endemic in the entire African continent, which suggest a coendemicity in regions already endemic for HIV; (2) HHV-8 is endemic in Northern South Africa; (3) Urban settings in Southern Africa are associated with high HHV-8 infection; (4) HHV-8 genotypes Q, B, E and N may be predominant in Northern South Africa, with B and P common on the entire African continent. Hence, studies should focus on the generation of full length HHV-8 genomes of the common genotypes to support the selection of genes for vaccine design and development. / NRF

This Master Thesis deals with image restoration using deconvolution. The terms introducing into deconvolution theory like two-dimensional signal, distortion model, noise and convolution are explained in the first part of thesis. The second part deals with deconvolution methods via utilization of the Bayes approach which is based on the probability principle. The third part is focused on the Alternating Minimization Algorithm for Multichannel Blind Deconvolution. At the end this algorithm is written in Matlab with utilization of the NAG C Library. Then comparison of different optimization methods follows (simplex, steepest descent, quasi-Newton), regularization forms (Tichonov, Total Variation) and other parameters used by this deconvolution algorithm.