Browsing by Title
-
Dimitrijević, M. S.; Popović, L. Č.; Kovačević, J.; Dačić, M.; Ilić, D. (RAS , 2006)[more][less]
-
Mićović, Nemanja (Beograd , 2018)[more][less]
-
Grulović, Milan (Belgrade , 1984)[more][less]
Abstract: 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 Files in this item: 1
phdMilanGrulovic.pdf ( 2.377Mb ) -
Stojanović, Sana (Beograd , 2016)[more][less]
Abstract: 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 Files in this item: 1
SanaStojanovic.pdf ( 1.885Mb ) -
Marić, Filip (Belgrade)[more][less]
-
Prešić, Marica (Beograd , 1982)[more][less]
-
Simić, Danijela (Beograd , 2017)[more][less]
Abstract: 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 Files in this item: 1
06062017danijela_doktorat.pdf ( 1.158Mb ) -
Marković, Mihalo (Kultura, Beograd , 1957)[more][less]
URI: http://hdl.handle.net/123456789/743 Files in this item: 1
Formalizam u savremenoj logici.pdf ( 14.97Mb ) -
Unknown author (, 2013)[more][less]
-
Smole, Majda (Beograd , 2017)[more][less]
Abstract: 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 Files in this item: 1
Majda_Smole_disertacija.pdf ( 4.149Mb ) -
Obuljen, Andrej (Beograd , 2013)[more][less]
-
Žokalj, Milan (Zagreb , 1969)[more][less]
-
Tomić, S. Aleksandar; Jovanović, A. Borivoje (Astron. Obs. Belgrade , 2000)[more][less]
-
Nicolis, Gregorie; Nicolis, Gregorie (World Scientific , 2007)[more][less]
-
Gallavotti, Giovanni (Roma , 2000)[more][less]
-
Abraham, Ralph; Marsden, E. Jerrold (New York , 1987)[more][less]
-
Fung, Y. C. (New Jersey , 1965)[more][less]
-
Penrose, O. (PERGAMON , 2014)[more][less]
-
Ioro, Jose Rafael; Ioro, Valeria de Magalhaes (Cambridge , 2001)[more][less]
-
Jankov, Slobodan (Obs. Astron. Belgrade , 1995)[more][less]