Browsing by Title
-
Stanišić, Aleksandra (Beograd , 2020)[more][less]
-
Miloradović, Sofija (Beograd)[more][less]
-
Budimirović, Stefan (Beograd , 2018)[more][less]
-
Radojčić, Miloš (Beograd)[more][less]
-
Bertolino, Milorad (Beograd , 1980)[more][less]
URI: http://hdl.handle.net/123456789/5222 Files in this item: 1
DrMiloradBertolino-Upozorenja....pdf ( 3.037Mb ) -
Malbašić, Stefan (Beograd , 2023)[more][less]
URI: http://hdl.handle.net/123456789/5669 Files in this item: 1
v1_masterStefanMalbasic.pdf ( 2.975Mb ) -
Ćosić, Jovana (Beograd , 2016)[more][less]
-
Mićić, Stevan (HEK , 2015)[more][less]
URI: http://hdl.handle.net/123456789/5417 Files in this item: 5
65_UrbanaTransf ... da_StevaMicic_20150519.pdf ( 16.30Mb )Arquitectura-del-futuro.pps ( 4.113Mb )Kad Smo Beograd I Mi Bili Mali.pps ( 3.338Mb )Priobalje Beograda 1930-te.pdf ( 1.381Mb )(more files) -
Govindjee, Sanjay (Zurich , 2007)[more][less]
URI: http://hdl.handle.net/123456789/3013 Files in this item: 1
Useful_definitions_and_concepts.pdf ( 468.3Kb ) -
Antelj, Kaja; Fras Zavrl, Vladimir (Sarajevo , 2010)[more][less]
URI: http://hdl.handle.net/123456789/2025 Files in this item: 1
008%20ANTLEJ%20FRAS%20ZAVRL.pdf ( 336.3Kb ) -
Videnović, I.; Kuraica, M.; Konjević, N. (Obs. Astron. Belgrade , 1995)[more][less]
-
Logan, W. Roger (Detroit , 1995)[more][less]
-
Lajbenšperger, Milica; Šegan, Marija; Rajić, Sanja (Journal of Education Culture and Society , 2013)[more][less]
-
Hill, R. (Pergamon , 1993)[more][less]
-
Guo, W.; Zeng, Q.; Chen, Y. (University of Florida , 2013)[more][less]
URI: http://hdl.handle.net/123456789/3225 Files in this item: 1
RECONSTRUCT_WHITE_MATTER_FIBER.pdf ( 438.0Kb ) -
Danezis, E.; Lyratzi, E.; Antoniou, A.; Popović, L. Č.; Dimitrijević, M. S. (Astronomical Observatory Belgrade , 2008)[more][less]
-
Alatrash, Emhimed Salem (Beograd , 2015)[more][less]
Abstract: Ontologies, often defined as an explicit specification of conceptualization, are necessary for knowledge representation and knowledge exchange. This means that ontology describes concepts and relations that exist in a domain. To enable knowledge exchange, it is necessary to describe these concepts and relations in a better way than just ordering them in taxonomy. A computational ontology consists of a number of different components, such as Concepts, Instances, Individuals or Facts, Relations and Attributes. The present research is intended to consider different software tools related to Semantic web, and achieve a kind of comparison among them. In fact, five ontology-editors are described and compared. They are: Apollo, Onto Studio, Protégé, Swoop and TopBraid Composer Free Edition. The structure and basic features of these editors as well as the way of using them are described. The main criterion used in the process of comparing these editors lies in their convenience for the user, and the possibility to apply them in different kinds of application. The main goal of the work is to introduce a method for ontology construction of a certain domain in applying the Semantic web. A number of software tools adapted to build up the domain ontologies of most wide–spread natural languages are available; however accomplishing that for any given natural language presents a challenge. This research proposes a semi-automatic procedure to create ontologies for different natural languages. The approach utilizes various software tools that are available on the Internet, most notably DODDLE-OWL which is a domain ontology development tool implemented for English and Japanese languages. Through this tool, WordNet, Protégé and XSLT transformations, the researcher proposes a general procedure to construct domain ontology for any natural language. URI: http://hdl.handle.net/123456789/4266 Files in this item: 1
phdEmhimedAlatrash.pdf ( 2.171Mb ) -
Jović, Aleksandar (Beograd , 2021)[more][less]
Abstract: The continuous-time programming problem consists in minimizing an integral functional, with phase constraints of different types. The subject of this doctoral dissertation is to establish extremum conditions as well as duality theorems for a class of convex and smooth continuous-time programming problems, with phase constraints of the inequality type. Unfortunately, some of the results in this field are not valid, which is confirmed in 2019. In this paper, new optimality conditions for the aforementioned class of problems are ob tained. The theorems of weak and strong duality are proved. The main tool for deriving these results is a new theorem of the alternative for a convex system of strict and nonstrict inequal ities in infinite dimensional spaces. In order to apply the aforementioned theorem, a suitable regularity condition must be satisfied. Some optimality conditions are obtained with additional constraint regularity qualification. Theoretical results are confirmed by practical examples. URI: http://hdl.handle.net/123456789/5298 Files in this item: 1
A.Jovic_doktorska_disertacija.pdf ( 1.280Mb ) -
Vicanović, Jelena (Beograd , 2024)[more][less]
Abstract: A convex continuous-time maximization problem is formulated and the nec- essary optimality conditions in the infinite-dimensional case are obtained. As a main tool for obtaining optimal conditions in this dissertation we use the new theorem of the alternative. Since there’s no a differentiability assumption, we perform a linearization of the problem using subdifferentials. It is proved that the multiplier with the objective function won’t be equal to zero. It was also shown that if the linear and non-linear constraints are separated, with additional assumptions it can be guaranteed that the multiplier with non-linear constraints will also be non-zero. In the following, an integral constraint is added to the original convex problem, so that a Lyapunov-type problem, i.e. an isoperimetric problem, is considered. Lin- earization of the problem using subdifferentials proved to be a practical way to ignore the lack of differentiability, so the optimality conditions were derived in a similar way. It is shown that the obtained results will also be valid for the vector case of the isoperimetric problem. Additionally, the optimality conditions for the smooth problem were considered. On the minimization problem, it was shown that the necessary conditions of Karush-Kuhn-Tucker type will be valid with the additional regularity constraint condition. Also, any point that satisfies the mentioned optimality conditions will be a global minimum. URI: http://hdl.handle.net/123456789/5676 Files in this item: 1
J.Vicanovic_doktorska_disertacija.pdf ( 2.198Mb ) -
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 )