Auflistung Doctoral Dissertations nach Titel
-
Petrić, Zoran (Belgrade)[more][less]
Zusammenfassung: In this dissertation methods of the proof theory are used to investigate coherence in some categories. Moreover, it is shown what the categorical notion of coherence means in the categorial proof theory. The thesis consists of three chapters. MacLane’s results for monoidal categories and symmetric monoidal categories are extended in Chapter 1 of the dissertation to some other categories with multiplication: relevant categories, affine categories and symmetric monoidal categories. All the results are formulated in terms of natural transformations equipped with “grafs” (g-natural transformations). It is proved, as consequences of these results, that relevant categories, affine categories and symmetric monoidal categories have the coherence property. Moreover, using these results, some basic relations between the free categories of these classes of categories are presented in Chapter 2 of the dissertation. In Chapter 3, an extension of the notion of dinatural transfomation is introduced in order to give a criterion of preservation of dinaturality under composition. An example of an application is given by proving that all cartesian closed canonical categories transformations are dinatural. Finally, an alternative sequent system for a fragment of intuitionistic propositional logic is introduced as a device, and a cut-elimination procedure is established for this system. URI: http://hdl.handle.net/123456789/187 Dateien zu dieser Ressource: 1
phdZoranPetric.pdf ( 3.130Mb ) -
Rakočević, Vladimir (Belgrade , 1984)[more][less]
URI: http://hdl.handle.net/123456789/250 Dateien zu dieser Ressource: 1
phdVladimirRakocevic.PDF ( 4.651Mb ) -
Martinović, Miroslav (Belgrade)[more][less]
URI: http://hdl.handle.net/123456789/191 Dateien zu dieser Ressource: 1
phdMiroslavMartinovic.pdf ( 3.650Mb ) -
Martinović, Nemanja (Beograd , 2017)[more][less]
Zusammenfassung: Within this dissertation results from the analysis of formation, abundance and evolution of the dwarf galaxies from cosmological simulations will be presented. We will present results from first cosmological simulation which was performed and analyzed in its entirety in Serbia. From the obtained results it was shown how the large scale structure formed, primarily the formation of clusters of galaxies. Since the clusters of galaxies are dominant structures in the universe, which are relatively slowly forming in relation to the existence of the universe, using the Illustris cosmological simulation, with included hydrodynamics, it will be shown that a significant part of the clusters of galaxies are not in the state of dynamic equilibrium, as some authors claim, therefore their formation process continues. The obtained results will be used to divide the clusters of galaxies into three types: interacting clusters, clusters interacting with smaller groups (weakly interacting clusters), and clusters of galaxies that are not interacting. As the dwarf galaxies constitute largest number of galaxies in the universe, notably largest number in the clusters of galaxies, this raises the question how cluster’s interactions affect the structure and abundance of a diverse type of dwarf galaxies within them. After a brief review of today’s known types of dwarf galaxies, we will show that there is susceptibility of the abundance of dwarf irregular galaxies in relation to whether the parent cluster of galaxies is in interaction or not. As it is assumed that the dwarf irregular galaxies are predecessors for the formation of the most numerous types of dwarf galaxies, this could point to the dominant channel of delivering these galaxies to clusters of galaxies where they are expected to undergo morphological transformation. In the end, the discovery of two formation channels for compact elliptical galaxies in the clusters of galaxies will be presented. The formation of this type of dwarf galaxies has been the subject of discussion due to limitations in observations and their compact nature from which it could not be concluded which process leads to their formation. It has been shown here that they occur either by tidal stripping of large spiral galaxies after their spiraling into the cluster of galaxies or forming directly inside clusters from the clouds of gas which is most probably formed by the accretion of cold gas from the environment. URI: http://hdl.handle.net/123456789/4505 Dateien zu dieser Ressource: 1
nm_dis1.pdf ( 25.52Mb ) -
Berić, Mladen (Belgrade , 1912)[more][less]
-
Daoub, Hamza (Beograd , 2013)[more][less]
Zusammenfassung: In this thesis, we are going to highligth two di erent relations between graphs and nite commutative rings. The rst one is the well known as Unitary Cayley Graph, where the study of this assocciation and some results are presented from [1]. The second one is a completely di erent; it connects digraphs with quadratic polynomials with coe tents in Zn under the mapping (a; b) 7! (a + b; ab), for some n < 1. A Computer calculations are involved to support the study. The algorithm which is used for these calculations is built on original Mathematica and Matlab Softwares. Furthermore, Some principles are needed in this thesis for the seek of support and completeness. . . URI: http://hdl.handle.net/123456789/4267 Dateien zu dieser Ressource: 1
phdHamza_Daoub.pdf ( 1.154Mb ) -
Daoub, Hamza (Belgrade , 2013)[more][less]
Zusammenfassung: In this thesis, we are doing to highlight two different relations between graphs and finite commutative rings. The first one is the well known as Unitary Cayley Graph, where the study of this association and some results are presented from (1). The second on is a completely different; it connects digraphs with quadratic polynomials with coeffitients in Zn under the mapping (a,b)-> (a+b,ab), for some n<...... A Computer calculations are involved to support the study. The algorithm which is used for these calculations is built on original Mathematica and Matlab Softwares. Furthemore, Some principles are needed in this thesis for the seek of support and completeness... URI: http://hdl.handle.net/123456789/3834 Dateien zu dieser Ressource: 1
HDPhD_o.pdf ( 2.806Mb ) -
Grulović, Milan (Belgrade , 1984)[more][less]
Zusammenfassung: The thesis consists of five chapters. In the first part of Chapter 1 forcing relations for infinite logics are considered. It is shown that if in the case of infinite logic we want to extend syntactic apparatus adequately and that forcing joining stays deductive closed set which contains all logically valid formulas, then forcing joining has to formulate by "weak" formulas. In the second part of this chapter a correction of the proof of the interpolation theorem for infinite logics is presented. The result from Chapter 2 is the following: it is shown that all important properties of Robinson’s finite forcing are transmitted to n-finite forcing by corresponding "n-notions". Moreover, a construction of n-finite forcing joining by Henrard’s approximation chains is presented. The main result of Chapter 3 is that for each theory T of a language L there is an extension T' defined in the corresponding extension L' such that. Relations between a theory (the theory of dense linearly ordering with maximal and minimal elements, the theory of groups, the theory of Abelian groups, the theory of fields, full arithmetic, Peano’s arithmetic) and its corresponding n-finite forcing joins are studied in Chapter 4. Also relations between n-finite forcing joins are studied. A connection between n-finite forcing and the type theory are studied in Chapter 5, and some generalizations of the known results are given. URI: http://hdl.handle.net/123456789/56 Dateien zu dieser Ressource: 1
phdMilanGrulovic.pdf ( 2.377Mb ) -
Stojanović, Sana (Beograd , 2016)[more][less]
Zusammenfassung: The advance of geometry over the centuries can be observed through the development of di erent axiomatic systems that describe it. The use of axiomatic systems begins with Euclid, continues with Hilbert and Tarski, but it doesn't end there. Even today, new axiomatic systems for Euclidean geometry are developed. Avigad's axiomatic system goes back to the beginnings and precisely describes basic derivations presented in Euclid's ½Elements . Writing an axiomatic system in a format suitable for computer theorem proving is a challenge in itself. Imprecise formulations of axioms which appear in books get exposed only when they need to be written in a format suitable for computers. The formalization of di erent axiomatic systems and computer-assisted proofs within theories described by them is the main motif of this thesis. The programs for theorem proving have existed since the eighties and today they present a collection of very powerful tools. This thesis presents a system for automated and formal theorem proving which uses the power of resolution theorem provers, a coherent prover, as well as interactive theorem provers for verifying the generated proofs. Coherent prover ArgoCLP is one of the contributions of the thesis. Additionally, the thesis develops a dialect of coherent logic based on natural deduction which enables simple transformation of generated proofs into proofs written in languages of interactive provers Isabelle and Coq as well as in natural languages, English and Serbian. The system for theorem proving is applied to three axiomatic systems of Euclidean geometry, thus illustrating its applicability to both proving the large mathematical theories and veri cation of informal proofs from mathematical textbooks. URI: http://hdl.handle.net/123456789/4416 Dateien zu dieser Ressource: 1
SanaStojanovic.pdf ( 1.885Mb ) -
Marić, Filip (Belgrade)[more][less]
URI: http://hdl.handle.net/123456789/231 Dateien zu dieser Ressource: 1
phdFilipMaric.pdf ( 1.980Mb ) -
Simić, Danijela (Beograd , 2017)[more][less]
Zusammenfassung: In this thesis is presented interactive formalization of various models of geometry and algebraic methods for automated proving geometry theorems. We present our current work on formalizing analytic (Cartesian) plane geometries within the proof assistant Isabelle/HOL. We give several equivalent definitions of the Cartesian plane and show that it models synthetic plane geometries (using both Tarski’s and Hilbert’s axiom systems). We also discuss several techniques used to simplify and automate the proofs. As one of our aims is to advocate the use of proof assistants in mathematical education, our exposure tries to remain simple and close to standard textbook definitions, but completely formal and mechanically verifiable. This formalization presents the develop of the necessary infrastructure for implementing decision procedures based on analytic geometry within proof assistants. Furthermore, we investigate complex numbers. Deep connections between complex numbers and geometry had been well known and carefully studied centuries ago. Fundamental objects that are investigated are the complex plane (usually extended by a single infinite point), its objects (points, lines and circles), and groups of transformations that act on them (e.g., inversions and Möbius transformations). In this thesis we treat the geometry of complex numbers formally and present a fully mechanically verified development within the theorem prover Isabelle/HOL. We discuss different approaches to formalization and discuss major advantages of the more algebraically oriented approach. Apart from applications in formalizing mathematics and in education, this work serves as a ground for formally investigating various non-Euclidean geometries and their intimate connections. We also present a formalization of part of Tarski axiom system withing Poincare disk model in Isabelle/HOL. Further on, we analyze connections between geometry and polynomials and the use of these connections. In Euclidean geometry, objects and relations between them can be expressed as polynomials. Further, any geometry construction can be expressed by set of polynomials and geometry statements can be proved by using algebraic methods (e.g. the Gröbner bases method or Wu’s method) over that set of polynomials. We describe an implementation of an algorithm in Isabelle/HOL that accepts a term representation of a geometry construction and returns its corresponding set of polynomials. Our further work will be to use the method of Gröbner bases within the Isabelle system on the generated polynomials, in order to prove correctness of the given construction. Furthermore, we investigate how spatial geometry constructions can be presented using polynomials. We investigate two different approaches in deriving those polynomials and then compare efficiency of algebraic provers depending on the approach used. We present a fully automated system for transforming geometry constructions into set of polynomials. Our further work would be to relate these geometry provers with dynamic geometry software and thus make easier for students to use it. URI: http://hdl.handle.net/123456789/4499 Dateien zu dieser Ressource: 1
06062017danijela_doktorat.pdf ( 1.158Mb ) -
Smole, Majda (Beograd , 2017)[more][less]
Zusammenfassung: Formation mechanism of supermassive black holes (SMBHs) observed in the early Universe is still not fully understood. The goal of this thesis is to nd under what conditions black hole (BH) remnants of Population III stars can form SMBH with mass 109 M by redshift z = 7. We use Millennium and Millennium-II N-body cosmological simulations to investigate BH growth on cosmological scales. In order to exploit both high mass resolution in the Millennium-II simulation and large box size in the Millennium simulation, we develop a method to combine these two simulations together. BHs can grow through mergers with other BHs and through episodes of gas accretion triggered by major mergers of dark matter haloes. As a constraint in our model, we use observed BH mass function at redshift z = 6. We nd that BH seeds with masses 100 M could grow to SMBHs in distant quasars if e ective Eddington ratio is xed at fEdd = 3:7 and each accretion episode is limited to 50 Myr. During a BH merger asymmetric emission of gravitational radiation can lead to BH kick. Gravitational wave recoil can completely eject BH from it's host if the kick velocity is larger than the escape velocity from the galaxy. Since gravitational wave recoil could a ect SMBH growth through mergers, recoiling BHs are investigated in di erent models of host galaxies. BH trajectories are investigated in static and evolving dark matter halo potential described by NFW and Einasto density distributions. We nd that evolution of dark matter haloes clearly impact their capability to retain recoiling BHs since escape velocities are lower for smaller haloes at high redshifts. If the Einasto pro le is considered, then a larger number of complete BHs ejections is expected compared to NFW potential. Further, we construct analytical and numerical host galaxy models whose components are dark matter halo, bulge and disc. If baryonic component of a galaxy is included escape velocity is higher compared to a purely dark matter halo potential. Major (1:1) and minor (1:10) galaxy remnants are modeled separately. In numerical models BHs are ejected from their host centre before galaxy merger is completed, so escape velocities are generally lower in numerical models compared to analytical models where galaxy potential is unperturbed. Even though BHs could occasionally escape the most massive hosts, our model is not considerably sensitive to the gravitational wave recoil except for mergers of equal mass BHs in the least massive haloes at high redshifts where kick velocities of Vk . 100 km=s could permanently eject BHs from their hosts. URI: http://hdl.handle.net/123456789/4502 Dateien zu dieser Ressource: 1
Majda_Smole_disertacija.pdf ( 4.149Mb ) -
Telebaković Onić, Sonja (Beograd , 2022)[more][less]
Zusammenfassung: n this dissertation the connection between Frobenius algebras and topological quantum field theories (TQFTs) is investigated. It is well-known that each 2-dimensional TQFT (2-TQFT) corresponds to a commutative Frobenius algebra and conversely, i.e., that the category whose objects are 2-TQFTs is equivalent to the category of commutative Frobe- nius algebras. Every 2-TQFT is completely determined by the image of 1-dimensional sphere S1 and by its values on the generators of the category of 2-dimensional oriented cobordisms. Relations that hold for these cobordisms correspond precisely to the axioms of a commutative Frobenius algebra. Following the pattern of the Frobenius structure assigned to the sphere S1 in this way, we examine the Frobenius structure of spheres in all other dimensions. For every d ≥ 2, the sphere Sd−1 is a commutative Frobenius object in the category of d-dimensional cobordisms. We prove that there is no distinction between spheres Sd−1, for d ≥ 2, because they are all free of additional equations formulated in the language of multiplication, unit, comultiplication and counit. The only exception is the sphere S0 which is a symmetric Frobenius object but not commutative. The sphere S0 is mapped to a matrix Frobenius algebra by the Brauerian representation, which is an example of a faithful 1-TQFT functor. We obtain the faithfulness result for all 1-TQFTs, mapping the 0-dimensional manifold, consisting of one point to a vector space of dimension at least 2. Finally, we show that the commutative Frobenius algebra QZ5 ⊗ Z(QS3), defined as the ten- sor product of the group algebra and the centre of the group algebra, corresponds to the faithful 2-TQFT. It means that 2-dimensional cobordisms are equivalent if and only if the corresponding linear maps are equal. URI: http://hdl.handle.net/123456789/5353 Dateien zu dieser Ressource: 1
stoDisertacijaOnic.pdf ( 9.095Mb ) -
Pavlović, Rade (Faculty of Mathematics, University of Belgrade , 2008)[more][less]
Zusammenfassung: We investigate the ful¯llment of conditions for application of Nekhoroshev theorem to real dynamical system, such as the motion of asteroids under the perturbation by major planets. We have in particular analyzed the regions of the phase space where asteroid families of Koronis and Veritas are located. The results obtained for a number of selected family members indicate that in these regions even stricter conditions (convexity, quasi-convexity and 3- jet), than the condition of steepness required by the theorem, are fullled. Consequently, the theorem of Nekhoroshev can be applied to members of Koronis family and to the members of Veritas family with regular motion. URI: http://hdl.handle.net/123456789/717 Dateien zu dieser Ressource: 1
phdRadePavlovic.pdf ( 3.135Mb ) -
Čukić, Ivan (Beograd , 2018)[more][less]
Zusammenfassung: There is a big class of problems that require software systems with asynchronously executed components. For example, distributed computations have the distributed nodes that process the data asynchronously to one anot- her, service-oriented architectures need to process separate requests asynchrono- usly, and multi-core and heterogeneous systems need to have multiple separa- te tasks running concurrently to best utilize the hardware. Even ordinary GUI applications need asynchronous components – the user interface needs to be re- sponsive at all times which means that no matter in what state the program is in, it needs to process and react to the input events coming from the user. The necessity of concurrency and asynchronous execution brings in the added com- plexity of the Inversion of Control (IoC) into the system, either through mes- sage passing or through event processing. IoC makes code difficult to develop and reason about, it increases component coupling and inhibits clean functional or object-oriented software design. In this dissertation, a method for solving the problems that IoC introduces is presented. It presents a way to model both synchronous and different types of asynchronous tasks with the continuation monad. The continuation monad serves as a primitive to build more complex control flow structures that mimic the control flow structures of the host programming language. It also allows for building more complex control structures specialized for parallelism, transactional execution, and for simulating functional programming idioms with asynchronous tasks through a generalization of the continuation monad that allows the asynchronous tasks to generate results one at a time. This allows for writing programming systems with asynchronously executed components by writing seemingly synchronous imperati- ve or functional code while leaving it up to the compiler to do all the heavy lifting and convert the written code to asynchronously executed set of tasks. Another benefit of the presented method is that it allows for easier automatic handling of the data lifetime without the need for garbage collection. This method has been successfully applied and tested in several Free/Libre Open Source Software and proprietary real-world software projects used by hun- dreds of millions of people around the world. In this dissertation, an example of a secure project management system is described which is based on a similar system implemented as a part of the KDE Plasma project. This dissertation also contains the important parts of the implementation of the AsynQt library which extends the Qt library, and its concurrency primitive – QFuture class – with functional reactive programming patterns based on the method proposed in this dissertation. URI: http://hdl.handle.net/123456789/4738 Dateien zu dieser Ressource: 1
ivan_cukic_phd.pdf ( 1.328Mb ) -
Tanović, Predrag (Montreal , 1994)[more][less]
Zusammenfassung: The thesis is a research about nonisolation properties of superstable types over finite domains in general. Two notions of nonisoltions, the notion of eventual-strong (i.e. esn) and the notion of internal are introduced. The thesis consists of three chapters. In Chapter 1 of the thesis the techniques of the stability theory which are used in Chapter 2 and Chapter 3 are overviewed. In Chapter 2 of the thesis NDFC theories are studied and the notions of dimension and U_α-rank through partial orders are developed. It is proved that if the theory T is strictly stable and the the order type of rationals cannot be embedded into the fundamental order of $T$ and there is no strictly stable group interpretable in T^eq, then the theory T has continuum non-isomorphic countable models. It is noted that strongly non-isolated types can be present due to the dimensional discontinuity property. In Chapter 3 of the thesis small superstable theories are studied. In the first part of that chapter the eventual-strong and internally nonisolated types are considered, and some properties were proved. The second part of Chapter 3 contains the proof of the following theorem: if the theory T is a complete, superstable theory, the generic type of every simple group definable in T^eq is orthogonal to all NENI types and sup{U(p)|pϵS(T)}≥ ω^ω holds, then the theory T has continuum non-isomorphic countable models. URI: http://hdl.handle.net/123456789/186 Dateien zu dieser Ressource: 1
phdPredragTanovic.pdf ( 2.221Mb ) -
Milisavljević, R. Slaviša (Belgrade , 2013)[more][less]
Zusammenfassung: The problem of the minimal mutual distances for two confocal elliptical orbits (local minima), in the literature known as the proximity calculation for minor planets and recognised recently as Minimal Orbit Intersection Distance – MOID, occupies a very important place in astronomical studies, not only because of the prediction of possible collisions of asteroids and other celestial bodies, but also because of the fact that by analysing the behaviour of asteroids during their encounters it is possible to determine their masses, changes of orbital elements and other important characteristics. Dealing with this problem in this thesis the author has analysed the distance function for two elliptical confocal orbits of minor planets combining analytical and numerical methods for proximity calculation. A survey of all relevant results in this field from the middle of the XIX century till our days indicates that the problem has been transformed from looking for a solution of two transcendental equations by applying various methods and approximations of long duration towards efficient and rapid solutions of vector equations of the system which describes the problem. In the thesis a simple and efficient analytic-numerical method has been developed, presented and applied. It finds out all the minima and maxima in the distance function and, indirectly, makes it possible to determine also the inflection points. The method is essentially based on Simovljevic’s (1974) graphical interpretation and on transcendental equations developed by Lazovic (1993). The present method has been examined on almost three million pairs of real elliptical asteroid orbits and its possibilities and the computation results have been compared to the algebraic solutions given by Gronchi (2005). The case of a pair of confocal orbits with four proximities found by Gronchi (2002), who applied the method of random samples and carried out numerous simulations with different values of orbital elements, gave the motivation to try here to find out such a pair among the real pairs of asteroid orbits. Thanks to the efficacy of the method developed in the thesis two such pairs have been found and their parameters are presented. In addition to the one meantioned above a further analysis of distance function through simulations including more than 20 million different pairs of asteroid orbits has resulted in several additional interesting solutions of the distance function. The results are given in the form of tables and plots showing the diversity of solutions for the distance function. URI: http://hdl.handle.net/123456789/2490 Dateien zu dieser Ressource: 1
phdSlavisaMilisavljevic.pdf ( 3.815Mb ) -
Šehu, Isljam (Priština , 1985)[more][less]
URI: http://hdl.handle.net/123456789/151 Dateien zu dieser Ressource: 1
phdIsljamASehu.pdf ( 2.582Mb ) -
Drešević, Milan (Beograd , 1973)[more][less]
URI: http://hdl.handle.net/123456789/4096 Dateien zu dieser Ressource: 1
Funkcionalni_prostori.PDF ( 2.559Mb ) -
Drešević, Milan (Belgrade)[more][less]
URI: http://hdl.handle.net/123456789/308 Dateien zu dieser Ressource: 1
phdMilanDresevic.pdf ( 3.667Mb )