http://hdl.handle.net/123456789/4 http://hdl.handle.net/123456789/5837 MODELIRANJE ZVEZDANIH OSCILACIJA U TESNO DVOJNIM ZVEZDAMA Latković, Olivera The dissertation deals with modeling of stellar oscillations in close binary systems. This topic is импортант not only in for the study of binary stars, but also for asteroseismo-logy. One of the key problems of asetroseismology is the “mode identification” of stellar oscillations. Mode identification is the process of associating an oscillation frequency measured from photometric or spectroscopic observations with a spherical harmonic of degree and order which describes the spatial characteristics of the mode. The main obstacle for this crucial step between the collection and interpretation of data is the symmetry inherent to the patterns of oscillations that makes the periodic changes in the brightness and the radial velocities of surface elements cancel each other out, resulting in diminishing of observed amplitudes. Low sensitivity of both photometry and spectroscopy to high degree modes ( and in photometric and spectroscopic observations, respectively), is one of the consequences of this phenomenon, making the detection and identification of oscillations a difficult task. A method for mode identification by grid-fitting spherical harmonics to photometric light curves of pulsating stars inside eclipsing binary systems is developed in the dissertation. The eclipse of the pulsating star by its binary companion has visible effects on the observed properties of the oscillations because the eclipse spoils the symmetry of oscillation pattern, producing a modulation of frequency, amplitude and phase unique for each mode that can be recognized and fitted. Fitting, however, requires a model of a binary system with pulsating components. The only existing implementation of the method of fitting spherical harmonics to light curves uses a very simple model of the binary, with ideally spherical stars in circular orbits, and does not account for any of the proximity effects. Moreover, the oscillations are represented as sinusoidal perturbations of an arbitrary surface brightness distribution. This dissertation uses a much more detailed model, based on Roche geometry that includes all the important proximity effects. Modeling of stellar oscillations is improved by representing them as direct perturbations of local tempe- v rature and gravitational potential and including the effects of tidal distortion and rotation on the frequencies and spatial properties of the modes. The scientific goal of the dissertation is to develop a reliable method – the method of fitting spherical harmonics – for mode identification on pulsating stars in close binary systems, in order to enable asteroseismological studies of their interiors. The basic assumption is that a close binary system can be represented using the Roche model, which is based on the approximation of total central condensation. In other words, it is assumed that the contribution of outer layers of the star to its total mass can be neglected. With this approximation, it is possible to treat the gravitational interaction of the components as the interaction of point masses. Within the Roche model, the shape of the star is determined by the Roche potential that corresponds to the superposition of the gravitational and the centrifugal force. The temperature distribution across the surface is determined by the von Zeipel law that defines the dependence of flux on the effective gravitational acceleration. Stellar oscillations are then modeled as perturbations of the local values of the Roche potential and temperature. It is assumed that the oscillations are adiabatic, of small amplitudes, and that they can be represented using spherical harmonics. It is also assumed that the symmetry axis of the oscillations will coincide with the dominant geometrical axis (usually with the rotation axis, or in the case of tidally distorted stars, with the line connecting the centers of the components). The proposed method of mode identification on pulsating components of close binary systems is implemented as a part of the modeling program Infinity. Infinity is based on the Roche model and accounts for all the phenomena that influence the formation of light and radial velocity curves, from limb darkening and surface temperature distribution caused by departures from spherical shape, to the reflection effect, irregularities in surface brightness and the presence of the accretion disc. Stellar oscillations can be modeled on one or both components of the system. The method is verified by means of tests using synthetic data. In other words, the results of fitting are compared to the stellar and orbital parameters that were used to generate vi the synthetic light curves, or the fake “observations”. The tests encompass both favorable and unfavorable configurations (total and partial eclipses, approximately spherical and tidally distorted stars, modes of low and high degrees and so forth). The results are finally compared to the results of a similar technique of mode identification – the method of eclipse mapping. From the obtained results, we can conclude that the proposed method of mode identification is reliable (i.e. provides correct identification) for approximately spherical stars in detached binary systems. The results for tidally distorted stars are encouraging, but show that before an attempt is made to apply the method on real observation of that nature, it will be necessary to include the simultaneous fitting of frequency, amplitude and phase for each trial mode into the procedure of mode identification, and to try to solve the problem of ambiguous identifications. This will be the focus of my future work. http://hdl.handle.net/123456789/5836 EKSTRAKCIJA INFORMACIJA VOĐENA ONTOLOGIJAMA (MODEL ZA SRPSKI JEZIK) Vujičić Stanković, Staša 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 semi‐ structured 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. http://hdl.handle.net/123456789/5835 UNAPREĐIVANJE SMT REŠAVAČA KORIŠĆENJEM CSP TEHNIKA I TEHNIKA PARALELIZACIJE Banković, Milan SMT solvers implement decision procedures that check for satisfiability of first-order logical formulae with respect to some decidable theory. They rely on the powerful techniques that are used for solving boolean satisfiability problem (SAT), combined with specific procedures that permit reasoning in a particular theory. Typical applications of SMT solvers are mostly found in software verification, and for this reason the theories frequently considered in SMT solvers are best suited for such kind of applications. Extending the applicability of SMT solvers to other areas may require defining new SMT theories, as well as developing the corresponding decision procedures for such theories. In that sense, in this thesis we consider improving of SMT solvers by extending their applicability to solving CSP problems. Such problems consider variables with finite domains, and the goal is to find the assignment of values to the variables of the problem satisfying all the imposed constraints. When CSP solving is considered, the main drawback of the existing SMT theories is that they are not adapted to the problems with finite domains, and are also incapable of reasoning about global constraints, which play the significant role in most CSP problems. For this reason, in this thesis a novel SMT theory is defined that enables natural representation of CSP problems, since it includes support for some frequently used global constraints. For such theory, we developed a decision procedure based on the existing techniques borrowed from the traditional CSP solvers, but these techniques are adapted in the way that permits their usage within SMT solvers. The decision procedure currently supports two types of global constraints: the alldifferent constraint and the linear constraint. In case of the alldifferent constraint, the main contribution is a novel algorithm for generating explanations of conflicts and propagations, which is required for the conflict analysis. In case of the linear constraint, a novel filtering algorithm is developed that takes into consideration the existence of the alldifferent constraints in the given problem, which can lead to a stronger propagation. Another direction of improving SMT solvers that is considered in the thesis is the usage of the parallelization techniques. We consider the parallelization of the simplex algorithm, which is used in SMT solvers as the decision procedure for the linear arithmetic. We also consider the parallel portfolio approach, as well as the hybridization of the two approaches. A comprehensive experimental evaluation is provided on a large number of instances, both industrial and randomly generated. For the purpose of all the mentioned research, during the work on the thesis a new open-source SMT solver called argosmt is developed, based on DPLL(T ) architecture. http://hdl.handle.net/123456789/5834 Verovatnosni računi sekvenata i klasifikacija neklasičnih logika zasnovana na entropiji Boričić, Marija After a brief introductory survey, this work is divided into two parts. The first part deals with presence of probability in logic (v. [16], [17], [18], [19], [22], [23] and [24]), and the second one is devoted to the application of entropy in classification of many–valued logics (v. [14], [15], [20], [21] and [25]). The basic idea, dominant in the first part of the work, is to enrich the Gentzen’s sequent calculus LK for propositional classical logic by a kind of probability operator defined over the sequents ¡ ` ¢ in order to express the fact that ”the truthfulness probability of ¡ ` ¢ belongs to the interval [a; b] µ [0; 1]”. We introduce the following four systems: LKprob, LKprob("), NKprob and LKfuzz. The basic form of sequents in LKprob is ¡ `b a ¢ with the above given intended meaning. The system LKprob(") is focused on the Suppes’ forms ¡ `n ¢ enabling to formalize the sentence ”the truthfulness probability of ¡ ` ¢ belongs to the interval [1 ¡ n"; 1] µ [0; 1]”, for some n 2 N. The system NKprob presents a natural deduction counterpart of the sequent calculus LKprob. The models founded on Carnap– Popper–Leblance probability semantics are defined for each of these calculi and accompanied by the corresponding soundness and completeness results. Finally, the calculus LKfuzz is introduced with a more general form of the sequents ¡ `x ¢, where x is an element of a finite lattice, with the aim to describe a fuzzification of LK. The meaning of ¡ `x ¢ is that ”x is the fuzziness measure of ¡ ` ¢”. Models for LKfuzz are given with soundness and completeness results, and a proof– theoretical treatment of LKfuzz includes the cut–elimination theorem. The second part of the work explores the fact that each logical system associated with the partition induced by the corresponding Lindenbaum–Tarski algebra makes it possible to define its entropy. We define the entropy of a logical system based on geometric distribution of measures over matching partition of set of formulae. This iv definition enables the classification of many–valued propositional logics according to their entropies. Asymptotic entropy approximations for some infinite–valued logics are proposed as well. The considered examples include Lukasiewicz’s, Kleene’s and Priest’s three–valued logics, Belnap’s four–valued logic, G¨odel’s and McKay’s m– valued logics, and Heyting’s and Dummett’s infinite–valued logics.