Browsing Doctoral Dissertations by Title
Prethodna
Strana 566-585 od 585
-
Nikolić, Mladen (Belgrade , 2013)[more][less]
Abstract: In this thesis the problem of guiding search in automated theorem proving is considered. The thesis consists of two parts that have the CDCL search system, the system intensively used by modern SAT solvers, as their common topic. In the rst part of the thesis a simple approach to guiding search is considered | guiding by the selection of the solver, its heuristics, and their parameters, based on the properties of an instance to be solved. The basis of the proposed methods for algorithm selection is syntactical similarity of formulae which is re ected in their graph structure. This graph similarity is established and analyzed by using an original graph similarity measure (which turned out to be useful in other contexts, too). Yet, practical approaches to measuring similarity of formulae are based on their numerical features due to the computational complexity issues. Two simple methods for algorithm selection, based on k nearest neighbors, were proposed. The rst technique, ArgoSmArT is based on classi cation of instance in one of the prede ned families for which the e cient algorithms are known. The instance is solved by algorithm corresponding to the family to which the instance was classi ed. The second technique, ArgoSmArT k-NN is based on nding several similar instances in the training set for which the solving times by all considered algorithms are known. The instance is solved by the algorithm that behaves the best on those instances. ArgoSmArT technique is better suited for con guration selection of a SAT solver, and ArgoSmArT k-NN for SAT solver selection. ArgoSmArT k-NN technique showed to be more e cient than the most important and very complex system for SAT solver selection | SATzilla system. Apart from CNF SAT solver selection, the problem of non-CNF SAT solver selection is considered. The focus was not on solver selection techniques, since the proposed techniques are directly applicable, but on the attributes that can be used to describe non-CNF SAT instances, which have not been proposed earlier. The results in this domain are positive, but still limited. The main reason for that is the lack of greater number of non-CNF SAT solver of di erent behaviour, which is not surprising, having in mind that this kind of solvers is in its early stage of development. Apart from construction of e cient SAT solver selection system, the methodology of SAT solver comparison, based on statistical hypothesis testing is proposed. The need for such a methodology comes from great run time variations of single instance solving by a solver, which can result in di erent SAT solver orderings when one tries to compare their performance or rank them, as experimentally demonstrated. The proposed methodology gives the estimate of statistical signi cance of the performed test and the estimate of the e ect size, for instance the probability of a solver being faster than another. The second part of the thesis is concerned with generalizing CDCL search system to fragments of rst order logic. The proposed system can be used as a basis for e cient proving in some fragment if the rules of resolution and factoring are speci ed for that fragment. These rules are de ned for an extension of coherent logic. The soundness and completeness of the system are proved. The system has several distinguishing features which are a consequence of previously performed analysis of challenges in coherent logic theorem proving. The system enables rst order reasoning, instead of ground one characteristic for all existing coherent logic provers. Moreover, it introduces backjumps and lemma learning. The special attention in system design was paid to the possibility of generating readable proofs by the prover implementing the system. This possibility is one of the greatest qualities of coherent logic, but it is not easy to achieve if CDCL search system is used. One of the properties of the system that came from the need for generation of readable proofs is preservation of quanti ers in proving process which is rather unusual for existing CDCL systems. Another advantage of the proposed CDCL system is the possibility of transfer of heuristics which are already successfully employed in SAT solving to other domains. Based on the proposed system, the proof procedure Calypso for extended coherent logic was de ned which can also be used in standard coherent logic. The extension of Rete algorithm which enables detection of con icts and literals to be propagated or decided is proposed. Procedure Claypso is implemented in C++. It was evaluated on a representative coherent logic problems and it showed superior to other coherent logic provers and also the prover Vampire, the most e cient prover for rst order logic. Based on the results presented in this thesis, it can be concluded that the main hypothesis of this work, that the search system used in CDCL SAT solvers can be signi cantly improved by simple guiding and that it can be successfully formulated for fragments of rst order logic such as coherent logic, was con rmed and that the concrete answers on how to do that were provided. URI: http://hdl.handle.net/123456789/2584 Files in this item: 1
nikolic_mladen.pdf ( 1.448Mb ) -
Jovanović Spasojević, Tanja (Beograd , 2022)[more][less]
Abstract: In this thesis, subjects of consideration are the embeddings theorems of weighted Bergman spaces in Lp-spaces, as well as embeddings theorems of harmonic mixed norm spaces. The first part of the thesis generalizes the theorems of embeddings Bergman spaces into Lp(μ)-spaces, where μ is a Borel measure on a given domain. They have been earlier studied on domains such as unit ball and upper half-space. Generalization refers to bounded domains Ω ⊂ Rn with C1 boundary. This embedding will be valid to any p > 0, whenever the measure of the spaces Lp satisfies the Carledon condition. Reverse the direction will be valid only in case if p > 1 + α+2 n−2 . The second part of the dissertation also generalizes the embeddings theorems of mixed norm spaces of harmonic functions on a unit ball, where the generalization is applied to the domain Ω ⊂ Rn with C1 boundary. However, in addition we are obtaining another important result relating to the limitation of the maximum operators in the mixed norm on the general domain for the class of QNS functions. URI: http://hdl.handle.net/123456789/5378 Files in this item: 1
Jovanovic_Spasojevic_Tanja.pdf ( 1.643Mb ) -
Jovanović, Predrag (Belgrade , 2005)[more][less]
-
Dimovski, Igor (Novi Sad , 2011)[more][less]
Abstract: A comprehensive pedagogical research regarding teaching mathematics at a tertiary, university level has been presented in the PhD dissertation. The educational resources tailored in an electronic form using the programme package Matlab are integrated in the learning process. The impact of ICT use to the essential knowledge that refers to multivariate calculus (functions of several variables, vector-valued functions and the three-dimensional analytical geometry) has been statistically explored by intensive use of 3D static and dynamic visual tools. Part of the students who have participated in the research have developed Matlab programmes all by their own. One part of the research has been focused on probable impact of the programming skills on learning mathematical concepts. URI: http://hdl.handle.net/123456789/3874 Files in this item: 1
PhD_I_Dimovski.pdf ( 5.423Mb ) -
Pavlović, Marina (Beograd , 2022)[more][less]
Abstract: The study of galaxies through high redshifts are key to understanding the evolution of galaxies through cosmic times. As such objects are very difficult to observe directly, they are mainly examined using empirically derived tools such as the numerous correlations between their different parametric characteristics, one of them being the linear relationship between far-infrared and radio emission in star-forming galaxies, named the Far Infrared-Radio (FIR) Correlation.Although the correlation was considered to be stable in terms of linearity, recent works, which include galaxies at high redshifts (0 < z < 6), showed a large deviation from the correlation in these systems. The goal of this doctoral dissertation is an examination of the physical processes that lead to this kind of behavior. As a possible cause of this evolution, we will assume for the first time, and examine interactions between galaxies (collisions and close approaches). Interactions be- tween galaxies lead to the formation of shock waves on large scales that can lead to changes in the relationship between infrared and radio emissions. Our hypoth- esis was tested in several stadiums and the main results are as follows: 1. We developed models of the evolution of the FIR correlation with redshift as functions of the galaxy interaction rate. We tested the models on a sample of galaxies with an already determined morphology separately for disc galaxies and for galaxies that have recently been or are currently interacting - irregular galaxies. 2. In a small sample of 34 galaxies that we took from paper Miettinen et al. (2017), it was shown that there is an indication that the interaction between galaxies can be responsible for the evolution of the correlation with the redshift. 3. The next analysis was performed on a much larger sample of star-forming galaxies taken from COSMOS field, where we did not find any evolution of corre- lation with the redshift. Also, it was shown that the mean value of the correlation parameter is lower in irregular galaxies than in disk galaxies. Although recent observations indicated an evolution of the FIR correlation with redshift, the results of this research failed to reproduce that evolution and showed that the FIR correlation is stable with redshift. However, it was also shown that due to the interaction of galaxies, the evolution of the FIR correlation is possible if the representation of interacting systems in the sample is higher. URI: http://hdl.handle.net/123456789/5460 Files in this item: 1
Disertacija_Marina_Pavlovic.pdf ( 8.624Mb ) -
Milanović-Lazarević, Smilja (Belgrade , 1987)[more][less]
URI: http://hdl.handle.net/123456789/248 Files in this item: 1
phdSmiljaMilanovicLazarevic.PDF ( 4.155Mb ) -
Dimitrijević, Milan (Belgrade)[more][less]
Abstract: A detailed analysis of the motion of a charged particle under the influence of Coulomb, polarization, and quadrupolar potential has been performed, and analytical expressions for particle path parameters have been obtained. Also, conditions for existence of a critical impact parameter, which separates paths ending in the atom from those going to infinity, have been examined, and methods for its determination have been elaborated. Results of this investigations have been applied to the theory of Stark broadening (broadening of spectral lines under the influence of collisions with charged particles), where a special attention has been paid to the adiabatic limit, and to quasistatic and impact approximations. Modification of Stark broadening functions has been performed and it has been demonstrated that the biggest influence of path curvature on them, is in the vicinity of the critical impact parameter, which separates paths ending in the atom from those going to infinity. The change in the values of the Stark broadening functions will have the largest influence on Stark broadening parameters for lines for which, at the most probable velocity, influence of the contribution of inelastic collisions is dominant and effective polarizability large. The application of semiempirical approximative approach for calculation of Stark broadening parameters for multiply charged emitters, has been analyzed as well, and the modification of semiclassical theory has been performed. The averaged ratio of experimental and theoretical results is 0.75 for semiempirical, 1.47 for semiclassical, and 1.04 for modified semiclassical approach.У раду је извршена детаљна анализа кретања наелектрисане честице под утицајем Кулоновог, поларизационог и квадруполног потенцијала и добијени су аналитички изрази за параметре путање честице. Такође су испитани услови за егзистенцију критичног сударног параметра, који раздваја путање које завршавају у атому од оних које одлазе у бесконачност, и разрађене методе за његово налажење. Резултати овог испитивања су примењени на теорију Штарковог ширења (ширења спектралних линија под утицајем судара са наелектрисаним честицама), при чему је посебна пажња посвећена адијабатској граници и квазистатичкој и сударној апроксимацији. Изведена је модификација функција Штарковог ширења и показано је да је највећи утицај закривљености путање на њих, у близини критичног сударног параметра, који раздваја путање које завршавају у атому од оних које одлазе у бесконачност. Промена у величини функција Штарковог ширења ће највише утицати на параметре Штарковог ширења код линија за које је, при највероватнијој брзини, утицај доприноса нееластичних судара доминантан а ефективна поларизабилност велика. Такође је анализирана примена семиемпиријског апроксимативног прилаза за израчунавање параметара Штарковог ширења за вишеструко наелектрисане емитере, при чему је извршена модификација семикласичне теорије. Усредњени однос експерименталних и теоријских резултата је 0.75 за семиемпиријски, 1.47 за семикласични а 1.04 за модификовани семикласични прилаз. URI: http://hdl.handle.net/123456789/77 Files in this item: 1
Dimitrijevic.pdf ( 6.262Mb ) -
Kovjanić, Milorad (Beograd , 2023)[more][less]
URI: http://hdl.handle.net/123456789/5598 Files in this item: 1
Milorad Kovjanić - Disertacija.pdf ( 2.190Mb ) -
Vince, Ištvan (Belgrade)[more][less]
-
Šćepanović, Radoje (Belgrade , 1978)[more][less]
-
Lazović, Jovan (Belgrade , 1964)[more][less]
-
Rašajski, Marija (Belgrade)[more][less]
-
Trifunović, Milomir (Belgrade)[more][less]
-
Mišić, Miodrag (Belgrade)[more][less]
-
Plavšić, Milan (Belgrade , 1966)[more][less]
-
Kastrati, Ruzhdi (Priština , 1989)[more][less]
URI: http://hdl.handle.net/123456789/4129 Files in this item: 1
Fourie_te_disa_klasa.PDF ( 1.942Mb ) -
Đorđević, Radmila (None)[more][less]
-
Đorđević, Radmilo (Beograd , 1979)[more][less]
-
Lučić, Blagota (Belgrade , 1985)[more][less]
-
Protić, Danijela (Beograd , 2023)[more][less]
Abstract: Anomaly detection is the recognition of suspicious computer network behavior by comparing unknown network traffic to a statistical model of normal network behavior. Binary classifiers based on supervised machine learning are good candidates for normality detection. This thesis presents five standard binary classifiers: the k-nearest neighbors, weighted k-nearest neighbors, decision trees, support vector machines and feedforward neural network. The main problem with supervised learning is that it takes a lot of data to train high-precision classifiers. To reduce the training time with minimal degradation of the accuracy of the models, a two-phase pre-processing step is performed. In the first phase, numeric attributes are selected to reduce the dataset. The second phase is a novel normalization method based on hyperbolic the tangent function and the damping strategy of the Levenberg-Marquardt algorithm. The Kyoto 2006+ dataset, the only publicly available data set of real-world network traffic intended solely for anomaly detection research in computer networks, was used to demonstrate the positive impact of such pre-processing on classifier training time and accuracy. Of all the selected classifiers, the feedforward neural network has the highest processing speed, while the weighted k-nearest neighbor model proved to be the most accurate. The assumption is that when the classifiers work concurrently, they should detect either an anomaly or normal network traffic, which occasionally is not the case, resulting in different decision about the anomaly, i.e. a conflict arises. The conflicting decision detector performs a logical exclusive OR (XOR) operation on the outputs of the classifiers. If both classifiers simultaneously detected an anomaly or recognized traffic as normal, their decision was no conflict had occurred. Otherwise a conflict is detected. The number of conflicts detected provides an opportunity for additional detection of changes in computer network behavior. URI: http://hdl.handle.net/123456789/5599 Files in this item: 1
Danijela Protic - Doktorska Disertacija.pdf ( 3.143Mb )
Prethodna
Strana 566-585 od 585