ARGO

Automated reasoning group

Argo seminar: najave predavanja

Click here for English version. --- Kliknuti ovde za verziju na engleskom jeziku.

Argo seminar je seminar Argo grupe. Bavi se uglavnom, ali ne isključivo, automatskim rezonovanjem i primenama, teorijskim računarstvom, veštačkom inteligencijom i data-mining-om. Seminar je posvećen uglavnom studentima poslediplomcima. U principu, prvi deo seminara je tutorijalski, u drugom se izlažu istraživački problemi.

Sastanci se održavaju jednom u dve nedelje, uglavnom četvrtkom u 18h u prostorijama Matematičkog fakulteta na Studentskom trgu, ucionica 718.

Sekretar seminara: Vesna Marinković

Ukoliko ste zainteresovani da primate obaveštenja vezana za seminar, molimo Vas da pošaljete e-poruku Vesni Marinković ili Predragu Janičiću .

3.10.2024.

Anna Petiurenko , Pedagogical University of Cracow, Poland
Alphageometry in Practice
Abstract:
Alphageometry is a program designed to solve advanced geometric problems in elementary geometry, such as those from the International Mathematical Olympiad (IMO). We will analyze:
1. The system's language, the types of constructions it employs, and the types of tasks solvable by the program.
2. The gap between the original problem formulation and the version fed into Alphageometry.
3. The gap between textual descriptions and visual outputs.
We will examine the system's ability to introduce auxiliary points and discuss the potential for incorporating this feature into other automated proof systems.

13.2.2023.

Srđan Vesić , CNRS, Francuska
Title: Human argumentation and artificial argumentation: normative, descriptive and prescriptive approach
Abstract:
Argumentation is the model of reasoning based on the construction and evaluation of arguments and identifying relations (attacks, supports) between them. Computational argumentation theory studies argumentative reasoning and formalizes it using tools from mathematics and computer science. In the first part of the talk, we present the rationality principles that were introduced for the argumentation process. We study the links between the principles and show that some sets of principles are incompatible. We overview the existing approaches in the literature and evaluate them formally with respect to the principles.
In the second part of the talk, we study the link between argumentation theory and human reasoning. In particular, we present the results of the cognitive studies that show to what extent humans comply with the principles of the computational argumentation theory. We test our hypothesis that graphical representation positively impacts the degree of compliance. We conclude the talk with a discussion on normative, descriptive, and prescriptive approaches to argument-based reasoning and their link with theory and cognitive studies.

12.3.2020.

Pavle Subotić , Amazon
Title: Rinser: Concise Explanations in Static Analysis Driven Code Reviews
Abstract:
We consider the problem of producing efficiently actionable evidence from a static analyzer. That is, we seek to close the gap between static analyzers and their human users by providing precisely the right evidence that enables users to accept or dismiss potential bugs reported by the analyzer.
In this talk, I present Rinser, a tool used at Amazon to improve the evidence developers receive from static analyzers. Specifically, Rinser provides an on-demand method to check the realdizability of potential bugs reported by the static analyzer Infer. We have developed an initial version of Rinser as a post-analysis automated-reasoning pass based on refutation reasoning. On industrial code bases, our tool is able to surface possible bugs to developers with evidence traces on average 4x steps shorter than standard Infer traces. Foremost, our tool has eased the adaption of static analyzers at Amazon and driven additional dialogue between engineers on the quality of the code. As a bonus, it has also provided a means to soundly remove many trivial false-positive warnings, thereby also reducing the subsequent triaging effort.

13.2.2020.

Aleksandar Zeljić , Stanford University
Title: Marabou Framework for Neural Network Verification
Abstract:
Deep neural networks are revolutionizing the way complex systems are designed. Consequently, there is a pressing need for tools and techniques for network analysis and certification. To help in addressing that need, we present Marabou, a framework for verifying deep neural networks. Marabou is an SMT-style tool that answers queries about a network’s properties by transforming these queries into constraint satisfaction problems. It can accommodate networks with different activation functions and topologies, and it performs high-level reasoning on the network that can curtail the search space and improve performance. It also supports parallel execution to further enhance scalability. We present Marabou, its performance on several classes of benchmarks and discuss ongoing work.

26.12.2019.

Alen Arslanagić, University of Groningen
Naslov: Lightweight Typestate Analysis
Apstrakt:
Typestate is refinement of the concept of a type: they describe which operations are available on an object in a particular program context. They are particularly useful as a type system for OOP languages and APIs. In order to be practical, typestate analysis should happen as soon as possible in the development cycle. However, developing efficient and precise typestate static analysis is a challenging task. Typically, typestate are modelled as general DFA that introduce a complexity in analyzing code in the presence of conditionals and loops. Moreover, the expressivity of a general DFA makes specifying a typestate error-prone and tedious task.
In this work, we focus on typestate analysis in the development time. We introduce restrictions on DFAs that allow us to have a complete lattice and a simple `join` operator on DFA states making analysis scalable and efficient. We provide the annotation-based language for specifying objects behaviour without a need to explicitly reason about DFAs. Our translation guarantees that constructed DFA meets restrictions we impose. We have implemented our approach as a type-checker for Java in Checker framework.
Marija Selaković, Huawei Research
Naslov: Dynamic Analysis and Test Generation for JavaScript
Apstrakt:
JavaScript je postao jedan od najzastupljenijih programskih jezika. Nazalost, svojstva jezika koja su doprinela njegovoj popularnosti cine programe napisane u JavaScriptu podlozne greskama i otezavaju automatske analize koda. Ova svojstva ukljucuju izuzetno dinamicnu prirodu jezika, set neobicnih karakteristika, nedostatak mehanizma enkapsulacije i "no-crash" filozofiju. Cilj ove prezentacije je predstavljanje razlicitih tehnika i alata za dinamicku analizu koda i generisanje testova u svrhu poboljsanja pouzdanosti, ispravnosti, performansi i sigurnosti softvera zasnovanog na JavaScriptu.
Pavle Subotić, Amazon
Naslov: Towards Verification of React Applications
Apstrakt:
React is the most popular front end JavaScript framework in 2019. It integrates the semantics of JavaScript with style sheets and HTML to allow developers to build flexible. powerful dynamic applications. As an increasing number of devices begin to support apps (e.g., smart TVs), developers must ensure that their applications render correctly and efficiently of a large number of configurations and devices. This limits the ability to test at scale and automated reasoning has been suggested to prune test case scenarios. In this talk, I will discuss an upcoming project that aims to leverage the state-of-the-art in automated reasoning to automatically detect slow or incorrectly rendered code on any given device.
Stefan Jakšić, Austrian Institute of Technology
Naslov: Monitoring of Cyber-Physical Systems for Correctness and Robustness
Apstrakt:
In this talk we will provide a brief overview of the recent results in the field of specification-based runtime monitoring of Cyber-Physical Systems (CPS). We show how to automatically obtain monitoring units for CPS, which can not only tell us if the system is operating safely, but also how robust the system is w.r.t. safety requirements. Different kinds of systems require different kinds of robustness quantification - we show a unified framework for robustness monitoring. We will present the challenges in builiding the monitors and highlight their applicability on verifying industrial devices. With the aim to fully highlight the efficiency of our monitors, we evaluate their hardware implementation on several industrial case studies and benchmarks.

23.09.2019.

Srdjan Vesić, CNRS, Francuska
Naslov: Rational Inference Relations from Maximal Consistent Subsets Selection

Apstrakt:
When one wants to draw non-trivial inferences from an inconsistent belief base, a very natural approach is to take advantage of the maximal consistent subsets of the base. But few inference relations from maximal consistent subsets exist. In this paper we point out new inference relations based on selection of some maximal consistent subsets, leading thus to inference relations with a stronger inferential power. The selection process must obey some principles to ensure that it leads to an inference relation which is rational. We define a general class of monotonic selection relations for comparing maximal consistent subsets and show that it corresponds to the class of rational inference relations, defined by Lehmann and Magidor.

27.12.2018.

Petar Vukmirović, Vrije Universiteit Amsterdam
Naslov: Proširivanje dokazivača logike prvog reda na logiku višeg reda

Apstrakt:
Decenije rada su uložene u razvijanje efikasnih računa, struktura podataka, algoritama i heuristika za automatske dokazivače za logiku prvog reda. Dokazivači za logike višeg reda zaostaju u pogledu efikasnosti. Rad koji predstavljam prikazuje implementaciju dokazivača za logiku višeg reda baziranog na vrlo napredom superpozicionom dokazivaču E. Ovaj red objašnjava jedan način na koji se prilagodjavaju strukture podataka, algoritmi i heuristike kako bi se podržala logika višeg reda bez lambda izraza, formalizam koji podržava parcijalnu aplikaciju i primenjene promenljive. Naš pristup pokazuje dve bitne prednosti u odnosu na razvoj dokazivača za logiku višeg reda ispočetka: zadržavamo visoke performanse dokazivača za logiku prvog reda i uspevamo da rešimo i do 15% više problema u odnosu na tradicionalni pristupe zasnovane na prevođenju u logiku prvog reda. Logika višeg reda bez lambda izraza predstavlja prvi korak ka proširenjima na druge logike višeg reda.

11.10.2018.

Pavle Subotic, Amazon
Naslov: Debugging Large Scale Logic Programs

Apstrakt:
Logic programming languages such as Datalog have become popular as Domain Specific Languages (DSLs) for solving large-scale problems, in particular, static program analysis including points-to analysis and network analysis. Logic programs that process large-scale data are, however, difficult to debug. In the database community, data provenance techniques have been proposed that could address the Declarative Debugging Challenge for large-scale inputs. Unfortunately, the current state-of-the-art approaches for data-provenance cannot cope with big data.
In this talk, I discuss a novel provenance evaluation strategy for debugging Datalog programs. The provenance evaluation strategy relies on a new provenance lattice which incorporates proof annotations. We define a new fixed-point semantics for semi-naive evaluation to compute with the augmented lattice, and propose a provenance query mechanism to constructs partial minimal height proofs for tuples.

29.03.2018.

Marc Bezem, Institute for Informatics, University of Bergen, Norway
Naslov: The Univalence Axiom in Dependent Type Theory

Apstrakt:
We give an introduction to the theory with dependent types and inductive equality, and discuss the new Univalence Axiom recently proposed by Voevodsky.

28.12.2017.

Aleksandar Zeljić, Uppsala University
Naslov: A Model-Constructing Approach to Solving Bit-Vector Constraints

Apstrakt:
The Model-Constructing Satisfiability Calculus (mcSAT) is a recently proposed generalization of the DPLL(T) framework for SMT. Unlike most DPLL(T)-based SMT solvers, which carry out conflict-driven learning only on the propositional level, mcSAT calculi can also synthesize new theory literals during learning, resulting in a simple yet very flexible framework for designing efficient decision procedures. In this talk, we present an instantiation of the mcSAT calculus for the theory of fixed-size bit-vectors, based on tailor-made conflict-driven learning that exploits both propositional and arithmetic properties of bit-vector operations. In our approach, bit-vectors are first-order citizens and unnecessary bit-blasting is avoided altogether.

23.03.2017.

Julien Narboux, University of Strasbourg
Naslov: GeoCoq, foundations of geometry formalized in Coq

Apstrakt:
In this talk we will give an overview of the GeoCoq library developed by our team in Strasbourg (http://geocoq.github.io/GeoCoq/ ). GeoCoq library contains a systematic development of geometry from Tarski’s or Hilbert’s axioms. From these axiom systems, we formalized the culminating results of both Tarski, Schwabhäuser, Szmielew, Metamathematische Methoden in der Geometrie and Hilbert, Foundations of Geometry, namely the arithmetization of geometry. This connection between synthetic geometry and algebra, allows us to use algebraic methods for automated deduction in geometry in a synthetic setting. We have also studied the formal proof of the equivalence between 34 versions of the parallel postulates. We work in neutral geometry in an intuitionistic setting and study the impact of different continuity properties on the equivalence proofs. This result in four groups of postulates, which are all equivalent assuming Archimedes’ axiom but distinct, in constructive logic without Archimedes’ axiom. Finally, I will report our ongoing work toward the formalization of Euclid’s Elements proposition in Coq.

22.09.2016.

Tetsuo Ida, University of Tsukuba
Naslov: Computational Origami System Eos

Apstrakt:
I will talk about a computational origami system called Eos (e-origami system) that we have developed over the years. I will cover briefly the motivation, the development process, underlying theories and the functionalities of Eos. During the talk, I would like to emphasize the aspects of Eos as a tool for interactive origami construction, and the geometric theorem prover of origami theorems.
Mircea Marin, West University of Timisoara
Naslov: Solving, Reasoning, and Programming in Common Logic

Apstrakt:
Common Logic (CL) is an ISO standard for exchanging logic-based information in heterogeneous, open networks of computer-based systems. The representational requirements of knowledge in open networks led to some important changes of traditional first-order logic: In CL, symbols (called names) do not have fixed arity (variable polyadicity), the language contains sequence variables that stand for finite sequences of terms, one and the same symbol can play the syntactic roles of both constant, function symbol and predicate (cross-categoricity), terms can be applied to other terms, and the language is type-free. These adaptations pose new challenges to the design and development of reasoning tools for Common Logic. Sharing and reasoning upon knowledge represented in CL require equation solving over terms of this language. We succeeded to identify computationally well-behaved fragments of such solving problems. In this talk, I will present the fragments and solving methods discovered by us, and indicate how they can influence reasoning in CL and transformations of CL expressions.

24.03.2016.

Pavle Subotić, University College London
Naslov: Synthesizing Analyzers from Datalog

Apstrakt:
Among the reasons for the slow industrial adoption of static code analysis is the lack of sufficient customizability and scalability available in tools. Recently, the use of Datalog, has had a resurgence in several computer science communities, particularly, in the area of program analysis where tools such as muZ, LogicBlox and bddbddb have shown great promise. In these tools, Datalog acts as a domain specific language to express custom program analyses concisely, reducing the complexity of developing program analyzers. The drawback, however, is that analyses specified in Datalog typically experience reduced performance compared to manually implemented tools. To close the performance gap, we have developed a tool called /Soufflè/ that overcomes the performance limitations of standard Datalog evaluation by performing an efficient synthesis of Datalog to executable C++ programs. As a result, /Soufflè/ is able to perform analyses on-par with state-of-the-art manual tools (e.g., performs a points-to analysis on OpenJDK in 35 seconds) while retaining the advantages of employing a domain specific language for expressing static analyses. In this talk, I will present an overview of the /Soufflè/ framework, focusing on one of its key optimizations, namely, /Optimal Index Generation/, which it performs to efficiently synthesize Datalog to C++.

07.05.2015.

Marc Bezem, Institute for Informatics, University of Bergen, Norway
Naslov: Coquand's site semantics of coherent logic

Apstrakt:
We introduce so-called site models of coherent theories, due to Coquand. We prove completeness and discuss the status of formulas that are true in the site model of a coherent theory.

30.04.2015.

Bojan Petrović, Haklab Beograd
Naslov: Neformalna verifikacija

Apstrakt:
U periodu između juna 2012. i decembra 2013. u hakerspejsu Haklab Beograd održana je radionica Coq-a prema kursu "Software Foundations" sa Univerziteta u Pensilvaniji. Tematsko jezgro kursa čini proučavanje operacione semantike i tipskih sistema programskih jezika, zajedno sa uvodom u formalno rezonovanje o funkcionalnim i imperativnim programima. Na izlaganju ćemo pružiti pregled kursa "Software Foundations", dati osnovne informacije o Coq interaktivnom dokazivaču teorema, i izneti neka iskustva stečena kroz podučavanje izvan formalno institucionalnog okvira.

22.07.2014.
24.07.2014.

Marc Bezem, Institute for Informatics, University of Bergen, Norway
Naslov: Homotopy Type Theory

Apstrakt:
Homotopy type theory is a new branch of mathematics that combines aspects of several different fields in a surprising way. It is based on a recently discovered connection between homotopy theory and type theory. Homotopy theory is an outgrowth of algebraic topology and homological algebra, with relationships to higher category theory; while type theory is a branch of mathematical logic and theoretical computer science. Homotopy type theory also brings new ideas into the very foundation of mathematics. For example, there is Voevodsky's subtle and beautiful Univalence Axiom. The univalence axiom implies, in particular, that isomorphic structures can be identified, a principle that mathematicians have been happily using on workdays, despite its incompatibility with the "official" doctrines of conventional foundations. In the seminar we will focus on type theory for formalizing mathematics and work through (parts of) the HoTT book, freely available from: http://uf-ias-2012.wikispaces.com/The+book

02.07.2014.

Sana Stojanović, Matematički fakultet, Univerzitet u Beogradu
Naslov: Automatsko generisanje masinski proverivih i citljivih dokaza i dijalekt koherentne logike

Apstrakt:
U ovom izlaganju ce biti predstavljeno automatsko generisanje dokaza iz dela knjige Tarskog "Metamathematische Methoden in der Geometrie" uz pomoc rezolucijskih dokazivaca teorema i koherentnog dokazivaca teorema. Nakon toga cemo predstaviti format dokaza koji smo koristili koji nam omogucava da u okviru koherentne logike dobijemo dokaze na jezicima razlicitih dokazivaca teorema (Isar i Coq).
Mirko Stojadinović, Matematički fakultet, Univerzitet u Beogradu
Naslov: Odabir CSP rešavača zasnovan na treniranju sa kratkim vremenskim ograničenjem.

Apstrakt:
Postoje mnoge različite metode za rešavanje problema zadovoljenja ograničenja (Constraint Satisfaction Problems - CSP) kao i srodne optimizacione verzije ovog problema. Međutim, ne postoji metoda (ili rešavač zasnovan na nekoj metodi) koja je efikasna u rešavanju svih tipova CSP problema. Razvijeni su mnogi pristupi za odabir pogodnog rešavača iz skupa rešavača koji su na raspolaganju (tzv. portfelj pristupi) pri čemu se odabir vrši na osnovu jednostavnih sintaksnih karakteristika ulazne CSP instance. ArgoCSPkNN je jedan od tih pristupa i zasnovan je na metodi k najbližih suseda. Za razliku od drugih portfelj pristupa, ovaj pristup koristi treniranje sa vrlo kratkim vremenskim ograničenjim za rešavače. Eksperimentalni rezultati potvrđuju da je ovaj portfelj pristup vrlo efikasan i da koristi značajno kraće vreme treniranja od uobičajenih portfelj pristupa.
Naslov: Pravljenje rasporeda smena za kontrolore letenja svođenjem na CSP, SAT i probleme zasnovane na SAT problemu.

Apstrakt:
Pravljenje rasporeda smena za kontrolore letenja je problem koji se spominje u literaturi ali do sada nije formalno opisan. Daćemo formalnu definiciju i predstaviti tri kodiranja ovog problema. Kodiranja omogućavaju zadavanje vrlo raznovrsnog skupa ograničenja. Problem se rešava korišćenjem SAT, MaxSAT, PB, SMT, CSP i ILP rešavača. U kombinaciji sa ovim rešavačima, prezentujemo i tri optimizacione tehnike: osnovnu i dve modifikacije osnovne. Modifikacije koriste lokalnu pretragu da unaprede neke delove pronađenog rešenja. Rezultati pokazuju da su pristupi za rešavanje SAT problema i njemu sličnih problema pogodniji od ostalih pristupa, kao i da jedna od tehnika koja koristi lokalnu pretragu značajno poboljšava performanse osnovne tehnike. Raspored za aerodrom u Vršcu je pravljen korišćenjem ovih tehnika.

13.03.2014.

Aleksandar Zeljic, Department of Information Technology, Uppsala University, Sweden
Naslov: Approximations for Model Construction

Apstrakt:
We consider the problem of efficiently computing models for satisfiable constraints, in the presence of complex background theories such as floating-point arithmetic (FPA). Model construction has various applications, for instance the automatic generation of test inputs. It is well-known that naive encoding of constraints into simpler theories (for instance, bit-vectors or propositional logic) can lead to a drastic increase in size, and be unsatisfactory in terms of memory and runtime needed for model construction. We define a framework for systematic application of approximations in order to speed up model construction. Our method is more general than previous techniques in the sense that approximations that are neither under- nor over-approximations (or the combination of both) can be used, and shows promising results in practice.

12.12.2013.

Pascal Schreck, University of Strasbourg, France
Naslov: Combinatorial approaches in incidence projective geometry

Apstrakt:
When dealing with robustness issues in geometric constraint solving, one has to take degenerated cases into account. Such cases appear when occurrences of geometric theorems appear and, particularly, theorems in incidence geometry. In this talk, I will present the framework of synthetic projective incidence geometry, the main theorems/properties of this domain and how they can be used to detect degenerated cases and to make combinatorial proofs of the subtended theorems.
Pierre Boutry, Julien Narboux, Pascal Schreck, University of Strasbourg, France
Naslov: Semi-interactive proofs within Tarski's geometry

Apstrakt:
We will present our current work and project about formalization of high-school geometry. After presenting Tarski's axiom system, we will give an overview of some decidability results in this context. Based on some well known examples, we will highlight some differences between a proof given to highschool students and its formalization within the Coq proof assistant. This analyse will help us to determine our next goals.

28.11.2013.

Pavle Subotic, Department of Information Technology, Uppsala University, Sweden
Naslov: Guiding Craig Interpolation with Domain-specific Abstractions

Apstrakt:
Craig Interpolation is a standard method to construct and refine abstractions in model checking. To obtain abstractions that are suitable for the verification of a software programs or hardware designs, model checkers rely on theorem provers to find the right interpolants, or interpolants containing the right predicates, in a generally infinite lattice of interpolants for any given interpolation problem. The problem of guiding solvers to the right interpolants has so far been investigated mainly on a syntactic level. In this talk we present a semantic and solver-independent framework for systematically exploring interpolant lattices, based on the notion of interpolation abstraction. We discuss interpolation abstractions, how they can be constructed, and how they can be used in the context of software model checking.

18.09.2013.

Gabriel Istrate, West University of Timisoara and e-Austria Research Institute Timisoara, Romania
Naslov: Phase Transitions in Random Constraint Satisfaction Problems: A Personal Perspective

Apstrakt:
Phase transitions in combinatorial optimization are an approach to the analysis of combinatorial optimization problems that has evolved into an interdisciplinary area, at the crossroads of Statistical Physics, Theoretical Computer Science and Artificial Intelligence. Methods from Statistical Physics have led to spectacular advances in the area of satisfiability solving. They have also provided intuition for the rigorous analysis of random instances of combinatorial optimization problems. In this talk I will present an introduction to this research direction, with a special emphasis on my research interests in this area. Some of the topics I will deal with include: 1. Classification of thresholds and rigorous results on the location of phase transitions in random CSP. 2. The connection between first-order phase transitions and exponential bounds for resolution. 3. The geometric structure of solution space of random CSP.

16.05.2013.

Alan Bundy, School of Informatics, University of Edinburgh, UK
Naslov: The Interaction of Representation and Reasoning (part I)

Naslov: The Interaction of Representation and Reasoning (part II)

13.12.2012.

Pascal Schreck, University of Strasbourg, France
Naslov: RC-(un)constructibility, proofs and constructions
Apstrakt:
Lebesgue's method is often presented as the method to prove RC-constructibility and unconstructibility. Actually, one of the key ingredient of the whole method is the triangularization of the algebraic system corresponding to the problem to be solved. It is interesting to note that triangularization methods are also key components of the algebraic technics used in proof in geometry. In this talk, I present both methods: Ritt-Wu's principle for decomposition/triangularization and Lebesgue's method for solving irreducuble polynomials using square radicals. I also present some examples of RC-constructibility and unconstructiblity.
Julien Narboux, University of Strasbourg, France
Naslov: Tarski's and Hilbert's geometry

20.09.2012.

Tihomir Gvero , Ecole Polytechnique Federale de Lausanne (EPFL)
Naslov: Fast Code Completion using Type Inhabitation
Apstrakt:
Developing modern software applications typically involves composing functionality from existing libraries. This task is difficult because libraries may expose many methods to the developer. To help developers in such scenarios, we present a technique that synthesizes and suggests valid expressions of a given type at a given program point. As the basis of our technique we use type reconstruction for lambda calculus with subtyping. We show that the inhabitation problem in the presence of subtyping remains PSPACE-complete. We introduce a succinct representation for type judgements that merges types into equivalence classes to reduce the search space. We implemented the resulting algorithm and deployed it as a plugin for the Eclipse IDE for Scala.

01.08.2012.

Marc Bezem , Department of Informatics, University of Bergen
Naslov: Automating Coherent Logic: an overview

29.12.2011.

Vesna Marinković , Matematički fakultet, Univerzitet u Beogradu
Naslov: Prikaz rada "Automatsko generisanje koraka u geometrijskim konstrukcijama" autora Chou, Gao, Zhang
Apstrakt:
U ovom izlaganju biće prikazan opis sistem za rešavanje geometrijskih ograničenja koji kao ulaz prihvata deklarativni opis geometrijskog crteža a kao izlaz vraća proceduru kako nacrtati sliku korišćenjem lenjira i šestara. Metod pokušava da odredi položaj geometrijskog objekta na osnovu skupa geometrijskih objekata čiji je položaj već poznat. Pritom se ne koriste samo ograničenja koja uključuju dati objekat, već i implicitne informacije izvedene na osnovu drugih objekata.
Novak Novaković, Matematički institut, Beograd
Naslov: Algebarska semantika dokaza i resursa u klasičnoj logici
Apstrakt:
Programi u cisto funkcionalnom programskom jeziku / lambda termi u lamda racunu se korespodencijom Karija i Hauarda dovode u vezu sa formalnim dokazima u (intuicionistickoj) logici. Opsta teorija dokaza je disciplina matematicke logike koja se bavi proucavanjem upravo tih formalnih dokaza kao formalnih matematickih objekata. Premda je pojam formalnog dokaza dobro definisan, gotovo ceo vek razvoja ove discipline i dalje nije pruzio odgovor na centralno otvoreno pitanje opste teorije dokaza -- kada su dva data dokaza u klasicnoj logici jednaka? Glavni deo predavanja demonstrira nedavne rezultate koji proizilaze iz algebarskog tretmana problema, i konkretno, vezu pojma Frobenijusovih algebri sa pitanjem jednakosti dokaza u klasicnoj logici. Frobeniusove algebre su u novije vreme intenzivno izucavane u matematickoj fizici zbog njihove veze sa topoloskim kvantnim teorijama polja. U logici, ove algebarske strukture vode ka novom pristupu standardnim pitanjima teorije dokaza i ka formulaciji pojma resursa za sisteme Gencenovog tipa za klasicnu logiku. Materija koja ce biti prikazana predstavlja deo doktorske disertacije odbranjene u novembru na institutu INRIA u Nansiju u Francuskoj.

08.12.2011.

Milena Vujošević - Janičić , Matematički fakultet, Univerzitet u Beogradu
Naslov: LAV: Sistem za automatsko pronalazenje gresaka u softveru
Apstrakt:
U okviru izlaganja bice prikazan LAV, alat za staticko pronalazenje gresaka i verifikaciju programa pisanih u programskom jeziku C. LAV koristi popularnu LLVM infrastrukturu za prevodjenje i analizu programa, pa se moze koristiti za analizu programa pisanih i u drugim programskim jezicima. LAV koristi simbolicko izracunavanje za konstruisanje formule logike prvog reda koja modeluje ponasanje programa na nivou osnovnih blokova. Veze izmedju blokova LAV modeluje koristeci iskazne promenljive. LAV implementira dva prisutpa razmotavanju petlji, aproksimaciju petlji fiksnim brojem razmotavanja kao sto je to u bounded model checking-u, ali i aproksimaciju petlji sa proizvoljnim brojem razmotavanja. Generisane uslove ispravnosti LAV salje na proveru jednom od nekoliko SMT solvera za koje ima podrsku: Boolector, MathSAT, Yices i Z3. Takodje, bice prikazani eksperimentalni rezultati poredjenja LAVa sa srodnim alatima, kao i rezultati primene LAVa u obrazovanju.
Mladen Nikolić, Matematički fakultet, Univerzitet u Beogradu
Naslov: Mapping efficiency and information content
Apstrakt:
The measures of quality of automatically generated maps do not take cost of the map production in the appropriate way. Especially not the cost of information content of maps. In this talks we discuss how these problems can be resolved. We especially focus at the measure of information content inspired by the results from algorithmic information theory. The problems in their construction are particularly interesting.

24.11.2011.

Ivan Petrović , Matematički fakultet, Univerzitet u Beogradu
Naslov: Implementacija Wu-ove metode za automatsko dokazivanje geometrijskih teorema u okviru OpenGeoProver dokazivaca
Apstrakt:
Wu-ova metoda je jedna od najefikasnijih metoda automatskog dokazivanja geometrijskih teorema. Implementacije pojedinih algoritama (poput triangulacije sistema polinoma ili izracunavanja pseudo-kolicnika dva polinoma) su veoma osetljive - potrebno ih je pazljivo uraditi kako bi se od Wu-ove metode dobili najbolji rezultati. Bice predstavljene ideje preuzete iz postojece C++ implementacije kao i novine u Java implementaciji dokazivaca. Nacinice se poseban osvrt na metode prevodjenja ulaznog geometrijskog problema na algebarsku formu i izazove na koje se naislo. Opisace se ukratko kako su NDG uslovi prevedeni na citljiv oblik. Prikazace se neki primeri dokazivanja teorema. Na kraju ce biti opisani dalji koraci u razvoju: integracija u GeoGebra sistem za interaktivnu geometriju, rad na paralelnim algoritmima, integracija sa Isabelle dokazivacem, razmatranje problema sa konusnim presecima i teorema koje su posledice aksioma rasporeda (implementacijom prosirenja osnovne Wu-ove metode), implementacija razlicitih heuristika za instanciranje tacaka i uopste biranje najboljeg puta za izvodjenje dokaza teorema, ideje za primenu Wu-ove metode u nekom modelu hiperbolicke geometrije itd.
Danijela Petrović, Filip Marić, Matematički fakultet, Univerzitet u Beogradu
Naslov: Formalna verifikacija algoritma svodjenja geometrijskih tvrdjenja na algebru
Apstrakt:
Najefikasniji automatski dokazivaci teorema u geometriji zasnovani su na algebarskim metodama. U okviru predavanja bice prikazani prvi koraci projekta koji za krajnji cilj ima formalno dokazivanje veze izmedju algebarskih metoda i sinteticke geometrije. Prvi korak primene algebarskih metoda je svodjenje geometrijskog problema koje se resava na algebru (tj. na sistem polinomijalnih jednacina). Algoritam svodjenja je implementiran u okviru interaktivnog dokazivaca Isabelle/HOL i formalno je pokazana njegova veza sa analitickom geometrijom.

03.11.2011.

Tijana Šukilović, Matematički fakultet, Univerzitet u Beogradu
Naslov: Detekcija krugova korišćenjem diskretne krivine
Apstrakt:
Definišemo pojam diskretne krivine vezane za crni piksel crno-belih raster slika. Oblasti primene uključuju detekciju proizvoljnih oblika, specijalno onih koji se sastoje od deo po deo glatkih krivih. Koristeći pristup diskretne krivine, opisujemo i implementiramo algoritam za detekciju krugova i lukova i uporedjujemo ga sa postojećim metodama.
Predrag Janičić, Matematički fakultet, Univerzitet u Beogradu
Naslov: Automatsko rezonovanje: neki uspesi i novi izazovi
Apstrakt:
U predavanju će biti dat kratak pregled nekih oblasti automatskog rezonovanja. Biće dat kratak istorijski razvoj, pomenuti neki od najznačajnijih rezultata i trenutnih izazova.
Isti materijal bio je izložen u okviru predavanja po pozivu na konferenciji CECIIS 2011.

29.06.2011.

Predrag Janičić, Matematički fakultet, Univerzitet u Beogradu
Naslov: Prikaz posete univerzitetu EPFL i ucesca na konferenciji SuRI
Apstrakt:
Bice ukratko opisane poseta grupi LARA (Lab for Automated Reasoning and Analysis) i ucesce na konferenciji SUmmer Research Institute (SURI), na EPFL (Lausanne, Switzerland).
Filip Marić, Matematički fakultet, Univerzitet u Beogradu
Naslov: Prikaz ucesca na "SAT/SMT Summer School"
Mladen Nikolić, Matematički fakultet, Univerzitet u Beogradu
Naslov: Odnos nekih pojmova mašinskog učenja i filozofije nauke
Apstrakt:
Pojam generalizacije je centralni pojam kako masinskog ucenja, tako i empirijskih nauka. Iako je u tim oblastima proucavan odvojeno, postoje zanimljive veze kako izmedju koncepata koji se koriste u ovim poljima, tako i izmedju zakljucaka do kojih se u njima doslo. Posebno je zanimljiva veza izmedju pojmova VC dimenzije i strukturalne minimizacije rizika s jedne strane i porecivosti (falsifiability) po Poperu i Okamove ostrice sa druge.

29.12.2010.

Aleksandar Zeljić, Matematički fakultet, Univerzitet u Beogradu
Naslov: Svodjenje problema SAT na problem klike i obratno
Apstrakt:
U ovom izlaganju ce biti predstavljeno svodjenje problema SAT na problem klike, kao i nekoliko nacina za svodjenje problema klike na problem SAT. Ukratko ce biti predstavljena i mera za poredjenje svodjenja na problem SAT.
Vesna Pavlović, Matematički fakultet, Univerzitet u Beogradu
Naslov: Resavanje konstruktivnih zadataka u geometriji
Apstrakt:
U ovom izlaganju ce biti ukratko izlozen tekuci rad na resavanju konstruktivnih zadataka u geometriji. Metod koji se koristi zasniva se na kombinaciji ulancavanja unapred i unazad, i ima kontrolu dubina.

15.12.2010.

Nikola Jelić, Matematički fakultet, Univerzitet u Beogradu
Naslov: Kombinovanje analitickih i induktivnih metoda masinskog ucenja
Apstrakt:
Oblast mašinskog učenja je zaživela praktično sa pojavom prvih elektronskih računara. Čim je ukazana moć mašine da izvršava složena izračunavanja, postavilo se razumno pitanje do kojeg stepena je moguće osposobiti računar ne samo da obrađuje podatke, već i da uči pravilnosti iz njih.
Pitanje mogućnosti mašine da uči, i time pomogne, a kasnije i odmeni čoveka na zadacima sve veće složenosti, ne pripada samo teoretskom računarstvu. Oponašanje opažajno-saznajnog procesa koji je svakodnevni fenomen kod živih bića ima velikog značaja za biologiju, psihologiju, medicinu, a oblast mašinskog učenja pozajmljuje ideje i koncepte iz tih i mnogih drugih oblasti da bi što potpunije i valjanije opisala različite pristupe problematici.
Dva dominantna pristupa su se izdvojila tokom godina: induktivni, zasnovani na statistici i drugim aproksimativnim metodama, i analitički, zasnovani na matematičkoj logici i dedukciji. Upravo su teorijski temelji ovih pristupa usmerili i ograničili upotrebu metoda mašinskog učenja. Induktivne metode krasi otpornost na greške u podacima za trening, mala potreba za predznanjem o problemu, kao i moć da razumno dobro aproksimiraju rešenje problema koji nema jednoznačno optimalno rešenje. S druge strane, analitički metodi su u stanju da daju rešenje koje se savršeno uklapa u teorijski okvir, ukoliko je predznanje savršeno i pravila izvođenja neprotivrečna.
U praksi se pokazalo da mnogi problemi ne spadaju striktno u samo jednu od ove dve grupe, već dele neka svojstva sa obe. Shodno tome, pojavila se potreba za metodama mašinskog učenja koje bi bile u stanju da integrišu oba pristupa, kao i da na taj način ublaže slabosti i istaknu prednosti obe metodologije.
Kombinovani metodi mašinskog učenja su u praksi pokazali da dolaze do boljih rešenja za manje vremena od čisto intuitivnih ili čisto analitičkih metoda, kao i da razumno dobro kompenzuju manjkavosti ta dva pristupa.
Mladen Nikolić , Matematički fakultet, Univerzitet u Beogradu
Naslov: Izvestaj o poseti grupi LARA
Apstrakt:
U ovom izlaganju bice ukratko prikazan rad clanova grupe LARA (Laboratory for Automated Reasoning and Analysis) sa univerziteta EPFL, kao i potencijalne ideje za saradnju i utisci nastali prilikom posete toj grupi.

24.11.2010.

Danijela Petrović, Matematički fakultet, Univerzitet u Beogradu
Naslov: Grebnerove baze
Apstrakt:
Na pocetku predavanja bice ukratko izlozeni osnovni pojmovi o prezapisivanju termova. Potom se razmatra problem pripadnosti polinoma idealu generisanim nad nekim skupom polinoma. Pokazuje se da se ovaj problem moze efikasno resiti koriscenjem Grebnerove baze datog skupa polinoma. U izlaganju bice predstavljen algoritam na koji se moze od datog skupa polinoma generisati Grebnerova baza. Na kraju predavanja bice izlozen primer primene Grebnerovih baza u geometriji.
Filip Marić, Matematički fakultet, Univerzitet u Beogradu
Naslov: Verifikovana efikasna provera dokaza nezadovoljivosti za SAT
Apstrakt:
Kako bi se mogli koristiti u praksi, SAT resavaci moraju biti pouzdani. Jedan od uobicajenih nacina postizanja pouzdanosti je prosirenje SAT resavaca mogucnoscu generisanja modela u slucaju zadovoljivih i dokaza u slucaju nezadovoljivih formula i naknadno proveravanje ovih objekata koriscenjem nezavisnih alata. Uobicajeni format dokaza nezadovoljivosti cine rezolucioni dokazi i oni se mogu proveriti relativno jednostavnim alatima, medjutim obicno zauzimaju veliki prostor i nije uvek jednostavno modifikovati SAT resavace tako da generisu ovakve dokaze. Alternativni format dokaza cine tzv. klauzalni dokazi koji su obicno znatno manji i koji se veoma jednostavno mogu eksportovati iz vecine SAT resavaca, medjutim alati koji bi ovakve dokaze efikasno mogli proveravali obicno nisu jednostavni i postavlja se pitanje njihove pouzdanosti. U ovom radu se predstavlja alat za proveru klauzalnih dokaza implementiran i verifikovan u okviru sistema Isabelle/HOL koji po preliminarnim eksperimentima daje postize zadovoljavajucu efikasnost.

10.11.2010.

Vesna Pavlović, Matematički fakultet, Univerzitet u Beogradu
Naslov: Izveštaj o učešću članova ARGO grupe na ADG konferenciji
Apstrakt:
U izlaganju će biti ukratko izloženi naši utisci sa učešća na ADG konferenciji koja je održana u Minhenu jula ove godine. ADG konferencija je vodeća konferencija iz oblasti automatskog rezonovanja u geometriji i održava se jednom u dve godine.
Milan Banković, Matematički fakultet, Univerzitet u Beogradu
Naslov: Izveštaj o učešću članova ARGO grupe na ovogodisnjem FLoC-u
Apstrakt:
Federated Logic Conference (FLoC) je jedan od najvecih i najznacajnijih naucnih skupova posvecen matematickoj logici kao i njenoj povezanosti sa racunarstvom. Ovaj skup se odrzava svake cetvrte godine i okuplja na jednom mestu nekoliko veoma znacajnih konferencija iz oblasti matematicke logike u racunarstvu, kao i veliki broj pridruzenih radionica. Ove godine FLoC je odrzan u Edinburgu. Ovo predavanje predstavlja kratak izvestaj o ucescu clanova ARGO grupe na ovogodisnjem FLoC-u.
Mladen Nikolić, Matematički fakultet, Univerzitet u Beogradu
Naslov: Merenje sličnosti grafova i njihovih čvorova uparivanjem suseda
Apstrakt:
Problem merenja sličnosti grafova i njihovih čvorova je važan u različitim praktičnim primenama. Postoji više predloženih mera zasnovnih na iterativnom računanju sličnosti i na principu da su dva čvora slična onoliko koliko su slični njihovi susedi. U ovom izlaganju biće opisan jedan nov metod te vrste zasnovan na profinjenom konceptu sličnosti čvorova koji uključuje uparivanje njihovih suseda. Za predloženi metod, pokazana je konvergencija, kao i da ima odredjena poželjna svojstva koja postojeći metodi nemaju. Metod je ilustrovan na dva praktična problema, pri čemu se poredi sa postojećim metodima.

23.06.2010.

Ivana Tanasijević, Matematički fakultet, Univerzitet u Beogradu
Naslov: Primene prostornog rezonovanja
Apstrakt:
U izlaganju ce biti reci o prostornom rezonovanju sa gledista njegove prakticne primenljivosti. Kroz nekoliko primera ce biti ilustrovano kako se moze prepoznati prostorni aspekt u nekim zadacima i upotrebiti prostorno rezonovanje za njihovo resavanje.
Mladen Nikolić, Matematički fakultet, Univerzitet u Beogradu
Naslov: Laicki uvod u algoritamsku teoriju informacija
Apstrakt:
U ovom izlaganju ce biti opisani osnovni pojmovi algoritamske teorije informacija kao sto su Kolmogorovljeva slozenost, slucajne niske, broj Omega, kao i njihov znacaj za razmatranje nepotpunosti aksiomatskih sistema.

21.05.2010.

Florian Haftmann, Fakultät für Informatik, TU München, Filip Marić, Matematički fakultet, Univerzitet u Beogradu
Naslov: Towards a verified parallel SAT solver
Apstrakt:
We present work in progress, which combines two milestones involving code generation from Isabelle/HOL:
a) data refinement
Data refinement, i.e. the replacement of data structures by other (more efficient) ones, is a central task in program development. We show how this acticity will be supported by Isabelle/HOL and its code generator with only a minimal extension of the trusted code base.
b) parallelizing in functional programming languages
The ancient continuous speedup of ever newer CPUs has come to an end -- to take advantage of progress in hardware design, programs must exploit parallization. We take a bluffer's glance how this has been undertaken in Isabelle/HOL, casting a light how parallelizing can work out in functional programming languages in general.

12.05.2010.

Predrag Janičić, Matematički fakultet, Univerzitet u Beogradu
Naslov: Neke novosti iz oblasti geometrijskog rezonovanja i dinamicke geometrije
Apstrakt:
U izlaganju ce biti reci o nekim aktivnostima u vezi sa geometrijskim rezonovanjem i dinamickom geometrijom: o konferencijama CADGME (Hagenberg, juli 2009) i AD+GG (Castro Urdiales, februar 2010), kao i o clanku "The Area Method - A Recapitulation" o metodi povrsina (autori: Janicic, Narboux, Quaresma).
Danijela Petrović, Matematički fakultet, Univerzitet u Beogradu
Naslov: Uvod u formalno dokazivanje teorema
Apstrakt:
U ovom izlaganju bice prikazan Isabelle, programski jezik osmisljen za lakse pisanje i dokazivanje definicija, teorema, lema, pomocu kompjutera. Na pocetku predavanja bice objasnjeni osnovni pojmovi. Zatim ce biti pokazani primeri dokazivanja teorema iz matematicke logike. Dokazi ce biti pisani u Isar-u, prosirenju Isabelle takvo da su dokazi citljiviji.

14.04.2010.

Milan Banković, Matematički fakultet, Univerzitet u Beogradu
Naslov: SMT tutorijal
Apstrakt:
Problem zadovoljivosti u teoriji (SMT) je problem odlučivanja da li za datu formulu A prvog reda postoji model date teorije T takav da zadovoljava formulu A. Rešavanje SMT problema za različite teorije nalazi primenu u mnogim oblastima od verifikacije softvera i hardvera, preko problema rasporedjivanja do raznih optimizacionih problema. U ovom izlaganju biće dat opšti pregled SMT problema i njihovog resavanja. Najpre će biti dat kratak teorijski uvod. Zatim će biti diskutovane neke teorije prvog reda koje se često javljaju u SMT rešavanju. Biće izloženi principi rada modernih SMT rešavaca i njihova veza sa SAT rešavanjem. Na kraju će biti dat kratak osvrt na dosadašnji, tekući i budući rad Argo grupe u oblasti SMT resavača.
Mladen Nikolić, Matematički fakultet, Univerzitet u Beogradu
Naslov: Neki detalji primenjene statistike
Apstrakt:
U ovom izlaganju, biće diskutovani pojmovi kao sto su p-vrednost i veličina efekta pri statističkom testiranju hipoteza, kao i njihova uloga u praksi. Biće prikazano nekoliko mera veličine efekta zasnovanih na korelaciji. Takodje ce biti diskutovana razlika izmedju frekventističkog i Bajesovskog pristupa verovatnoći i statistici.

31.03.2010.

Djordje Stakić, Matematički fakultet, Univerzitet u Beogradu
Naslov: Mašinsko učenje zasnovano na instancama
Apstrakt:
U izlaganju će biti predstavljeni metodi mašinskog učenja zasnovanog na instancama. Ovi metodi ne formiraju hipotezu unapred samo na osnovu trening primera, nego tek kada dobiju upitnu instancu na osnovu trening primera vrše njenu klasifikaciju. Značajniji predstavnici ovih metoda su metod k najbližih suseda, lokalna linearna regresija pomocu težina, radijalne baze funkcija i rezonovanje po slučajevima.
Predrag Janičić, Sana Stojanović, Vesna Pavlović, Mladen Nikolić, Matematički fakultet, Univerzitet u Beogradu
Naslov: Ideje o razvoju novog dokazivača teorema za koherentnu logiku
Apstrakt:
U izlaganju će biti ukratko opisani postojeći dokazivači teorema za koherentnu logiku - fragment logike prvog reda u kome se mogu izraziti različite značajne teorije. Jedna varijanta dokazivača je već razvijena u okviru ARGO grupe i testirana na teoremama iz oblasti geometrije. On se zasniva na pristupu koji se naziva 'forward chaining' i koji predstavlja dobru osnovu za generisanje čitljivih dokaza. Ipak, ovaj pristup nije dovoljno moćan za dokazivanje teških teorema. Biće diskutovano kako se pomenuti pristup može proširiti tehnikama iz drugih domena (npr. iz SAT rešavanja) koje bi mogle da značajno ubrzaju pretragu i kako se te tehnike mogu prilagoditi dokazivanju u koherentnoj logici.

30.12.2009.

Mladen Nikolić, Matematički fakultet, Univerzitet u Beogradu
Naslov: Metodologija poredjenja SAT rešavača
Apstrakt:
Odmeravanje poboljsanja modernih SAT rešavača, ili poredjenje dva proizvoljna rešavača je težak, ali važan zadatak. Rešavači se obično porede njihovim izvršavanjem na nekom skupu iskaznih formula i poredjenjem broja rešenih formula ili njihovih vremena izvršavanja na neki jednostavan način. Biće izložena nova, statistički zasnovana, metodologija njihovog poredjenja.
Mirko Stojadinović, Matematički fakultet, Univerzitet u Beogradu
Naslov: Kvalitetan istraživački rad, objavljivanje radova u časopisima i sposobnost dobrog organizovanja
Apstrakt:
U izlaganju će biti ukratko izloženi ključni problemi pri istraživanju, pisanju i objavljivanju radova, veštine prezentovanja i dobre organizacije, kao i način pisanja predloga za projekte. Biće napravljena i kratka paralela između mentorstva i post-diplomskih studija u Srbiji i Velikoj Britaniji. O svemu tome sam slušao na predavnjima organizovanim pri Ministarstvu za Nauku i Tehnološki razvoj koje je držao profesor Stiv Kvori (Steve Quarrie). Profesor Kvori ima dugogodišnje iskustvo u pisanju i objavljivanju radova, a radi i kao recenzent u više međunarodnih časopisa.

16.12.2009.

Bojan Marinković, Matematički institut SANU
Naslov: Gostovanje u okviru DEUKS projekta: O povezivanju heterogenih "overlay" mreža
Apstrakt:
Od 27. februara do 25. maja ove godine boravio sam u Sofii Antipolis u Francuskoj. Tokom ovog perioda radio sam u sastavu LogNet tima istraživačkog centra INRIA Sofia Antipolis - Mediteran, a pod mentorstvom profesora Luiđija Likvorija, šefa tima. Ovo je bila prilika da uđem u, za mene, novu oblast istraživanja - distribuirani sistemi. Glavni cilj mog rada je bila implementacija softvera prema algoritmu opisanom u radu "L. Liquori, C. Tedeschi, and F. Bongiovanni: BabelChord: a Social Tower of DHT-Based Overlay Networks. In 14th Symposium on Computers and Communications (ISCC 2009). IEEE, 2009. Short paper." Tokom ovog izlaganja biće izloženi osnovni koncetpi "overlay" mreža, distribuiranih sistema, kao i "chord" i "babelchord" protokola.
Aljoša Obuljen, Matematički fakultet, Univerzitet u Beogradu
Naslov: Metoda za poravnanje na nivou reči zasnovana na dvojezičnom korpusu poravnatom na nivou rečenice
Apstrakt:
Automatsko poravnanje na nivou reči je jedan od ključnih problema u statističkom pristupu mašinskom prevođenju. Razni metodi su do sada predlagani, sa različitim rezultatima. U ovom radu, predlažemo jednostavnu metodu rangiranja sa primenom na poravnanje na nivou reči, ako je dat dvojezički korpus poravnat na nivou rečenice. Ova metoda se takođe može primeniti i na korpuse poravnate na drugim nivoima, kao što je nivo pasusa ili čak većeg segmenta teksta, ako je količina poravnatog teksta dovoljno velika. Drugim rečima, metoda je robustna u odnosu na granularnost poravnanja. Za potrebe ovog rada, poravnanje na nivou rečenice je odabrano, kao standardno poravnanje u statističkom mašinskom prevođenju. Dvojezični korpus umerene veličine (oko 1M reči/tokena po jeziku) je korišćen radi dobijanja rezultata - poravnat srpsko-engleski korpus tekstova vezanih za obrazovanje, ekonomiju, zdravstvo i zakonodavstvo (SELFEH - Serbian-English Law Finance Education and Health), jedan od brojnih resursa razvijenih u okviru HLT grupe pri Univerzitetu u Beogradu.

18.11.2009.

Vesna Pavlović, Matematički fakultet, Univerzitet u Beogradu
Naslov: Izveštaj o boravku na Politehničkom univerzitetu u Valensiji
Apstrakt:
U okviru Tempus DEUKS projekta u periodu od 01.05 do 28.07. boravila sam na Politehničkom Univerzitetu u Valensiji, Španija, kao gostujući istraživač. Glavna tema mog rada bila je automatsko generisanje linearnih elementarnih interpretacija za dokazivanje zaustavljanja datog sistema za prezapisivanje termova. Na ovom predavanju biće ukratko izložene osnove sistema za prezapisivanje termova, metode koje se koriste za dokazivanje njihovog zaustavljanja, sa osvrtom na konkretan problem na kome sam radila.
Ivana Tanasijević, Matematički fakultet, Univerzitet u Beogradu
Naslov: Predstavljanje prostora i prostorno rezonovanje
Apstrakt:
Potreba za prostornom reprezentacijom i rezonovanjem je zauzela posebno mesto u mnogim sferama Vestačke inteligencije. U ovom izlaganju je dat pregled osnovnih pojmova, pri čemu je naglasak na kvalitativnoj reprezentaciji i problemima prostornog rezonovanja. Kako se ovi problemi mogu svesti na problem konzistentnosti, to će ovde biti reči o pristupu tom konkretnom problemu.

4.11.2009.

Filip Marić, Matematički fakultet, Univerzitet u Beogradu
Naslov: Izveštaj o učešću na konferencijama SAT2009 i TPHOLs2009
Apstrakt:
U izlaganju će biti prikazani najznačajniji utisci sa poseta konferencijama SAT2009 (Swansea, Velika Britanija) i TPHOLs2009 (Munich, Nemačka). Konferencija SAT je posvećena teoriji i primenama ispitivanja zadovoljivosti dok je konferencija TPHOLs posvećena najnovijim trendovima u interaktivnom dokazivanju teorema.
Mladen Nikolić, Matematički fakultet, Univerzitet u Beogradu
Naslov: Osnove geostatistike
Apstrakt:
Geostatistika pretstavlja podskup statistike specijalizovan za analizu i interpretaciju prostornih podataka. U ovom izlaganju bice prikazana osnovna predikciona metoda koja ima siroke primene u geostatistici. Pored toga, bice pokazano kako se geostatisticka analiza moze vrsiti kombinacijom alata kao sto su R i Google Earth umesto skupim komercijalnim softverima.

17.06.2009.

Julien Narboux, Univerzitet "Louis Pasteur", Strazbur
Naslov: Formalization and automation of geometric reasoning within the Coq proof assistant
Apstrakt:
I will present my work about the formalization and automation of geometric reasoning within the Coq proof assistant. In the first part, I will present a mechanization of the geometry of Tarski. This consists in the formalization of the first eight chapters of the book of Schwabäuser, Szmielew and Tarski: Metamathematische Methoden in der Geometrie. I will explain our approach to deal with degenerated cases using ranks in the context of projective geometry. In the second part, I will present my implementation in Coq of a decision procedure for affine plane geometry: the area method of Chou, Gao and Zhang. This method produces short and readable proofs. In the last part, I will we propose a diagrammatic formal system to perform proofs in the field of abstract term rewriting. For instance, using this system we can formalize the diagrammatic proof of the Newman's lemma. The system is proved correct and complete for a class of formulas called the coherent logic.

27.05.2009.

Filip Marić, Matematički fakultet, Univerzitet u Beogradu
Naslov: Refaktorisanje - poboljšanje dizajna postojećeg koda
Apstrakt:
Refaktorisanje je proces menjanja softverskog sistema tako da se ne menja njegovo spoljno ponašanje, već se poboljšava unutrašnja struktura koda. Na ovom predavanju će (kroz jednostavniji primer u programskom jeziku JAVA) biti prikazane osnovne ideje i tehnike sistematskog refaktorisanja. Takodje, biće prikazana tehnika testiranja funkcionalnih jedinica sistema (unit testing) i biće nagoveštena upotreba projektnih obrazaca (design patterns) kao "gotovih rešenja" za određene probleme softverskog dizajna.

13.05.2009.

Gordana Pavlović Lažetić, Nenad Mitić, Matematički fakultet, Univerzitet u Beogradu
Naslov: N-gramska karakterizacija i predikcija genomskih ostrva
Apstrakt:
Biće predstavljena nova, na n-gramima zasnovana metoda za analizu segmenata u bakterijskim genomima poznatih kao genomska ostrava (GI). Identifikacija GI u bakterijskim genomima je veoma značajna jer mnoga od njih predstavljaju ubačene delove (inserte) koji doprinose bakterijskoj evoluciji i patogenezi. Karakterizacija GI je izvedena na osnovu raspodele n-gramskih frekvencija i zifovske (Zipf) analize prezastupljenih i podzastupljenih n-grama, identifikovanih statistikom baziranom na Markovljevom modelu maksimalnog reda. Metoda je primenjena na specifične regione genoma bakterije Escherichia coli O157:H7 EDL933. Ona profinjuje karakterizaciju zasnovanu na drugim kompozicionim svojstvima genoma kao što su G+C sadržaj ili korišćenje kodona.

N-gramska karakterizacija GI poslužila je kao osnov za metodu predikcije GI. Sastoji se u kombinovanju n-gramskih raspodela operatorima unije i preseka uz definisanje dve mere za ocenu rezultata - odziva (recall) i preciznosti (precision). Korišćenjem najboljih kriterijuma (kombinacija), dobijenih obučavanjem na soju Escherichia coli O157:H7 EDL933, izvršeno je predviđanje GI u 14 genoima familije Enterobacteriaceae i u 21 genomu slučajno odabranih bakterija. Predviđanja su upoređena sa rezultatima dobijenim iz dve posojeće baze genomskih i patogenih ostrva. Rezultati pokazuju da primena n-grama poboljšava i preciznost i odziv predviđanja.

Prikazani rezultati objavljeni su u dva rada ([1], [2]).

Biće ukratko predstavljen i prethodni rad autora u oblasti bioinformatike, kao i neka tekuća istraživanja.

Reference:
G.M. Pavlović-Lažetić, N.S. Mitić, M.V. Beljanski: n-Gram characterization of genomic islands in bacterial genomes, Computer methods and programs in biomedicine, 93 (2009) 241-256
N.S. Mitić, G.M. Pavlović-Lažetić, M.V. Beljanski: Could n-gram analysis contribute to genomic island determination?, Journal of Biomedical Informatics, 41(6) (2008) 936-943

29.04.2009.

Tihomir Gvero , Miloš Gligorić
Naslov: UDITA: Ujedinjene Deklarativne i Imperativne Test Apstrakcije
Apstrakt:
Test apstrakcije su opisi test problema na visokom nivou pomoću kojih alati mogu automatski da generišu konkretne skupove testova. Ranijim istraživanjima su razvijena dva odvojena pristupa za generisanje testova na osnovu 1) deklarativnih 2) imperativnih test apstrakcija. Ova dva pristupa pokazuju svoje dobre strane kroz različite test apstrakcije. Programeri su trenutno primorani da izaberu jedan od ova dva pristupa, što određene aspekte kompleksnih test apstrakcija čini teškim za opis ili neefikasnim za izvršavanje.
Mi predstavljamo UDITA-u, novi radni okvir koji ujedinjuje deklarativne i imperativne test apstrakcije koristeći nedeterministička proširenja u Javi. Kako bi se postiglo efikasno generisanje testova, uvodimo ideju odloženog nedeterminističkog izbora u model checking-u, i razvijamo nove algoritme za odloženo generisanje povezanih struktura. Objašnjavamo implementaciju našeg pristupa u Java PathFinder-u (JPF), popularnom model checker-u za Java programe. Evaluirali smo našu tehniku generianjem testova za niz struktura podataka, za refactoring engine-e, i za sam JPF. Naši eksperimentalni rezultati pokazuju da je generisanje testova korišćenjem ovog pristupa praktično, vodeći ka apstrakcijama koje se lakše pišu i nudi brže generisanje nego u predhodnim radnim okvirima. Rezultati pokazuju da je naša optimizujuća tehnika odloženog izbora od velike važnosti za efikasno generisanje testova. Eksperimenti su otkrili nekoliko predhodno nepoznatih bagova u Eclipse-u, NetBeans-u, i JPF-u.
Predrag Janičić, Matematički fakultet, Univerzitet u Beogradu
Naslov: Korišćenje lema u algebarskim dokazivačima geometrijskih teorema
Apstrakt:
Postoji nekoliko veoma efikasnih algebarskih metoda za dokazivanje geometrijskih teorema i nekoliko pratećih implementacija. Međutim, nijedna od njih ne podržava korišćenje lema i proces dokazivanja uvek kreće iznova, bez oslanjanja na već stečeno znanje. U ovom izlaganju biće izložena jedna ideja za korišćenje lema i plan realizacije u okviru sistema GCLC.

16.04.2009.

Srdjan Vesić, Univerzitet Pol Sabatje, Tuluz
Naslov: Apstraktni okvir za odlučivanje zasnovan na argumentima
Apstrakt:
U ovom radu predlažemo novi pristup za odlučivanje zasnovan na argumentima. Koristimo sistem za argumentaciju u Dungovom stilu koji na ulazu ima različite argumente u prilog mogućim opcijama, konflikte izmedju argumenata kao i preferencije medju njima a na izlazu daje status svake od opcija i kompletan poredak opcija.
U drugom delu ovog rada predstavljamo jedan specijalan slučaj opšteg sistema, naime sistem koji odabira opciju koju podržava najjači argument, pod uslovom da taj argument preživljava sve napade ostalih argumenata. Potom izučavamo svojstva ovog sistema, sa posebnim naglaskom na to kako se menja status opcija (npr. prihvaćena opcija postaje odbijena) u svetlu novog argumenta.
Jasmina Lazić , Univerzitet Brunel, Velika Britanija , Matematički institut Srpske Akademije Nauka i Umetnosti, Beograd
Naslov: Metoda promenljivih okolina sa dekompozicijom za rešavanje problema 0-1 mešovitog celobrojnog programiranja
Apstrakt:
U ovom radu predstavljena je nova hibridna heuristika za rešavanje 0-1 mešovitog celobrojnog programiranja. Sistematično tvrdo fiksiranje promenljivih vrši se u skladu sa pravilima metode promenljivih okolina. Promenljive koje će biti fiksirane se biraju u zavisnosti od rastojanja njihovih vrednosti do vrednosti odgovarajućih promenljivih u rešenju linearne relaksacije polaznog problema. Ako se time postigne poboljšanje vrednosti funkcije cilja, metoda promenljivih okolina sa spustom se primenjuje kao lokalno pretraživanje u celom prostoru pretraživanja. Ovim pristupom poboljšano je 8 do sada najboljih poznatih rezultata za instance iz poznate klase od 29 vrlo teških problema mešovitog celobrojnog programiranja. Osim toga, eksperimenti su pokazali da ova metoda daje bolje rezultate od komercijanog CPLEX rešavača, kao i od još tri aktuelne najuspešnije metode.

01.04.2009.

Damjan Krstajić, Istraživački centar za hemijsku informatiku
Naslov: Proces pronalaska leka i mogućnosti primene automatskog rezonovanja u tom procesu
Apstrakt:
Pronalazak leka je iterativan proces gde se radi na optimizaciji više ciljeva, na prvi pogled kontradiktornih. Proces će biti predstavljen u kratkim crtama i to pre svega matematičkim jezikom. Na kraju izlaganja će biti predstavljene početne ideje za moguću primenu automatskih rešavača. Cilj izlaganja je da se na kraju pokrene diskusija o mogućnostima primene automatskih rešavača u procesu pronalaska leka.
Filip Marić, Matematički fakultet, Univerzitet u Beogradu
Naslov: Primer primene SAT rešavača na parsiranje prirodnog jezika
Apstrakt:
U okviru ovog predavanja biće prikazana tehnika parsiranja prirodnog jezika zasnovana na korišćenju SAT rešavača. Parsiranje se zasniva na formalizmu "link-gramatika" --- svakoj reči u rečenici, korišćenjem rečnika, pridružuje se skup veza koje ona može da ostvari sa ostalim rečima u rečenici i zadatak parsiranja je da se uspostave veze izmedju svih reči u rečenici tako da se ispoštuju odredjeni, unapred zadati, uslovi. Pristup o kome će biti reči predstavlja sve uslove ovog tipa iskaznom formulom i koristi SAT rešavač kako bi pronašao njene modele. Pronadjeni modeli odgovaraju ispravnim povezivanjima, tj. sintaksnim stablima rečenice. Projekat je radjen tokom leta 2008. godine u okviru programa Google Summer of Code i očekuje se dalji rad na ovom projektu.

18.03.2009.

Sana Stojanović, Vesna Pavlović, Matematički fakultet, Univerzitet u Beogradu
Naslov: Tutorijal: Koherentna logika
Apstrakt:
U ovom izlaganju ćemo ukratko izložiti oblast koherentne logike (koja se ponekad naziva i "geometrijskom logikom") i njene osobine. U poslednjih petnaest godina korišćena je u nekoliko okruženja za dokazivanje teorema na tradicionalni način. Takodje ćemo diskutovati o tome kakva je veza dokazivača teorema koji mi razvijamo i koherentne logike, kao i ostalih sistema koji je koriste.
Saša Malkov, Matematički fakultet, Univerzitet u Beogradu
Naslov: Istraživanje korelacija izmedju aminokiselina i sekundarne strukture proteina
Apstrakt:
Korelacija primarne i sekundarne strukture proteina je analizirana na osnovu podataka iz kolekcije Protein Data Bank (PDB). Izračunate su statističke korelacije izmedju svake od 20 aminokiselina i 8 tipova sekundarnih struktura, na medjusobnoj udaljenosti od 25 jedinica.
Na osnovu dobijenih rezultata i skolonosti gradjenju odredjenih sekundarnih struktura, aminokiseline su klasifikovane u četiri grupe: sklone α-heliksima, sklone trakama, sklone zavojima i ostale (His i Cys ne pokazuju naklonost ni prema jednoj sekundarnoj strukturi). Pokazuje se da aminokiseline u istoj grupi imaju slične strukturne karakteristike na Cβ i Cγ atomima. Sve AK sklone α-heliksima nemaju ni polarne heteroatome vezane na atome Cβ i Cγ, ni grananje ni aromatične grupe na atomu Cβ. Sve AK sklone trakama imaju aromatične grupe ili heteroatome na atomu Cβ. Sve AK sklone zavojima imaju polarne heteroatome na atomima Cβ ili Cγ ili uopšte nemaju atom Cβ. Ova nova pravila mogu biti korisna u predvidjanju ponašanja sintetisanih AK koje ne postoje u prirodi.
Rezultati udaljenih korelacija pokazuju značajnost korelacija na udaljenosti do 10 jedinica. Pokazuje se da delovi vezani na atome Cβ i Cγ imaju primarnu ulogu u sklonosti AK prema sekundarnim strukturama podataka na istom mestu, a da polarnost aminokiselina ima značajan uticaj na gradjenje α-heliksa i traka na udaljenim mestima u sekvenci. Korelacije koje odgovaraju polarnim AK su značajno asimetrične.

25.02.2009.

Aljoša Obuljen
Naslov: Tutorijal: Bajesovsko ucenje
Apstrakt:
Ovaj tekst predstavlja kratak pregled oblasti bajesovskog učenja (eng. Bayesian learning). Bajesovski pristup mašinskom učenju je pogodan kada je potrebno analizirati podatke i donositi odluke na osnovu teorije verovatnoće. Ovaj pristup je važan kako za odredjivanje merodavnosti podataka koji idu u prilog hipotezi koja se razmatra koristeći teoriju verovatnoće, tako i u uporednoj analizi različitih metoda mašinskog učenja.
Predrag Janičić, Matematički fakultet, Univerzitet u Beogradu
Naslov: Uniformno svodjenje teških problema na SAT
Apstrakt:
U izlaganju će biti predstavljen jedan uniforman pristup za svodjenje teških problema na SAT. Pristup koristi ideju preopterećivanja operatora u objektno-orijentisanom programiranju. Pristup je već korišćen na kriptoanalitičkim problemima (zajednički rad sa Dejanom Jovanovićem i Milanom Šešumom). Biće opisano kako dodatni tipovi problema, sa posebnim naglaskom na NP-kompletne probleme, mogu biti obradjivani na sličan način.

30.01.2009. - 31.01.2009.

Second Workshop on Formal and Automated Theorem Proving and Applications

24.12.2008.

Staša Vujičić, Matematički fakultet, Univerzitet u Beogradu
Naslov: Tutorijal: Genetski algoritmi
Apstrakt:
Genetski algoritmi su pristup mašinskom učenju baziran nasimuliranju evolucije. Hipoteze se najčešće reprezentuju nizovima bitova čija interpretacija zavisi od aplikacije, mada mogu biti reprezentovane i simboličkim izrazima ili čak računarskim programima. Potraga za odgovarajućom hipotezom počinje populacijom, to jest skupom inicijalnih hipoteza. Članovi trenutne populacije utiču na razvoj naredne generacije putem operatora ukrštanja i mutacije, koji su definisani po uzoru na procese u biološkoj evoluciji. U svakom koraku,hipoteze u trenutnoj populaciji se procenjuju na osnovu mere prilagodjenosti, gde se najbolje prilagodjene hipoteze biraju za proizvodnju naredne generacije. Genetski algoritmi se uspešno primenjuju u nizu problema učenja i problema optimizacije. Na primer, koriste se za učenje skupa pravila za kontrolu robota i za optimizaciju topologije i parametara učenja za veštačke neuronske mreže. U ovom radu prikazana je varijantagenetskih algoritama, u kojoj se hipoteze reprezentuju kao nizovibitova i varijanta genetskog programiranja, u kojoj se hipotezereprezentuju pomoću programa.
Bojan Marinković, Matematički institut SANU
Naslov: Logika sa operatorom uslovne verovatnoće
Apstrakt:
Tokom avgusta meseca 2008. godine u Hamburgu je održana letnja škola ESSLLI 2008. Grupa mladih istraživača Matematičkog instituta SANU predstavila je svoj rad u okviru studentske sesije na ovoj letnjoj školi. Tokom ovog izlaganja biće predstavljen sam rad koji dajesaglasnu i jaku kompletnost aksiomatizacije za rezonovanje o linearnoj kombinaciji uslovnih verovatnoća, odlučivost sa procedurom odlučivanja u klasi PSPACE, kao i informacije o samoj letnjoj školi.

03.12.2008.

Predrag Janičić, Matematički fakultet, Univerzitet u Beogradu
Naslov: Poseta Univerzitetu u Rimu i prezentacija paketa GCLC
Apstrakt:
U izlaganju će biti dat osvrt na skorašnju posetu Matematičkom fakultetu Univerziteta u Rimu. Biće ukratko ponovljena i dva predavanja o paketu GCLC koja su tamo održana. Posebno će biti reči o mogućim pravcima daljeg razvoja GCLC-a.
Panel diskusija: Aktuelne i planirane istraživačke teme

Diskusija o tekućim i planiranim istraživačkim problemima, posebno o aspektima potencijalno interesantnim novim studentima doktorskih studija.

19.11.2008.

Mladen Nikolić, Matematički fakultet, Univerzitet u Beogradu
Naslov: Tutorijal: Linearna regresija i njena primena u ubrzavanju SAT rešavača
Apstrakt:
Regresija je postupak odredjivanja funkcije koja približno povezuje vrednosti dve slučajne promenljive. Najčešće je ta funkcija definisana skupom parametara čijim se fiksiranjem bira jedna iz unapred definisanog skupa. Ovaj izbor se vrši na osnovu datih trening podataka. Ukoliko su sve dopustive funkcije linearne po svojim parametrima, regresija se naziva linearnom. Taj problem se obično rešava minimizacijom srednjekvadratne greške metodom najmanjih kvadrata uz eventualnu regularizaciju problema. Jedna od primena linearne regresije je predikcija vremena rešavanja diskretnih problema kao što je SAT na osnovu nekih karakteristika instance koja se rešava.
Milan Banković, Matematički fakultet, Univerzitet u Beogradu
Naslov: Alldifferent SMT rešavači
Apstrakt:
Programiranje ograničenja je istraživačka oblast koja poslednjih godina sve više dobija na značaju zbog svoje fleksibilnosti i široke oblasti primene. U pitanju je deklarativni stil programiranja u kome se problem definiše skupom ograničenja koje njegovo rešenje mora da zadovoljava. Rešavanje ovakvog problema se svodi na pronalaženje vrednosti promenljivih koje zadovoljavaju sva data ograničenja. Jedno od najpoznatijih i najčešćih ograničenja je tzv. "alldifferent" ograničenje koje zahteva da nikoje dve promenljive iz datog skupa promenljivih ne mogu uzeti jednake vrednosti. Poseban izazov predstavlja povezivanje programiranja ograničenja i SAT problema, koristeci SMT pristup. U ovom izlaganju ćemo dati kratak opis "alldifferent" ograničenja, povezujuci ga sa teorijom uparivanja u bipartitnim grafovima. Zatim ćemo uspostaviti vezu "alldifferent" ograničenja i SAT problema, predstavljajući ovo ograničenje kao SMT problem. Na kraju ćemo dati predlog algoritma za generisanje objašnjenja propagacija u "alldifferent" SMT rešavaču.

05.11.2008.

Vesna Pavlović, Matematički fakultet, Univerzitet u Beogradu
Naslov: Izveštaj sa Letnje škole ICCL 2008, Dresden
Apstrakt:
Šesta po redu ICCL letnja škola održana je u Dresdenu u periodu od 24. avgusta do 6. septembra u organizaciji TU Dresden. Glavna tematika letnje škole bio je odnosizmedju moderne formalne logike i zdravog razuma koji karakteriše ljudsko rasudjivanje. Na predavanju će biti ukratko prikazane osnovne ideje razmatrane na ovoj letnjoj školi.
Damjan Krstajić, Istraživački centar za hemijsku informatiku
Naslov: Discovery Bus - sistem za automatsko pravljenje QSAR modela
Apstrakt:
Postoji više različitih načina i pristupa prilikom pravljenja statističkih/QSAR modela. Bez obzira na naše preference, praksa nas uči dane postoji jedno rešenje koje daje najbolje rezultate u svim situacijama. Sa druge strane, sa razvojem robotizovanih laboratorija u situaciji smo daimamo konstantan priliv eksperimentalnih rezultata. Izazov nam je bio da napravimo sistem koji će da se nosi sa konstantnim prilivom novih podataka i koji će automatizovati pravljenje statističkih/QSAR modela. Discovery Bus je naš odgovor tom izazovu. To je implementacija Competitive Workflow arhitekture koja se bazira na autonomnim softver agentima.

18.06.2008.

Panel diskusija: Aktuelne istraživačke teme

Istraživački problemi kojima smo se bavili tokom prethodne akademske godine, kojima se trenutno bavimo i kojima planiramo da se bavimo.

04.06.2008.

Mladen Nikolić, Matematički fakultet, Univerzitet u Beogradu
Naslov: Metodologija izbora pogodnih vrednosti parametara SAT rešavača
Apstrakt:
Razni aspekti funkcionisanja SAT rešavača se definišu pomoću odredjenih parametara. Efikasnost SAT rešavača u velikoj meri zavisi od konkretne iskazne formule koja se rešava i od konkretnih vrednosti parametara rešavača. Stoga postoji potreba da se formuliše metodologija izbora vrednosti parametara koja bi polazila od analize svojstava formule koja se rešava. Formulisani pristup se bazira na predstavljanju formule u vidu grafa i korišćenju mera sličnosti nad grafovima kako bi se za nepoznatu formulu našli parametri za koje se SAT rešavač dobro ponaša pri rešavanju sličnih formula.
Vesna Pavlović, Sana Stojanović, Matematički fakultet, Univerzitet u Beogradu
Naslov: Formalizacija i automatizacija euklidske geometrije
Apstrakt:
Ideja formalizacije geometrijskog rezonovanja je novijeg datuma i još je u svojim počecima, te predstavlja oblast za koju se očekuje da ćebiti u centru pažnje narednih godina. Više autora uspelo je da formalizuje deo Hilbertovih aksioma, takodje i deo aksioma Tarskog, i da uspe da formalizuje neke od teorema koje se odnose na te grupe aksioma. Dokazi teorema su izvedeni 'ručno' uz pomoć sistema tipa Isabelle. Predmet našeg istraživanja je automatizacija ovog procesa, čime dobijamo i formalnu verifikaciju dokaza u sistemu Isabelle.

14.05.2008.

Prof. Pedro Quaresma, Univerzitet Coimbra, Portugal
Naslov: Cryptology - a (very) Brief Survey
Apstrakt:
Cryptology is the science of the enciphering and deciphering of messages in a secret code or cipher, the cryptography, and also the science (and art) of recovering information from ciphers without knowledge of the key, the cryptoanalysis. A brief presentation of this dual process of hidden/cracking the information, from the classical ciphers, to the modern symmetric, and public key ciphers will be presented.

19.04.2008. - 25.04.2008.

Spring School Geometry and Visualization
1. Predrag Janičić, The Faculty of Mathematics, University of Belgrade
  Naslov: Intelligent Geometrical Software
2. Vesna Pavlović, Sana Stojanović, The Faculty of Mathematics, University of Belgrade
  Naslov: Formalization and Automation of Euclidean Geometry
3. Predrag Janičić, The Faculty of Mathematics, University of Belgrade
  Naslov: GCLC - lab session

16.04.2008.

Prof. Steve A. Quarrie, Direktor Konsultativne kancelarije za medjunarodne projekte, Ministarstvo nauke, Srbija
Naslov: FP7 and looking for the truth: you mathematicians have it easy!
Apstrakt:
What is the relevance of FP7 to young researchers and PhD students? FP7 has a lot of opportunities for young scientists to improve their research skills, but the best FP7 money goes to only the very best quality research. The talk will focus on how you ensure that you are doing the best quality research. Developing effective research skills needs constant help and support to understand what to do and, more importantly, why. The purpose of the post-graduate education is to teach PhD students how to THINK and to become RELIABLE as independent workers using RESEARCH as the vehicle for these goals. Research is looking for the TRUTH and a key to finding the truth is good experimental design. Examples will be presented of how to design experiments to enable you to find the truth and to recognise when you have found it. You will learn something about cheese, ozone, wheat and Canadian burglars!

02.04.2008.

Jelena Tomašević, Matematički fakultet, Univerzitet u Beogradu
Naslov: Tutorijal: XML baze podataka
Apstrakt:
U poslednjih nekoliko godina Extensible Markup Language (XML) je postao dominantni standard za opisivanje i razmenu podataka na Internetu. Sa druge strane, XML je uveo nekoliko novih problema kao na primer kako efikasno čuvati i upravljati XML podacima. U zavisnosti od stepena regularnosti strukture, XML dokumenti upadaju u dve široke kategorije: data-centric i document-centric. Data-centric dokumenti se karakterišu regularnom strukturom bez mešovitog sadržaja. Moguće je izvršiti preslikavanje ovakvih XML dokumenta u relacionu bazu podataka. Takve baze podataka nazvane su XML-proširene. Document-centric XML dokumenti se karakterišu neregularnom strukturom i mešanim sadržajem. Najbolji način za skladištenje i manipulisanje ovim dokumentima je u okviru izvornih XML baza podataka. Osnovne karakteristike izvornih XML baza podataka su:
1. XML dokument je osnovna logička jedinica, kao što je to vrsta u tabeli kod relacionih baza.
2. Minimalno, model mora uključiti elemente, atribute, tekstualne podatke (PCDATA) i redosled dokumenta.
3. Nema zahteva za postojanjem bilo kakvog specifičnog fizičkog modela skladištenja.
Izvorne XML baze podataka smeštaju XML dokumente kao logičke jedinice i dobijaju podatke iz baze korišćenjem nekog od upitnih jezika kao što su XPath ili XQuery.
Vladan Radivojević
Naslov: Mali deduktivni sistemi
Apstrakt:
Teorija L ima jedno pravilo izvodjenja i tri aksiomatske sheme (nad veznicima implikacija i negacija). Nad istim skupom veznika i sa istim pravilom izvodjenja postoje i manji deduktivni sistemi ekvivalentni teoriji L. Na primer, Mereditov sistem konstruisan 1953. godine sadrži samo jednu aksiomu. Nad Šeferovim veznikom se takodje, moze konstruisati deduktivni sistem sa jednom aksiomom ekvivalentan teoriji L. Jedan takav sistem je dao Nikod 1917. godine.
Rad se bavi ovim, "malim" deduktivnim sistemima kao i još nekim osobinama formula nad Šeferovim veznikom. Takodje, rad sadrži i kratak sažetak knjige S.Volframa "New kind of science".

12.03.2008.

Bojan Marinković, Matematički institut SANU
Naslov: Tutorijal: Uvod u analizu algoritama
Apstrakt:
Ovim predavanjem biće prikazan pregled knjige "An Introduction to the Analysis of Algorithms" R. Sedgewick-a i P. Flajolet-a, u okviru ispitnog rada za kurs "Teorijsko računarstvo" na prvoj godini poslediplomskih studija na Matematičkom fakultetu Univerziteta u Beogradu.
Petar Maksimović, Matematički institut SANU
Naslov: Jednostavna karakterizacija potpunih jednočlanih skupova logičkih veznika
Apstrakt:
Za skup logičkih veznika kažemo da je potpun ukoliko se sve iskazne formule mogu izraziti koristeći samo veznike iz tog skupa. Na ovom predavanju će biti predstavljeni potrebni i dovoljni uslovi za potpunost jednočlanog skupa logičkih veznika. Ovi uslovi daju jednostavnu i elegantnu karakterizaciju, i, dodatno, omogućavaju obrojavanje potpunih jednočlanih skupova logičkih veznika proizvoljne arnosti.

29.01.2008. - 01.02.2008.

Workshop on Formal Theorem Proving
1. Filip Marić, The Faculty of Mathematics, University of Belgrade
  Naslov: Formal Verification of SAT Solvers
2. Predrag Janičić, The Faculty of Mathematics, University of Belgrade
  Naslov: ARGO Group Presentation

16.01.2008.

Goran Predović, Microsoft Development Center Serbia
Naslov: Tutorijal: Algebarsko dokazivanje geometrijskih teorema (ADGT)
Apstrakt:
Iako je jasna veza izmedju geometrije i algebre utvrdjena još u 17. veku (Rene Dekart), teorija dokazivanja geometrijskih teorema koje su formulisane na algebarski način je razvijena tek krajem 20. veka kada je uspešne rezultate objavio kineski matematičar Vu Ven Cen (Wen-Tsun Wu). Algebarski dokazivači su se pokazali veoma moćni dokazujući na stotine netrivijalnih teorema i otkrivajući nove teoreme u geometriji. U okviru predavanja će biti predstavljene osnove ADGT-a, dve najpoznatije metode - Vuova metoda i metoda Grebnerovih baza, kao i integracija dokazivača u sistem GCLC sa primerima dokazanih teorema.
Filip Marić, Matematički fakultet, Univerzitet u Beogradu
Naslov: Izrada rasporeda časova korišćenjem iskaznog rezonovanja
Apstrakt:
U ovom predavanju će biti predstavljena tehnika izrade rasporeda časova tehnikom svodjenja na iskazno rezonovanje. Uslovi koji opisuju uslove korektnosti rasporeda časova (npr. da jedna nastavna grupa ne može istovremeno da ima dva predmeta, da jedan predavač ne može istovremeno da predaje dva različita predmeta) kao i uslovi koji opisuju pojedinačne želje predavača (odredjeni predavači žele da rade samo odredjen broj radnih dana, imaju termine u kojima ne žele da rade, ne žele da imaju pauze u toku radnog dana) se opisuju iskaznom formulom i SAT solveru se prepušta pronalaženje modela formule. Svaki pronadjeni model predstavlja zadovoljavajući raspored časova.

26.12.2007.

Vesna Pavlović, Matematički fakultet, Univerzitet u Beogradu
Naslov: Tutorijal: Teorija tipova
Apstrakt:
Konstruktivna terija tipova s jedne strane predstavlja okvir koji spaja logiku i programske jezike na jedan elegantan način; na taj način razvoj programa i njegova verifikacija mogu da se izvršavaju kao jedinstven sistem. S druge strane, teoriju tipova možemo videti kao funkcionalni programski jezik sa nekim novim svojstvima. Pri odredjenim pretpostavkama moguće je definisati sistem koji je ujedno i logički sistem i programski jezik i u kome su tvrdjenja i tipovi ekvivalentni, kao i dokazi tvrdjenja, odnosno elementi tipova.
U okviru ovog predavanja razmatraćemo osnove konstruktivističke logike, netipiziranog i tipiziranog lambda računa, a zatim ćemo videti na kojim je pravilima zasnovana teorija tipova, upoznaćemo se sa osnovnim pojmovima i tvrdjenjima teorije tipova, zaključno sa Curry Howard izomorfizmom.
Milena Vujošević-Janičić, Matematički fakultet, Univerzitet u Beogradu
Naslov: Automatsko otkrivanje prekoračenja bafera u programskom jeziku C
Apstrakt:
Prekoračenje bafera je važan problem za kvalitet i bezbednost softvera. Tehnike za automatsko detektovanje prekoračenja bafera dele se na dinamičke i statičke tehnike. Dinamičke tehnike analiziraju program u fazi izvršavanja dok statičke tehnike analiziraju izvorni kod i imaju za cilj otkrivanje mogućih prekoračenja bafera pre nego što se program pusti u rad. U okviru ovog predavanja biće prikazan nov statički sistem za automatsko otkrivanje prekoračenja bafera. Sistem uzima u obzir kontrolu toka podataka i analizira i statički i dinamički alocirane bafere. Arhitektura sistema je fleksibilna i modularna. Na primer, sistem koristi spoljašnju biblioteku uslova koja je lako proširiva, a koja čuva pravila rezonovanja tako da ona nisu direktno kodirana u okviru sistema. Takodje, za proveru važenja generisanih uslova ispravnostii neispravnosti komandi, može da se koristi bilo koji spoljašnji automatski dokazivač teorema koji prati SMT-LIB standarde. U okviru ovog predavanja, biće prikazana i prototip implementacija sistema - alat FADO.

5.12.2007.

Milan Banković, Matematički fakultet, Univerzitet u Beogradu
Naslov: Tutorijal: Analiza algoritama - praktičan pristup
Apstrakt:
Prilikom analize algoritama u praksi, veoma je važno proceniti očekivano vreme izvršavanja algoritma, odnosno proučiti ponašanje algoritma u prosečnom slučaju. Analiza prosečnog slučaja je, po pravilu, znatno složenija od analize najgoreg slučaja, i zbog toga je potrebno razviti moćniji matematički aparat. U okviru ovog predavanja biće ilustrovana primena funkcija generatrisa u analizi algoritama, pre svega kroz primenu u teoriji prebrojavanja, na kojoj se analiza prosečnog slučaja i temelji. Upoznaćemo se sa simboličkim metodom, kao jednim veoma intuitivnim šablonom za povezivanje skupova kombinatornih objekata sa funkcijama generatrisama koje te skupove prebrojavaju. Takodje će biti razmotrena i primena funkcija generatrisa u rešavanju rekurentnih relacija.
Vesna Pavlović, Matematički fakultet, Univerzitet u Beogradu
Naslov: Fazna promena u k-GD-SAT problemu
Apstrakt:
k-GD-SAT problem označava familiju slučajnih SAT problema koji se zasnivaju na geometrijskoj raspodeli dužina klauza sa parametrom p (0 < p < = 1); za p = 1 dobija se tačnok-SAT model. Friedgut je napravio veliki proboj dokazom postojanja neuniformnog praga zadovoljivosti, tj. niza r(n) oko koga verovatnoća zadovoljivosti formule ide od 1 do 0. Naš cilj jeda dokažemo istu stvar za k-GD-SAT problem - tj. da k-GD-SAT ima oštar prag za svaku vrednost parametra p, i da na taj način (obzirom da je k-SAT problem samo jedna potklasa k-GD-SAT problema za p = 1) proširimo klasu SAT problema za koje ovo tvrdjenje važi.

14.11.2007.

Filip Marić, Matematički fakultet, Univerzitet u Beogradu
Naslov: Tutorijal: Formalizacija iskazne logike u okviru sistema Isabelle
Apstrakt:
U okviru ovog predavanja će biti prikazane osnovne mogućnosti sistema Isabelle. Sistem Isabelle je jedan od najkorišćenijih alata za formalizaciju matematike koji omogućuje da se matematički pojmovi izraze u odgovarajućem formalnom okviru (najčešće u logici višeg reda) i da se nakon toga formalno dokažu teoreme koje opisuju njihova svojstva. Korišćenje sistema Isabelle će biti prikazano kroz formalizaciju iskaznog računa. Na početku će biti definisani pojmovi promenljive, literala, formule, valuacije, relacija zadovoljivosti, a nakon toga će biti dokazane mnoge teoreme koje važe za iskaznu logiku.
Claudio Castellini, LIRA-Lab, Univerzitet Genova, Italija
Naslov: Machine Learning for Hand Prosthetics (and more)
Apstrakt:
Currently, the dexterity of active hand prosthetics is hindered due to limitations in interfaces. How is an amputee supposed to command the prosthesis what to do (i.e., how to grasp an object) and with what force (i.e., holding a hammer or grasping an egg)? In this talk I address the issue by applying machine learning to the problem of regression from surface forearm EMG to the force a subject is applying. A detailed comparative analysis among three different machine learning approaches reveals that the apporach, as a whole, is viable. More applications of machine learning to grasping and reaching will be shown, among which prediction of grasping postures and of the user's intention to grasp.

31.10.2007.

Mladen Nikolić, Matematički fakultet, Univerzitet u Beogradu
Naslov: Tutorijal: Mašinsko učenje
Apstrakt:
Mašinsko učenje je disciplina koja se bavi proučavanjem generalizacije i konstrukcijom i analizom algoritama koji generalizuju. Učenje se često može videti kao aproksimiranje ciljne funkcije (onoga što treba naučiti) ili kao pretraga prostora hipoteza vodjena podacima. Izbor prostora hipoteza je ključan za uspešno učenje, a kvalitet tog izbora se može proceniti pomoću Vapnik-Červonenkisove (VC) dimenzije ovog prostora. VC dimenzija opisuje prilagodljivost hipoteza podacima. Visoka VC dimenzija prostora hipoteza dovodi do poznatog problema overfitting-a. Način da se ovaj problem izbegne, odnosno da se postigne kvalitetna generalizacija je predložen u statističkoj teoriji učenja kroz princip strukturalne minimizacije rizika.
Filip Marić, Matematički fakultet, Univerzitet u Beogradu
Naslov: SMT rešavači i ArgoLib - kratak osvrt
Apstrakt:
U okviru ovog kratkog predavanja biće prikazani problemi koji se rešavaju korišćenjem SMT (Satisfiability Modulo Theory) resavača. SMT se bavi ispitivanjem zadovoljivosti formula odredjenih teorija prvog reda za koje postoje specijalizovane procedure odlučivanja. Najčešće korišćene teorije su linearna aritmetika (LA), teorija jednakosti sa neinterpretiranim funkcijskim simbolima (EUF), teorija nizova (ARRAYS), itd. Savremeni SMT rešavači su uglavnom zasnovani na DPLL(T) algoritmu koji predstavlja nadogradnju DPLL procedure na kojoj se zasnivaju savremeni SAT rešavači. SMT danas nalazi svoje primene u formalnoj verifikaciji softvera i hardvera, izgradnji kompilatora, optimizaciji i mnogim drugim oblastima računarstva.
Saša Misailović, Elektrotehnički fakultet, Univerzitet u Beogradu
Naslov: Automatizovano generisanje test ulaza korišćenjem imperativnih predikata
Apstrakt:
Korat je program za generisanje strukturno kompleksnih test ulaza. Iscrpno se generišu svi test ulazi do neke odredjene veličine. Osobine test ulaza korisnik piše u Javi u obliku imperativnog predikata. Pored toga, korisnik ograničava prostor stanja, kroz navodjenje mogućih vrednosti za polja strukture. Na osnovu ovako pripremljene strukture, Korat vrši pretragu prostora stanja i efikasno generiše sve neizomorfne strukture sa željenim osobinama. Više informacija oKoratu se može naći na adresi: http://korat.sourceforge.net .

17.10.2007.

Filip Marić, Matematički fakultet, Univerzitet u Beogradu
Naslov: Tutorijal: SAT rešavači
Apstrakt:
SAT rešavači su programi koji ispituju zadovoljivost iskaznih formula. Formule se obično zadaju u konjunktivnoj normalnoj formi (CNF) i njihova zadovoljivost se ispituje modifikovanom verzijom DPLL (Davis-Putnam-Logemann-Loveland) procedure. Današnji SAT rešavači su u stanju da ispitaju zadovoljivost formula koje imaju nekoliko desetina pa čak i stotina hiljada varijabli i milione klauza. U okviru ovog predavanja će biti prikazan pregled vodećih SAT rešavača i biće dat prikaz nerekurzivne implementacije DPLL agoritma upravo na način na koji se koristi prilikom implementacije vodećih rešavača. Takodje, biće pomenute i neke modifikacije osnovnog DPLL algoritma koje su doprinele ogromnom uspehu današnjih SAT rešavača (nonchronological backtracking (backjumping), clause learning).
Mladen Nikolić, Matematički fakultet, Univerzitet u Beogradu
Naslov: Nove metode za računanje sličnosti čvorova grafova i sličnosti celih grafova
Apstrakt:
Postoji veći broj metoda za procenu sličnosti grafova. Jedan od pristupa se bazira na proceni sličnosti njihovih čvorova. Metoda rasparenih sličnosti je nova metoda za računanje sličnosti čvorova koja na odredjenim problemima pokazuje bolje ponašanje od dosadašnjih, ali se može primeniti i na problemima na koje su dosadašnje metode bile neprimenljive. Najvažnija prednost je mogućnost konstrukcije mere sličnosti celih grafova na osnovu procenjenih sličnosti njihovih čvorova. Prva testiranja daju vrlo ohrabrujuće rezultate.

ARGO

Automated reasoning group

≡ Navigation

Argo seminar: najave predavanja