Browsing Doctoral Dissertations by Title

Bertolino, Milorad (Belgrade)[more][less]

Dajović, Vojin (Belgrade)[more][less]

Vujičić Stanković, Staša (Beograd , 2016)[more][less]
Abstract: The basic goal of this doctoral thesis is a research into different techniques and models which are applied in information extraction, and providing an informatic support in processing of natural language texts from culinary and gastronomy domain. Information extraction is a subfield of computational linguistics which includes techniques for natural languages processing, in order to find relevant information, define their meaning and establish relations between them. A very special attention is given to ontology based information extraction. It consists of the following: recognition of instances of ontology concepts in non‐structured or semistructured texts written in natural language, reasoning over the identified instances based on the rules defined in the ontology, as well as recognition of instances and their use for instantiating the proper ontology concepts. The main result of thesis reflects in the presentation of a new model for ontology based information extraction. Besides solving tasks of information extraction, the new model includes not only upgrade of existing lexical resources and ontologies, but also creation of the new ones. Its application resulted in development of a system for extraction of information related to the culinary domain, but this new model can be used in other fields as well. Beside this, the food ontology has been developed, Serbian WordNet is extended for another 1.404 synsets from the culinary domain, while electronic dictionary of Serbian is enlarged with 1.248 entries. The significance of the model application comes from the fact that the new and enriched linguistic resources can be used in other systems for natural language processing. The opening chapter of the thesis elaborates the need of providing an informatic model for processing a huge linguistic corpus related to culinary and gastronomy domain, through methodologically precise and solid approach integrating pieces of information on the domain. Also, the formalization of the basic research subject, text in electronic form, has been presented. Further on, the chapter contains a description of the natural languages approximations introduced in order to enable modern information technologies to process texts written in natural languages, and it emphasizes the need to make the characterisation of the text language with corresponding corpus and sublanguage. Further on in the first chapter, the task of information extraction, and the models for informatic processing of non‐structured or semi‐structured texts, used by the computer to interpret the meaning that the author (not necessarily a human) has intended to give while writing the text, are defined. Additionally, this chapter contains the description of the methods used in information extraction field – methods based on rules and methods based on machine learning. Their advantages and shortcomings are listed, so as the reasons why in this thesis are used techniques based on linguistic knowledge. As a conclusion to the introduction chapter, a special attention is given to ontologies, WordNet, and the significance of its usage as ontology. The second chapter contains the presentation of the linguistic resources and tools exploited in this thesis. It describes morphological dictionaries and local grammars used for solving the problem of information extraction from texts written in Serbian. A review of information extraction systems is given subsequently. At the end of the second chapter, the stages in processing of Serbian written texts during the information extraction in the software systems Unitex and GATE are described. The main result of the thesis is presented in the third chapter. It is the model for solving the problem of information extraction by integrating linguistic resources and tools, which includes creation of a text corpus, definition of tasks for information extraction, establishment of finite state models for information extraction, and their application accordingly, iterative enlarging of electronic morphological dictionaries, enrichment and enhancement of WordNet, and creation of new ontologies. Each of these steps is described thoroughly. Even though the model was at first considered as a solution for problems in processing Serbian, it can be equally applied for processing texts written in other languages, with the development of suitable language resources accordingly. The implementation of the above explained steps is described in the fourth chapter, through a system for information extraction from the culinary texts written in Serbian. Then follows the description of a bond in the development and mutual complement of lexical resources through steps in creating domain corpus, identifying culinary lexica, expanding and upgrading of WordNet and electronic morphological dictionaries, and developing of domain ontologies – the food ontology, the approximate measure ontology, and the ontology of ingredients that can be used as mutual replacements in the culinary domain. This system, developed for information extraction, has served for creating an advanced search system which, based on a corpus of culinary texts, generates all possible answers to inquiries made by users. In the frame of this system is implemented a specific method which serves for creation of links between different recipes. This is used in case when the user reviews a text of a recipe and notices that in preparing description features some part which already had appeared in other recipe, but with additional or different explanation. Another contribution of this thesis is application of developed ontologies in tasks that convert approximate measures into standard measures, and establishment of similarities among the recipes. The similarity of the recipes is defined as similarity of texts which describe process of course preparation in accordance with a specific recipe. The last chapter contains final conclusions and directions for future research. URI: http://hdl.handle.net/123456789/4410 Files in this item: 1
teza_Stasa.pdf ( 10.38Mb ) 
Hajduković, Dimitrije (Belgrade)[more][less]
URI: http://hdl.handle.net/123456789/38 Files in this item: 1
phdDimitrijeHajdukovic.pdf ( 1.535Mb ) 
Mališić, Jovan (Belgrade)[more][less]

Zlatanović, Milan (Niš , 2010)[more][less]

Milošević, Stefan (Beograd , 2017)[more][less]
Abstract: In this paper we present some norm inequalities for certain elementary operators and inner product type transformers, specially for Schatten norms, if the families of operators generating those transforms consists of arbitrary operators, and Q norms if at least one of those families consists of mutually commuting normal operators. Among others, we present inequalities that are generalizing the inequality p IA AX p IB B 6 X AXB ; from [11, Th. 2.3], for normal contractions and arbitrary unitarily invariant norm, to the case of Schatten norms and arbitrary contractions, as well as Q norms if at least one of the contractions A or B is normal. Also, by applying norm inequalities for operator monotone and operator convex functions, some refined Cauchy  Schwarz operator inequalities, as well as Minkowski and Landau  Gruss norm inequalities for operators are obtained as well. URI: http://hdl.handle.net/123456789/4656 Files in this item: 1
Stefan_Milosevic_Disertacija.pdf ( 2.544Mb ) 
Kurepa, Đuro (Paris , 1935)[more][less]
Abstract: This thesis is the first systematic study of trees and ramified partially ordered sets and of their close relationship to linear orderings. It was the source of many crucial notions and problems in this area as, for example, the notions of Aronszajn and Souslin tree. The problem whether inaccessible cardinals have the tree property i. e., whether they satisfy the analogue of Koning’s infinity lemma is considered in this thesis for the first time. The thesis consists of Chapter I (the subchapters t1t8), Chapter II (the subchapters t9t12), and an appendix ("Complément"). In t8A11 trees are classified as "large", "étrioit" and "ambigu" according to their heights and widths. In the Theorem 5bis the following property is presented: the very thin and tall trees ("étrioit") always have cofinal branches i.e., chains intersecting every level. This result was a source of the problem whether the same fact is true about the class of slightly wider trees ("ambigu") i.e., the trees of height equal to some cardinal Θ and whose levels are now only assumed to be of size less than Θ. This is the problem known today as the problem whether Θ has the tree property. In t10.2 the important notion σE is defined, where E is a linearly (or partially) ordered set. Namely, σE is a tree of all nonempty bounded and wellordered subsets of E with the endextension as the tree ordering. The problem whether inaccessible cardinals have the tree property appeared in t10.3. In t10.4 two following problems are mentioned: whether every Aronszajn tree is a subtree of σQ, and if every two uniformly branching Aronszajn trees are isomorphic. A question related to previous one, whether there is a homogeneous Aronszajn tree is also mentioned. The property that every two countable infinitely branching trees of the same height are isomorphic is proved in t10.5 (Theorem 1). Appendix contains a proof that Souslin’s problem is equivalent to the statement that every uncountable tree contains an uncountable chain or untichain i.e., that three are no Souslin trees. URI: http://hdl.handle.net/123456789/326 Files in this item: 1
disert.pdf ( 7.243Mb ) 
Šovljanski, Mirjana (Belgrade)[more][less]

Petrić, Zoran (Belgrade)[more][less]
Abstract: 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” (gnatural 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 cutelimination procedure is established for this system. URI: http://hdl.handle.net/123456789/187 Files in this item: 1
phdZoranPetric.pdf ( 3.130Mb ) 
Rakočević, Vladimir (Belgrade , 1984)[more][less]

Martinović, Miroslav (Belgrade)[more][less]
URI: http://hdl.handle.net/123456789/191 Files in this item: 1
phdMiroslavMartinovic.pdf ( 3.650Mb ) 
Martinović, Nemanja (Beograd , 2017)[more][less]
Abstract: 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 Files in this item: 1
nm_dis1.pdf ( 25.52Mb ) 
Berić, Mladen (Belgrade , 1912)[more][less]

Daoub, Hamza (Belgrade , 2013)[more][less]
Abstract: 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 Files in this item: 1
HDPhD_o.pdf ( 2.806Mb ) 
Daoub, Hamza (Beograd , 2013)[more][less]
Abstract: 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 Files in this item: 1
phdHamza_Daoub.pdf ( 1.154Mb ) 
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 nfinite forcing by corresponding "nnotions". Moreover, a construction of nfinite 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 nfinite forcing joins are studied in Chapter 4. Also relations between nfinite forcing joins are studied. A connection between nfinite 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 computerassisted 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]

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 nonEuclidean 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 )