Argo Seminar: Announcements
Click here for Serbian version.  Kliknuti ovde za verziju na srpskom jeziku.
Argo seminar is a regular seminar of the Argo group. Main fields discussed are Automated Reasoning and Applications, Theoretical Computer Science, Artificial Intelligence and Data Mining. The seminar is dedicated mainly to PhD students in Computer Science. One meeting typically consists of two lectures: a tutorial one (where known results on one specific topic are presented) and a research one (where original research work is presented).
Meetings take place once in two weeks, usually on Thursday at 6:00PM, in the premises of the Faculty of Mathematics in Studentski trg street, classroom 718.
Seminar secretary: Vesna Marinković
If you are interested in receiving information on the seminar and lecture announcements, please send an email to Vesna Marinković or Predrag Janičić .
27.12.2018.

Petar Vukmirović, Vrije Universiteit Amsterdam
Title: Extending Firstorder Theorem Prover to Higherorder LogicAbstract:
Decades of work have gone into developing efficient proof calculi, data structures, algorithms, and heuristics for firstorder automatic theorem proving. Higherorder provers lag behind in terms of efficiency. Instead of developing a new higherorder prover from the ground up, we propose to start with the stateoftheart superpositionbased prover E and gradually enrich it with higherorder features. We explain how to extend the prover’s data structures, algorithms, and heuristics to λfree higherorder logic, a formalism that supports partial application and applied variables. Our extension outperforms the traditional encoding and appears promising as a stepping stone towards full higherorder logic
11.10.2018.

Pavle Subotic, Amazon
Title: Debugging Large Scale Logic ProgramsAbstract:
Logic programming languages such as Datalog have become popular as Domain Specific Languages (DSLs) for solving largescale problems, in particular, static program analysis including pointsto analysis and network analysis. Logic programs that process largescale data are, however, difficult to debug. In the database community, data provenance techniques have been proposed that could address the Declarative Debugging Challenge for largescale inputs. Unfortunately, the current stateoftheart approaches for dataprovenance 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 fixedpoint semantics for seminaive evaluation to compute with the augmented lattice, and propose a provenance query mechanism to constructs partial minimal height proofs for tuples.
29.3.2018.

Marc Bezem, Institute for Informatics, University of Bergen, Norway
Title: The Univalence Axiom in Dependent Type TheoryAbstract:
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
Title: A ModelConstructing Approach to Solving BitVector ConstraintsAbstract:
The ModelConstructing 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 conflictdriven 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 fixedsize bitvectors, based on tailormade conflictdriven learning that exploits both propositional and arithmetic properties of bitvector operations. In our approach, bitvectors are firstorder citizens and unnecessary bitblasting is avoided altogether.
23.3.2017.

Julien Narboux, University of Strasbourg
Title: GeoCoq, foundations of geometry formalized in CoqAbstract:
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
Title: Computational Origami System EosAbstract:
I will talk about a computational origami system called Eos (eorigami 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
Title: Solving, Reasoning, and Programming in Common LogicAbstract:
Common Logic (CL) is an ISO standard for exchanging logicbased information in heterogeneous, open networks of computerbased systems. The representational requirements of knowledge in open networks led to some important changes of traditional firstorder 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 (crosscategoricity), terms can be applied to other terms, and the language is typefree. 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 wellbehaved 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
Title: Synthesizing Analyzers from DatalogAbstract:
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 onpar with stateoftheart manual tools (e.g., performs a pointsto 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
Title: Coquand's site semantics of coherent logicAbstract:
We introduce socalled 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 Belgrade
Informal VerificationAbstract:
A Coq workshop based on "Software Foundations" course at University of Pennsylvania was held in Hacklab Belgrade hackerspace from June 2012 to December 2013. The core of the course is the study of operational semantics and type systems of programming languages, together with an introduction to formal reasoning about functional and imperative programs. We will present an overview of the "Software Foundations" course, provide some basic information on Coq proof assistant, and highlight some of the experiences gained through teaching in an informal, noninstitutional setting.
22.07.2014.
24.07.2014.

Marc Bezem, Institute for Informatics, University of Bergen, Norway
Title: Homotopy Type TheoryAbstract:
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://ufias2012.wikispaces.com/The+book
02.07.2014.

Sana Stojanović, Faculty of Mathematics, University of Belgrade
Title: A Vernacular for Coherent Logic and Automated Generation of Machine Verifiable and Readable ProofsAbstract:
We will present our framework for automated generation of proofs from the book "Metamathematische Methoden in der Geometrie" (by Wolfram Schwabhauser, Wanda Szmielew, and Alfred Tarski) using resolution theorem provers and a coherent logic theorem prover. Also, we will present a simple proof representation that we developed within coherent logic. This proof representation can be used for generation of proofs in different proof assistants (Isar and Coq). 
Mirko Stojadinović, Faculty of Mathematics, University of Belgrade
Title: Instancebased Selection of CSP Solvers using Short TrainingAbstract:
Title: Air Traffic Controller Shift Scheduling by Reduction to CSP, SAT and SATrelated Problems
Many different approaches for solving Constraint Satisfaction Problems (CSP) (and related Constraint Optimization Problems (COP)) exist. However, there is no single solver that performs well on all classes of problems and many portfolio approaches for selecting a suitable solver based on simple syntactic features of the input CSP instance are developed. We will present a portfolio method for CSP based on knearest neighbors method. Unlike other existing portfolio approaches for CSP, our methodology is based on training with very short timeouts, thus significantly reducing overall training time. Still, thorough evaluation has been performed on large publicly available corpora and our portfolio method gives good results. The method improves upon the efficiency of single stateoftheart tools used in comparison, and is comparable to classical methods that use long timeout during the training phase.Abstract:
We will present our experience in solving Air Traffic Controller Shift Scheduling Problem. We will give a formal definition of this optimization problem and introduce three encodings. The encodings make possible to formulate a very wide set of different scheduling requirements. The problem is solved by using SAT, MaxSAT, PB, SMT, CSP and ILP solvers. In combination with these solvers, three different optimization techniques will be presented, a basic technique and its two modifications. The modifications use local search to modify some parts of the initial solution. Results indicate that SATrelated approaches outperform other solving methods used and that one of the introduced techniques which uses local search can significantly outperform the basic technique. We have successfully used these approaches to make shift schedules for one air traffic control center.
13.03.2014.

Aleksandar Zeljic, Department of Information Technology, Uppsala University, Sweden
Title: Approximations for Model ConstructionAbstract:
We consider the problem of efficiently computing models for satisfiable constraints, in the presence of complex background theories such as floatingpoint arithmetic (FPA). Model construction has various applications, for instance the automatic generation of test inputs. It is wellknown that naive encoding of constraints into simpler theories (for instance, bitvectors 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 overapproximations (or the combination of both) can be used, and shows promising results in practice.
12.12.2013.

Pascal Schreck, University of Strasbourg, France
Title: Combinatorial approaches in incidence projective geometryAbstract:
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
Title: Semiinteractive proofs within Tarski's geometryAbstract:
We will present our current work and project about formalization of highschool 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
Title: Guiding Craig Interpolation with Domainspecific AbstractionsAbstract:
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 solverindependent 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 eAustria Research Institute Timisoara, Romania
Title: Phase Transitions in Random Constraint Satisfaction Problems: A Personal PerspectiveAbstract:
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 firstorder 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
Title: The Interaction of Representation and Reasoning (part I)
Title: The Interaction of Representation and Reasoning (part II)

Pascal Schreck, University of Strasbourg, France
Title: RC(un)constructibility, proofs and constructionsAbstract:
Lebesgue's method is often presented as the method to prove RCconstructibility 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: RittWu's principle for decomposition/triangularization and Lebesgue's method for solving irreducuble polynomials using square radicals. I also present some examples of RCconstructibility and unconstructiblity. 
Julien Narboux, University of Strasbourg, France, December
Title: Tarski's and Hilbert's geometryAbstract:
20.09.2012.

Tihomir Gvero, Ecole Polytechnique Federale de Lausanne (EPFL)
Title: Fast Code Completion using Type InhabitationAbstract:
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 PSPACEcomplete. 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
Title: Automating Coherent Logic: an overview
29.12.2011.

Vesna Marinković, Faculty of Mathematics, University of Belgrade
Title: Overview of the paper "Automated Generation of Construction Steps for Geometric Constraint Problems", Chou, Gao, ZhangAbstract:
In this talk a brief description of the system for geometric constraint solving that takes as an input the declarative description of a geometric diagram and outputs a procedure of how to draw a diagram using ruler and compass will be given. The method tries to determine the position of some geometric object using the known positions of some other geometric objects, and the constraints used are not only those involving this object, but also some implicit information derivation derived from other constraints. 
Novak Novaković, Mathematical Institute of the Serbian Academy of Sciences and Arts, Belgrade
Title: Algebraic resource semantics of proofs in classical logicAbstract:
Programs of a purely functional programing language / terms of lambda calculus are in relation to formal proofs in (intuitionistic) logic through the CurryHoward correspondence. General proof theory is a discipline of mathematical logic which investigates precisely those formal proofs as formal mathematical objects. While the notion of a formal proof is well defined, nearly a century of the development of the discipline has failed to provide an answer to the central open problem of the general proof theory  when are two given proofs considered equal? Main part of the lecture demonstrates recent results coming from the algebraic treatment of the problem, and in particular, connection of the concept of Frobenius algebras with the issue of proof identity in classical logic. Frobenius algebras have been subject to intensive investigation in mathematical physics following the realization of their connection to topological quantum field theories. In logic, these algebraic structures lead to a novel approach to standard questions of proof theory and a concept of resources for Gentzen type systems for classical logic. The material to be presented is a part of the lecturers PhD thesis defended last November at the INRIA institute in Nancy, France.
08.12.2011.

Milena Vujošević  Janičić , Faculty of Mathematics, University of Belgrade
Title: LAV: System for Automated Bug FindingAbstract:
In this talk design and evaluation of LAV will be presented. LAV is a new opensource tool for statically checking program assertions and errors. It integrates into the popular LLVM infrastructure for compilation and analysis. LAV uses symbolic execution to construct a firstorder logic formula that models the behavior of each basic blocks. LAV models the relationships between basic blocks using propositional formulas. It uses underapproximating or overapproximating unrolling to handle loops. LAV can pass generated verification conditions to one of the several SMT solvers: Boolector, MathSAT, Yices, and Z3. Our experiments with small 200 benchmarks suggest that LAV is competitive with related tools, so it can be used as an effective alternative for certain verification tasks. The application of LAV in education will also be presented. 
Mladen Nikolić, Faculty of Mathematics, University of Belgrade
Title: Algebraic resource semantics of proofs in classical logicAbstract:
Programs of a purely functional programing language / terms of lambda calculus are in relation to formal proofs in (intuitionistic) logic through the CurryHoward correspondence. General proof theory is a discipline of mathematical logic which investigates precisely those formal proofs as formal mathematical objects. While the notion of a formal proof is well defined, nearly a century of the development of the discipline has failed to provide an answer to the central open problem of the general proof theory  when are two given proofs considered equal? Main part of the lecture demonstrates recent results coming from the algebraic treatment of the problem, and in particular, connection of the concept of Frobenius algebras with the issue of proof identity in classical logic. Frobenius algebras have been subject to intensive investigation in mathematical physics following the realization of their connection to topological quantum field theories. In logic, these algebraic structures lead to a novel approach to standard questions of proof theory and a concept of resources for Gentzen type systems for classical logic. The material to be presented is a part of the lecturers PhD thesis defended last November at the INRIA institute in Nancy, France.
24.11.2011.

Ivan Petrović , Faculty of Mathematics, University of Belgrade
Title: Implementation of Wu's method for Automated Theorem Proving of geometry theorems in OpenGeoProver GATPAbstract:
Wu's method is one among most efficient methods of automated theorem proving for geometry theorems. Implementations of certain algorithms (e.g. triangulation of a polynomial system or pseudo division of two polynomials) are pretty sensitive  therefore it is necessary to carefully write them in order to obtain results of Wu's method the best way is possible. I will represent ideas taken from existing C++ implementation of Wu's prover as well as new ideas introduced with Java implementation of this prover. Special part of my lecture will be devoted to methods of input geometry problem transformation to algebraic form and challenges of that piece of work. I will also shortly describe the algorithm of transformation of NDG conditions from polynomial to user readable form. Some examples of theorem proving by this prover will be shown. At the end I will describe tips for the future work: integration with GeoGebra system for interactive geometry, work on parallel algorithms, integration with Isabelle/HOL system, problems that include conic sections and theorems that are consequences of Axioms of Order (extended versions of Wu's method), implementation of various heuristics for the point instantiation and for choosing the best way of proving a theorem, ideas for applying Wu's method in problems from hyperbolic geometry etc. 
Danijela Petrović, Filip Marić, Faculty of Mathematics, University of Belgrade
Title: Formal verification of an algorithm for reducing geometric statements to algebraAbstract:
Most efficient automated theorem provers in geometry are based on algebraic methods. In this talk, we describe first steps of the project that aims to formally prove connections between algebraic methods and synthetic geometry. First step when applying algebraic methods is to reduce the geometric problem that is being solved to algebra (i.e., to a system of polynomial equations). A reduction algorithm has been implemented in proof assistant Isabelle/HOL and its connections to analytic geometry have been formally proved.
03.11.2011.

Tijana Šukilović, Faculty of Mathematics, University of Belgrade
Title: Circle detection using discrete curvatureAbstract:
In this talk is defined notion of discrete curvature associated to a black pixel of black and white raster image. Possible areas of its application include detection of arbitrary shapes, especially those consisting of piecewise smooth curves. Using the discrete curvature approach, we describe and implement an algorithm for circle and circular arc detection, and compare it to the generalized Hough transform. 
Predrag Janičić, Faculty of Mathematics, University of Belgrade
Title: Automated Reasoning: Some Successes and New ChallengesAbstract:
In this talk, a brief account of some areas of automated reasoning will be given. Some historical remarks will be given along with an overview of some of the most significant results and current challenges.
The same material was presented as an invited talk at the conference CECIIS 2011.
29.06.2011.

Predrag Janičić, Faculty of Mathematics, University of Belgrade
Title: Report on visit to EPFL university and participation in SuRI conferenceAbstract:
The visit to the LARA group (Lab for Automated Reasoning and Analysis) and the participation at SUmmer Research Institute (SURI), both at EPFL (Lausanne, Switzerland) will be briefly discussed. 
Filip Marić, Faculty of Mathematics, University of Belgrade
Title: Report on participation in "SAT/SMT Summer School" 
Mladen Nikolić, Faculty of Mathematics, University of Belgrade
Title: Relation of some concepts of machine learning and philosophy of scienceAbstract:
Notion of generalization is central for both machine learning and empirical sciences. Although these disciplines study it separately, there are interesting connections between both concepts used in these disciplines and conclusions that are drawn. Most interesting connection is between the notions of VC dimension and structural risk minimization on the one side and Poperian falsifiability and Ocam's razor on the other.
29.12.2010.

Aleksandar Zeljić, Faculty of Mathematics, University of Belgrade
Title: Reduction from SAT problem to clique problem and vice versaAbstract:
This talk will present reduction of SAT problem to clique problem and several approaches to reduce clique problem to SAT problem. Also, a measure for comparison of reductions to SAT problem will briefly described. 
Vesna Pavlović, Faculty of Mathematics, University of Belgrade
Title: Solving geometric construction problemsAbstract:
In this talk, I will briefly present our current work in the area of solving geometric construction problems. Method that we use is based on the combination of forward and backward chaining and it keeps control on depths.
15.12.2010.

Nikola Jelić, Faculty of Mathematics, University of Belgrade
Title: Combining analytical and inductive methods of machine learningAbstract:
The area of machine learning came into being together with the first electronic computers. As soon as the power of the machine to do complex calculations was made apparent, question was raised of the ability of the machine to not only process the data, but to learn from it.
Question of possibility of the machine to learn, and therefore help, and later even replace human in tasks of increased complexity belongs not only to computer science. Replication of sensorycognitive process, which is a daily phenomenon in living creatures has great importance for biology, psychology, medicine, and the area of machine learning borrows from these and many other disciplines in order to describe different approaches to the problem with greater accuracy.
Two dominant approaches have emerged during the years: inductive, based on statistics and others methods of approximation, and analytical, based on mathematical logic and deduction. Theoretical foundation of these approaches determined the use of methods of machine learning. Inductive methods are very robust against errors in training data, they can do well with minimum domain theory and are able to reasonably well approximate solutions for problems which do not have single optimal solution. On the other hand, analytical methods are capable of giving solutions which fit perfectly in theoretical boundaries, given perfect domain theory and consistent rules of derivation.
In practice, many problems fail to be categorized in one of the two groups, because they share some properties with both. Appropriately, the need has arose for methods of machine learning which will be able to integrate both approaches, and in doing so alleviate the weaknesses and emphasize advantages of both methodologies.
Combined methods of machine learning have showed in practice that they are able to find better solutions in lesser time than purely intuitive or purely analytical methods, and that they are also able to compensate various deficiencies of these approaches. 
Mladen Nikolić, Faculty of Mathematics, University of Belgrade
Title: Report on visit to LARA groupAbstract:
In this talk, I will briefly present the work of the members of LARA (Laboratory of Automated Reasoning and Analysis) group from EPFL. Also, I will talk about new ideas of possible cooperation and personal impressions which emerged during the visit to that group.
24.11.2010.

Danijela Petrović, Faculty of Mathematics, University of Belgrade
Title: Groebner basesAbstract:
In the beginning of the section will be shown basic features of term rewriting system. Then it will be presented ideal membership problem and it will be shown that this problem can effectively be solved using Groebner bases. In presentation it will also be shown how to generate Groebner bases from a given set of polynomials. At the end of the talk it will be discussed example of using Groebner bases in geometry. 
Filip Marić, Faculty of Mathematics, University of Belgrade
Title: Verified efficient unsatisfiability proof checking for SATAbstract:
In order to be used in realworld applications, SAT solvers must be trusted. One of the main approaches for achieving trusted solvers is to make solvers emit evidences for their claims (models for satisfiable and proofs for unsatisfiable instances), and checking these evidences by independent tools. Usual unsatisfiability proofs are series of resolution steps and they can be checked by very simple tools, but they usually consume much space and it is not always easy to modify SAT solvers so that they can emit this kind of proofs. Alternative proofs are so called clausal proofs. They usually consume significantly less space and they can be easily emitted by most modern SAT solvers. However, if efficient proof checking is required, tools that can check clausal proofs have to be rather complex and the question arises how can these tools be trusted. In this work we present a proof checker for clausal proofs implemented in Isabelle/HOL. Our preliminary experiments show that this fully verified checker manages to achieve the desired level of efficiency.
10.11.2010.

Vesna Pavlović, Faculty of Mathematics, University of Belgrade
Title: A report on participation of the members of ARGO group in ADG 2010Abstract:
In this talk we will briefly present impressions about participation in ADG conference which was held in Munich in July of this year. ADG conference is a leading conference in the area of automated reasoning in geometry and it takes place once in two years. 
Milan Banković, Faculty of Mathematics, University of Belgrade
Title: A report on participation of the members of ARGO group in this year's FLoCAbstract:
Federated Logic Conference (FLoC) is one of the greatest and the most significant scientific meetings devoted to mathematical logic and its bonds to computer science. The meeting takes place once in every four years and brings together several very significant conferences related to mathematical logic in computer science, as well as a great number of affiliated workshops. This year, FLoC took place in Edinburgh. This talk presents a short survey on participation of the members of ARGO Group in this year's FLoC. 
Mladen Nikolić, Faculty of Mathematics, University of Belgrade
Title: Measuring Similarity of Graphs and their Nodes by Neighbor MatchingAbstract:
The problem of measuring similarity of graphs and their nodes is important in a range of practical problems. There is a number of proposed measures, some of them being based on iterative calculation of similarity between two graphs and the principle that two nodes are as similar as their neighbors are. We present one novel method of that sort, with a refined concept of similarity of two nodes that involves matching of their neighbors. For this method the convergence has been proven it has been shown that it has some additional desirable properties that, to our knowledge, the existing methods lack. The method is illustrated on two specific problems and empirically compared to other methods.
23.06.2010.

Ivana Tanasijević, Faculty of Mathematics, University of Belgrade
Title: Applications of spatial reasoningAbstract:
This talk will present spatial reasoning from the view of its practical applicability. Through several examples will be illustrated how spatial aspect can be recognized in some tasks and how thay can be resolved using spatial reasoning. 
Mladen Nikolić, Faculty of Mathematics, University of Belgrade
Title: A Layman Introduction to Algorithmic Information TheoryAbstract:
In this talk, elementary concepts of algorithmic information theory will be described, some of those being Kolmogorov complexity, random strings, Omega number. Also the importance of these concepts for incompleteness of formal axiomatic systems will be discussed.
21.05.2010.

Florian Haftmann, Fakultät für Informatik, TU München, Filip Marić, Faculty of Mathematics, University of Belgrade
Title: Towards a verified parallel SAT solverAbstract:
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ć, Faculty of Mathematics, University of Belgrade
Title: Some news from the fields of geometrical reasoning and dynamic geometryAbstract:
The talk will discuss some recent activities related to geometrical reasoning and to dynamic geometry: about the conference CADGME (Hagenberg, July 2009) and AD+GG (Castro Urdiales, February 2010), and about the article "The Area Method  A Recapitulation" on the area method (the authors: Janicic, Narboux, Quaresma). 
Danijela Petrović, Faculty of Mathematics, University of Belgrade
Title: Introduction to Formal Theorem ProvingAbstract:
This talk will present Isabelle, programming language developed in order to make easier writing definitions, theorems, lemmas, by computer. In the beginning of the section will be shown basic features. After that it will be discussed examples containing proves of some lemmas from mathematical logic. Proves will be written in Isar, extension of Isabelle, that helps better understanding.
14.04.2010.

Milan Banković, Faculty of Mathematics, University of Belgrade
Title: SMT tutorialAbstract:
Satisfiability Modulo Theory (SMT) is a problem of deciding whether, for a given first order formula A, exists a model of a given theory T that satisfies the formula A. SMT solving for different theories finds its application in many areas from hardware and software verification, scheduling problems, to different optimization problems. In this talk a general overview of SMT problems and their solving will be given. First, a brief theoretical introduction will be presented. Then some common theories frequently appearing in SMT solving will be disscussed. Principles of modern SMT solvers will be presented, as well as their connection with SAT solving. Finally, a short overview of previous, current and future work of the Argo Group in the field of SMT solving will be presented. 
Mladen Nikolić, Faculty of Mathematics, University of Belgrade
Title: Some details of applied statisticsAbstract:
In this talk the notions of the pvalue and the effect size in statistical hypothesis testing will be described. Their role in practice will be discussed. Several correlation based effect size measures will be briefly explained. The difference between the frequentist and the Bayesian approach to probability and statistics will be discussed.
31.03.2010.

Djordje Stakić, Faculty of Mathematics, University of Belgrade
Title: Instancebased machine learningAbstract:
This talk will present methods of instancebased machine learning. These methods delay processing of training examples until they must label a new query instance. Significant representatives of these methods are: kNearest Neighbour Learning, Locally Weighted Linear Regression, Radial Basis Functions and Casebased Reasoning. 
Predrag Janičić, Sana Stojanović, Vesna Pavlović, Mladen Nikolić, Faculty of Mathematics, University of Belgrade
Title: Ideas for developing new theorem prover for coherent logicAbstract:
In this talk we will be briefly discuss existing theorem provers for coherent logic (fragment of firstorder logic in which many important theories can be expressed). One version of the prover is already developed within ARGO group and it is tested on theorems from geometry. It is based on approach called forward chaining which represents a good base for generating readable proofs. However, this approach is not powerful enough for proving hard theorems. The ideas how this approach could be extended using techniques from other domains (i.e. SAT solving), which could speed up the search significantly will be discussed and, also, how these techniques can be adapted to coherent logic.
30.12.2009.

Mladen Nikolić, Faculty of Mathematics, University of Belgrade
Title: Methodology of SAT solver comparisonAbstract:
Weighing improvements to modern SAT solvers, or comparison of two arbitrary solvers is a challenging, but important task. Relative performance of two solvers is usually assessed by running them on some set of SAT instances and comparing the number of solved instances and their running time in some simple manner. New, statistically founded methodology of their comparison will be presented. 
Mirko Stojadinović, Faculty of Mathematics, University of Belgrade
Title: Good quality research, publishing results in journals and good management skillsAbstract:
In this lecture I’ll present key problems regarding doing research, scientific writing, publishing and presenting results. Problems that also arise are how to successfully manage everything and how to write proposals for projects. I’ll briefly compare supervision and PhD studies in Great Britain and Serbia. I have learned about all this on lectures held by Prof. Steve Quarrie, Ministry of Science and Technological Development. Prof. Quarrie has got long experience in scientific writing and publishing results in journals, and he works as a reviewer in couple of international journals.
16.12.2009.

Bojan Marinković, Mathematical Institute of the Serbian Academy of Sciences and Arts
Title: DEUKS internship: On the Interconnection of Heterogeneous Overlay NetworksAbstract:
From February 27th till May 25th this year I stayed at Sophia Antipolis, France. During this period, I worked in LogNet team of INRIA Sophia Antipolis  Mediterrane, under supervision of Luigi Liquori, head of the team. This was opportunity for me to enter to the new field of my research  distributed systems. Final goal was to develop a software which will follow algorithm described in the paper: L. Liquori, C. Tedeschi, and F. Bongiovanni: BabelChord: a Social Tower of DHTBased Overlay Networks. In 14th Symposium on Computers and Communications (ISCC 2009). IEEE, 2009. Short paper. During this talk, it will be presented basics of overlay networks, distrubuited systems, chord and babelchord protocols. 
Aljoša Obuljen, Faculty of Mathematics, University of Belgrade
Title: A word alignment method based on bilingual corpora aligned at sentence levelAbstract:
Automatic word alignment is one of the crucial problems in the statistical approach to machine translation (SMT). Various methods have been proposed for this task yielding different results. In this paper, we propose a simple ranking method for word alignment given a bilingual corpus aligned at sentence level. The method can also be applied to corpora aligned at any other level, such as paragraph or even larger text segments, provided that a suficient amount of aligned text is available. In other words, the method is robust as to the granularity of alignment. For purposes of this work, the sentence level alignment has been chosen, as the standard alignment technique in SMT. A bilingual corpus of moderate size (approx. 1M words per language) has been used to obtain results  an aligned SerbianEnglish corpus of texts related to education, finance, health and law (SELFEH  SerbianEnglish Law Finance Education and Health), one of the numerous resources developed within the HLT Group at the University of Belgrade.
18.11.2009.

Vesna Pavlović, Faculty of Mathematics, University of Belgrade
Title: Report on a research visit to Polytechnical University of ValenciaAbstract:
Within Tempus DEUKS project I was staying at the Polytechnical University of Valencia, Spain, as a visiting researcher from May 1st till July 28th. The main topic of my work was automatic generation of linear elementary interpretations for proving termination of a given term rewriting system. In this lecture basics of term rewriting systems and methods for proving its termination will be presented, along with the specific problem I was working on. 
Ivana Tanasijević, Faculty of Mathematics, University of Belgrade
Title: Spatial representation and reasoningAbstract:
The need for spatial representation and reasoning has taken a special place in many spheres of Artificial intelligence. This presentation is an overview of basic concepts, where the emphasis is on the qualitative spatial representation and reasoning problems. How these problems can easily be transformed into the problem of consistency, it will be here a word about the approach of that particular problem.
04.11.2009.

Filip Marić, Faculty of Mathematics, University of Belgrade
Title: Report on attending the conferences SAT2009 and TPHOLs2009Abstract:
This talk will present impressions from the conferences SAT2009 (Swansea, United Kingdom) and TPHOLs2009 (Munich, Germany). The SAT conferences are dedicated to the theory and applications of satisfiability testing, and TPHOLs conferences are dedicated to formal and interactive theorem proving in higherorder logics. 
Mladen Nikolić, Faculty of Mathematics, University of Belgrade
Title: Introduction to geostatisticsAbstract:
Geostatistics is a part of statistics specialized for analysis and interpretation of spatial data. In this presentation basic prediction method will be shown. Also, it will be shown how geostatistic analysis can be performed using free tools like R, SAGA and Google Earth instead of using expensive commercial software.
17.06.2009.

Julien Narboux, University Louis Pasteur, Strasbourg
Title: Formalization and automation of geometric reasoning within the Coq proof assistantAbstract:
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ć, The Faculty of Mathematics, University of Belgrade
Title: Refactoring  improving the design of existing codeAbstract:
Refactoring is the process of changing a software system so that its outer functionality is not affected, but only the inner structure of the code is improved. This talk will (through a simple JAVA example) demonstrate the techniques of systematic code refactoring. Also, unit testing will be described and the idea of using design patterns as a form of "of the shelf solutions" for some software design problems will be introduced.
13.05.2009.

Gordana Pavlović Lažetić, Nenad Mitić, The Faculty of Mathematics, University of Belgrade
Title: nGram characterization and prediction of genomic islandsAbstract:
A novel, ngrambased method for analysis of bacterial genome segments known as genomic islands (GIs) will be presented. Identification of GIs in bacterial genomes is an important task since many of them represent inserts that may contribute to bacterial evolution and pathogenesis. Characterization of GIs is performed by ngram frequency distribution and a Zipflike analysis of overrepresented and underrepresented ngrams identified by a statistic based on the maximal order Markov model. The method is applied to strainspecific regions in the Escherichia coli O157:H7 EDL933 genome. It refines a characterization based on other compositional features such as G+C content and codon usage.
Ngrambased characterization of GIs gave rise to a method for GIs' prediction. Ngram distributions were combined by union and intersection and two measures defined for evaluating the results  recall and precision. Using the best criteria (by training on the Escherichia coli O157:H7 EDL933 genome), GIs were predicted for 14 Enterobacteriaceae family members and for 21 randomly selected bacterial genomes. These predictions were compared with results obtained from two existing databases of genomic and pathogenecity islands. The results obtained show that application of ngrams improves both relative precision and recall.
The results presented are published in two articles [1], [2].
The presentation will skim the authors' previous work in bioinformatics, as well as their ongoing research.
References:
[1] G.M. PavlovićLažetić, N.S. Mitić, M.V. Beljanski: nGram characterization of genomic islands in bacterial genomes, Computer methods and programs in biomedicine, 93 (2009) 241256.
[2] N.S. Mitić, G.M. PavlovićLažetić, M.V. Beljanski: Could ngram analysis contribute to genomic island determination?, Journal of Biomedical Informatics, 41(6) (2008) 936943.
29.04.2009.

Tihomir Gvero , Miloš Gligorić
Title: UDITA: Unified Declarative & Imperative Test AbstractionsAbstract:
Test abstractions are highlevel descriptions of testing problems from which tools can automatically generate a concrete set of tests. Previous research has developed separate approaches for generating tests from 1) declarative and 2) imperative test abstractions. These two approaches show their strengths in different kinds of test abstractions. Developers are currently forced to choose one of these approaches, making certain aspects of complex test abstraction awkward to describe or inefficient to execute.
This paper presents UDITA, a new framework that unifies both declarative and imperative test abstractions using a nondeterministic Java extension. To make test generation using this approach efficient, we leverage the ideas of delayed non deterministic choice in model checking, and develop new algorithms for delayed generation of linked structures. We describe an implementation of our approach in Java PathFinder (JPF), a popular model checker for Java programs. We evaluate our technique by generating tests for a number of data structures, for refactoring engines, and for JPF itself. Our experimental results show that test generation using this approach is practical, leading to test abstractions that can be easier to write and offer faster generation than in previous frameworks. The results show our delayed optimization technique to be essential for making test generation feasible. The experiments revealed several previously unknown bugs in Eclipse, NetBeans, and JPF. 
Predrag Janičić, The Faculty of Mathematics, University of Belgrade
Title: Using lemmas in algebraic methods for geometry theorem provingAbstract:
There are several very efficient algebraic methods for geometry theorem proving and several implementations of these methods. However, none of them address the problem of lemma invocation and the proving process always starts from a scratch, without using knowledge built so far. In this talk, one idea for using lemmas and a plan how to incorporate it in the system GCLC will be discussed.
16.04.2009.

Srdjan Vesić, Paul Sabatier University, Toulouse
Title: An abstract argumentation framework for decision makingAbstract:
In this work, we propose a novel approach for argumentationbased decision making. We suggest a Dung style general argumentation framework that takes as input different arguments, defeat and preference relations among them, and returns as outputs a status for each option, and a total preordering on a set of options.
We study a particular class of this general framework, the one that privileges the option that is supported by the strongest argument, provided that this argument survives to the attacks. The properties of the system are investigated, and the revision of the status of a given option in light of a new argument is studied. 
Jasmina Lazić , Brunel University, UK , Mathematical Institute of the Serbian Academy of Sciences and Arts, Belgrade
Title: Variable Neighbourhood Decomposition Search for 01 Mixed Integer ProgramsAbstract:
In this paper we propose a new hybrid heuristic for solving 01 mixed integer programs based on the variable neighbourhood decomposition search principle. It combines variable neighbourhood search with generalpurpose CPLEX MIP solver. We perform systematic hard variables fixing (or diving) following the variable neighbourhood search rules. Variables to be fixed are chosen according to their distance from the corresponding linear relaxation solution values. If there is an improvement, variable neighbourhood descent branching is performed as the local search in the whole solution space. Numerical experiments have proven that by exploiting boundary effects in this way, solution quality can be considerably improved. With our approach, we have managed to improve the best known published results for 8 out of 29 instances from a wellknown class of very di±cult MIP problems. Moreover, computational results show that our method outperforms CPLEX MIP solver, as well as three other recent most successful MIP solution methods.
01.04.2009.

Damjan Krstajić, Research Centre for Cheminformatics
Title: The process of drug discovery and possibilities of application of automated reasoning in that processAbstract:
The process of drug discovery is an iterative process which can be seen as a multiobjective optimisation. The simple layout of the process will be presented using mainly mathematical terms. Some ideas regarding the implementation of SAT solvers in this field will be presented. The aim of the presentation is to start a discussion on possibilites of implementing SAT solvers in drug discovery. 
Filip Marić, The Faculty of Mathematics, University of Belgrade
Title: An Example of Natural Language Parsing by reduction to SATAbstract:
This lecture will present a method of parsing natural language by using a SAT solver. Parsing is based on the "link grammar" formalism  to each lecture in a sentence a number of possible connectors is assigned (based on its dictionary description) and the task is to connect all the words in a sentence and form a linkage which satisfies some predetermined citeria. The approach that is going to be presented encodes the linking constraints by a SAT formula and uses a SAT solver to construct its models. Models correspond to valid linkages, i.e., to the correct parses of the sentence. This project was a part of Google Summer of Code in 2008., and further work on this project is expected.
18.03.2009.

Sana Stojanović, Vesna Pavlović, The Faculty of Mathematics, University of Belgrade
Title: Tutorial: Coherent LogicAbstract:
In this talk we will briefly present coherent logic (sometimes referred to as "geometry logic") and its properties. Over the last fifteen years it has been used in several frameworks for proving geometrical theorems in traditional way. We will also discuss how the theorem prover that we are developing relates to coherent logic and other systems that use it. 
Saša Malkov, The Faculty of Mathematics, University of Belgrade
Title: A Reexamination of Correlations of Amino Acids with Particular Secondary StructuresAbstract:
The correlations of primary and secondary structures of proteins were analyzed using a data set from the Protein Data Bank. The correlation values of the amino acids and the eight secondary structure types were calculated, where the position of the amino acid and the position in sequence with the particular secondary structure differ at most 25. Clear preferences of amino acids towards certain secondary structures classify amino acids into four groups: αhelix preferrers, strand preferrers, turn and bend preferrers, and His and Cys (the latter two amino acids do not show clear preference for any secondary structure). Amino acids in the same group have similar structural characteristics at their Cβ and Cγ atoms that predicts their preference for a particular secondary structure. All αhelix preferrers have neither polar heteroatoms on Cβ and Cγ atoms nor, branching nor aromatic group on the Cβ atom. All strand preferrers have aromatic groups or branching on the Cβ atom. All turn and bend preferrers have polar heteroatom on Cβ or Cγ atoms or do not have a Cβ atom at all. These new rules can be helpful in making predictions about nonnatural amino acids. The results show that the substituents on Cβ or Cγ atoms of amino acid play major role in their preference for particular secondary structure at the same position in the sequence, while the polarity of amino acid has significant influence on αhelices and strands at some distance in the sequence. The diagrams corresponding to polar amino acids are noticeably asymmetric.
25.02.2009.

Aljoša Obuljen
Title: Tutorial: Bayesian learningAbstract:
This article represents a brief overview of Bayesian learning. Bayesian approach to machine learning is appropriate when data analysis and decision making should be done based on probability theory. This approach is important both for using probability theory to determine relevance of data in favor of some hypothesis, as well as to analyze and compare other methods of machine learning. 
Predrag Janičić, The Faculty of Mathematics, University of Belgrade
Title: Uniform reduction of hard problems to SATAbstract:
In this talk, a uniform approach for reducing hard problems to SAT will be presented. The approach uses the idea of operator overloading in objectoriented programming. The approach has already been applied to cryptoanalitical problems (joint work with Dejan Jovanovic and Milan Sesum). It will be described how additional types of problems, with a special emphasis on NPcomplete problems, can be addressed in a similar same way.
30.01.2009.  31.01.2009.
24.12.2008.

Staša Vujičić, The Faculty of Mathematics, University of Belgrade
Title: Tutorial: Genetic algorithmsAbstract:
Genetic algorithms provide an approach to learning that is based on simulated evolution. Hypotheses are often described by bit strings whose interpretation depends on the application, though hypotheses may also be described by symbolic expressions or even computer programs. The search for an appropriate hypothesis begins with a population, or collection, of initial hypotheses. Members of the current population give rise to the next generation population by means of operations such as random mutation and crossover, which are patterned after processes in biological evolution. At each step, the hypotheses in the current population are evaluated relative to a given measure of fitness, with the most fit hypotheses selected probabilistically as seeds for producing the next generation. Genetic algorithms have been applied successfully to a variety of learning tasks and to other optimization problems. For example, they have been used to learn collections of rules for robot control and to optimize the topology and learning parameters for artificial neural networks. This paper covers both genetic algorithms, in which hypotheses are typically described by bit strings, and genetic programming, in which hypotheses are described by computer programs. 
Bojan Marinković, Mathematical Institute of the Serbian Academy of Science and Arts
Title: A Logic with a Conditional Probability OperatorAbstract:
In August 2008, summer school ESSLLI 2008 took place at Hamburg. Group of young researchers of the Mathematical Institute of the Serbian Academy of Science and Arts presented their paper during student session of ESSLLI. In this talk, that paper is going to be presented. It presents a sound and strongly complete axiomatization of the reasoning about linear combinations of conditional probabilities and decidability with a PSPACE containment for the decision procedure. Also, the information on ESSLLI summer school is going to be given.
03.12.2008.

Predrag Janičić, The Faculty of Mathematics, University of Belgrade
Title: Visit to University of Rome and presentation of the GCLC packageAbstract:
In this talk, a recent visit to the Department of Mathematics at the University of Rome will be discussed. Two lectures on GCLC given there will be briefly repeated. Special attention will be given to possible directions for further improvements of GCLC. 
Panel discussion: Current research issues
Discussion on current and planned research problems, especially about aspects relevant for new postgraduate students.
19.11.2008.

Mladen Nikolić, The Faculty of Mathematics, University of Belgrade
Title: Tutorial: Linear regression and its application in SAT solver improvementAbstract:
Regression is a way of estimating a function that approximately defines a relationship between two random variables. Usually such a function is determined by a set of parameters for which suitable values should be chosen. The choice is made based on given training data. If all feasible functions are linear in its parameters regression is called linear. This problem is usually solved by minimization of mean squared error using the method of the least squares with optional problem regularization. One application of linear regression is prediction of solving time for discrete problems like SAT based on characteristics of problem instance. Milan Banković, The Faculty of Mathematics, University of Belgrade
Title: Alldifferent SMT solversAbstract:
Constraint programming is research area with growing importance in recent years due to its flexibility and broad application area. It is declarative programming style in which problem is defined by set of constraints the problem's solution must satisfy. To solve this kind of problem means finding values of variables that satisfy all the problem's constraints. One of the best known and the most common constraints is alldifferent constraint which restricts every two different variables in given set of variables not to take equal values. Special challenge is relating constraint programming to SAT problem, using SMT approach. In this talk, we will give a short overview of alldifferent constraint, relating it to the matching theory in bipartite graphs. We will establish relation between alldifferent constraint and SAT problem by representing alldifferent constraint as a SMT problem. Finally, we will propose an algorithm for generating explanations of theory propagations in alldifferent SMT solver.
05.11.2008.

Vesna Pavlović, The Faculty of Mathematics, University of Belgrade
Title: ICCL Summer school 2008, Dresden  trip reportAbstract:
Sixth ICCL summer school was held in Dresden from 24. August until 6. September and it was organized by TU Dresden. The main topic was the relationship between modern formal logic and common sense which characterize human reasoning. In this lecture the main ideas from this summer school will be presented in short. 
Damjan Krstajić, Research Centre for Cheminformatics
Title: Discovery Bus  a system for automating QSAR modellingAbstract:
There are many different methods and approaches to solve QSAR/statistical modelling problems. Regardless of our preference to a set of techniques, practice teaches us that there is no single bullet proof way to solve QSAR problems. On the other hand, in the age of highly automated laboratories there is a bombardment of new data and experimental results. The challenge is to design a system that will cope with constant influx of new information and to automate QSAR modelling without sacrificing the quality of predictions. Discovery Bus is our solution to the challenge. It is an implementation of Competitive Workflow, a novel software architecture, implemented using autonomous software agents.
18.06.2008.

Panel discussion  Current research issues
Research problems that we worked on during the past academic year, that we work on now, and that we are planning to work on.
04.06.2008.

Mladen Nikolić, The Faculty of Mathematics, University of Belgrade
Title: Methodology of Parameter Values Setting for SAT SolversAbstract:
Some aspects of SAT solver functioning can be defined by different parameters of those solvers. Performance of a solver depends on boolean formula being solved and on choice of it's parameter values. Therefore, a methodology for choosing parameter values is needed. Such a methodology should take into account properties of the problem instance being solved. Approach we take is based on representing formulae as graphs and using graph similarity measures in order to find good parameter values for solving the unknown formula. Those would be the values for which SAT solver efficiently solves the similar formulae. 
Vesna Pavlović, Sana Stojanović, The Faculty of Mathematics, University of Belgrade
Title: Formalization and Automation of Euclidean GeometryAbstract:
The idea of formalization of geometrical reasoning is present from recent days and it is still in its beginnings, so it presents the area which is expected to be in the focus in the following years. Some of the authors succeeded in formalizing one part of Hilbert's axioms, and also part of Tarski's axioms and in formalizing some of the theorems that belong to these groups of axioms. The objective of our research is automation of this process and obtaining along formal verification of the proof in Isabelle proof assistant.
14.05.2008.

Prof. Pedro Quaresma, University of Coimbra, Portugal
Title: Cryptology  a (very) Brief SurveyAbstract: 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

Predrag Janičić, The Faculty of Mathematics, University of Belgrade
Title: Intelligent Geometrical Software 
Vesna Pavlović, Sana Stojanović, The Faculty of Mathematics, University of Belgrade
Title: Formalization and Automation of Euclidean Geometry 
Predrag Janičić, The Faculty of Mathematics, University of Belgrade
Title: GCLC  lab session

16.04.2008.

Prof. Steve A. Quarrie, Director of the Consultative Bureau for International Projects, Ministry of Science, Serbia
Title: FP7 and looking for the truth: you mathematicians have it easy!Abstract:
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 postgraduate 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ć, The Faculty of Mathematics, University of Belgrade
Title: Tutorial: XML databasesAbstract:
For the past few years Extensible Markup Language (XML) has become dominant standard for describing and exchanging data over Internet. But on the other hand XML has introduced several new problems. The more pressing problems are how to store and manage XML data. Regarding rigidity of XML document structure, XML documents fall into two broad categories: datacentric and documentcentric. When dealing with datacentric XML documents, it is possible to convert XML documents into a relational database, which can then be queried using SQL. Such relational databases are called XMLenabled databases. Documentcentric XML documents are those characterized by irregular structure and mixed content. The best choice for storing, updating and retrieving these kind of XML documents is usually a native XML database (NXD). Basic characteristics of an NXD are the following: A logical unit of an NXD is an XML document or its rooted part, and it corresponds to a row in a relational database.
 It includes at least the following components: elements, attributes, textual data (PCDATA), and document order.
 Physical model (and type of persistent NXD storage) is unspecified.
NXDs store XML documents as logical units, and retrieve documents using specific query languages such as XPath or XQuery.

Vladan Radivojević
Title: Small deductive systemsAbstract:
One way to formulate propositional logic is the L theory which consists of one rule of inference and three axioms over two connectives. There are smaller axiomatic systems equivalent to the L theory with the same rule of inference and same set of connectives. For instance, the system which was discovered by C.A. Meredith in 1953. consists of only a single axiom. In 1917. J. Nicod discovered even simplier system with the single axiom schema in which the only connective is the Sheffer stroke.
This article is about these "small" axiomatic systems and about some properties of formulas with the Sheffer stroke.
12.03.2008.

Bojan Marinković, Mathematical Institute of the Serbian Academy of Sciences and Arts
Title: Tutorial: An Introduction to the Analysis of AlgorithmsAbstract:
Cause of this lecture is to present an oversee of the book "An Introduction to the Analysis of Algorithms" of R. Sedgewick and P. Flajolet. This lecture is part of exam for post graduated course "Theoretical computer science" at The Faculty of Mathematics of University of Belgrade. 
Petar Maksimović, Mathematical Institute of the Serbian Academy of Sciences and Arts
Title: Simple Characterization of Functionally Complete OneElement Sets of Propositional ConnectivesAbstract:
A set of propositional connectives is said to be functionally complete if all propositional formulae can be expressed using only connectives from that set. In this paper we give sufficient and necessary conditions for a oneelement set of propositional connectives to be functionally complete. These conditions provide a simple and elegant characterization of functionally complete oneelement sets of propositional connectives (of arbitrary arity).
29.01.2008.  01.02.2008.

Workshop on Formal Theorem Proving

Filip Marić, The Faculty of Mathematics, University of Belgrade
Title: Formal Verification of SAT Solvers 
Predrag Janičić, The Faculty of Mathematics, University of Belgrade
Title: ARGO Group Presentation

16.01.2008.

Goran Predović, Microsoft Development Center Serbia
Title: Tutorial: Automated Geometry Theorem Proving using Algebraic MethodsAbstract:
Although the connection between geometry and algebra is determined in seventeenth century (Rene Dekart), theory for proving geometry theorems that are formulated using algebraic notations was developed only at the end of the twentieth century. At that time, successful results were reported by the Chinese mathematicians WenTsus Wu. Algebraic methods proved to be very powerful, able to prove hundreds of nontrivial geometry theorems and discovering new ones. First part of the lecture is basic introduction into Automated Geometry Theorem Proving. Second part of the lecture is the presentation of the two most successful algebraic methods  Wu's method and the Groebner basis method. Finally, integration of the implemented geometry provers into GCLC system will be demonstrated. 
Filip Marić, The Faculty of Mathematics, University of Belgrade
Title: Automatic Timetabling by using a SAT encodingAbstract:
This lecture will describe a case study of automated timetabling on Faculty of Mathematics. Conditions of timetable are encoded with a propositional formula and a SAT solver is used to find its models, which represent valid timetable solutions.
26.12.2007.

Vesna Pavlović, The Faculty of Mathematics, University of Belgrade
Title: Tutorial: Type TheoryAbstract:
Constructive type theory represents, on one hand, the framework which joins logic and programming languages in one elegant way; that way program development and its verification may execute as one system. On the other hand, type theory may be considered as a functional programming language with some new properties. Under certain conditions it is possible to define a system which is a logical system and programming language all in one, and within which statements and types are equivalent, as if the proofs of the statements and elements of types.
In this lecture we are going to consider some basic facts about constructive logic, untyped and typed lambda calculus, and after that we are going to see what are the rules that form a basis of a type theory, and to learn some basic facts and propositions of the type theory, ending with Curry Howard isomorphism. 
Milena VujoševićJaničić, The Faculty of Mathematics, University of Belgrade
Title: Automated Detection of Buffer Overflows in Programming Language CAbstract:
Automated detection of buffer overflow bugs in C programs is very important problem because buffer overflows are suitable targets for security attacks and sources of serious programs' misbehavior. Buffer overflow bugs can be detected in runtime by dynamic analysis of the program being executed, and before runtime by static analysis of the source code. In this talk we will present our new static system for automated detection of buffer overflows. The system is flowsensitive and interprocedural, and it deals with both statically and dynamically allocated buffers. Its architecture is flexible and pluggable. For instance, the system uses an external and easyextendable knowledge database that stores all the reasoning rules so they are not hardcoded within the system. Also, for checking generated correctness and incorrectness conditions, any external automated theorem prover that follows SMTLIB standards can be used. We will also report on our prototype implementation  the FADO tool.
5.12.2007.

Milan Banković, The Faculty of Mathematics, University of Belgrade
Title: Tutorial: Analysis of Algorithms  practical approachAbstract:
When algorithms are analysed in practice, it is very important to estimate expected execution time and examine the algorithm's average behavior. The average case analysis is, in most cases, more complexed, compared to the worst case analysis, and more advanced mathematical tools must be developed. In this talk we will illustrate generating functions and their application to analysis of algorithms. Generating functions are usually related to enumeration theory and combinatorics, which is the essence of the average case analysis. We will introduce the symbolic method, an intuitive method that binds sets of combinatorial objects to generating functions that enumerates them. Application of generating functions to solving of recurrence relations will also be considered. 
Vesna Pavlović, The Faculty of Mathematics, University of Belgrade
Title: Phase transition in kGDSAT problemAbstract:
kGDSAT problem denotes the class of random SAT problems with geometrical distribution of clause length with parameter p (0 < p <= 1); for the value p = 1 it becomes the kSAT model. Friedgut made a huge breakthrough with a proof of existence of nonuniform satisfiability threshold, i.e. array r(n) around which probability of satisfiability of a formula goes from one to zero. Our goal is to prove the same thing for the kGDSAT problem  i.e. that kGDSAT has a sharp threshold for every value of parameter p and thus (keeping in mind that kSAT problem is a subclass of the kGDSAT problem for the value p = 1) to extend the class of SAT problems for which this statement hold.
14.11.2007.

Filip Marić, The Faculty of Mathematics, University of Belgrade
Title: Tutorial: Formalization of propositional logic within the system IsabelleAbstract:
This lecture will introduce the basics of proof assistant Isabelle. The Isabelle/HOL system one of the most widely used tools for formal theorem proving, developed at University of Cambridge (Larry Paulson) and TU Munich (Tobias Nipkow). System allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. This lecture will show the use of Isabelle through using the propositional logic as an example. The notions of propositional variables, literals, formulas and valuations, and the satisfiability relation will be defined and some of their basic properties will be formally proved. 
Claudio Castellini, LIRALab, University of Genova, Italy
Title: Machine Learning for Hand Prosthetics (and more)Abstract:
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ć, The Faculty of Mathematics, University of Belgrade
Title: Tutorial: Machine LearningAbstract:
Machine learning is a field concerned with study of generalization and construction and analysis of algorithms that can generalize. Machine learning can often be seen as an approximation of goal function (function that is to be learned) or as a data driven search of hypotheses space. Choice of hypotheses space is crucial for successive learning, and quality of that choice can be estimated based on VapnikChervonenkis (VC) dimension of that space. VC dimension describes adaptability of hypotheses to data. High VC dimension of hypotheses space leads to well known problem of overfitting. A way to solve this problem and to achieve good generalization is outlined by statistical learning theory through structural risk minimization principle. 
Filip Marić, The Faculty of Mathematics, University of Belgrade
Title: SMT solvers and ArgoLibAbstract:
Satisfiability Modulo Theories (SMT) problem is a decision problem for logical formulas with respect to combinations of background theories expressed in classical firstorder logic with equality. Examples of theories typically used in computer science are the theory of real numbers, the theory of integers, and the theories of various data structures such as lists, arrays, bit vectors and so on. This lecture will give a brief introduction to SMT problem and the SMT solver ArgoLib. 
Saša Misailović, School of Electrical Engineering, University of Belgrade
Title: Automated testinput generation using imperative predicatesAbstract:
Korat is tool for constraintbased generation of structurally complex test inputs. Korat performs boundedexhaustive generation  it generates all structures up to the given bound on their size. Properties of desired test inputs are specified as imperative predicate, in the form of Java code. User also bounds the size of state space through finitization, which specifies possible values for the fields of the structure. Korat performs search of bounded state space and efficiently generates all nonisomorphic structures with desired properties. More informations about Korat can be found at http://korat.sourceforge.net/ .
17.10.2007.

Filip Marić, The Faculty of Mathematics, University of Belgrade
Title: Tutorial: SAT solversAbstract:
Propositional satisfiability problem (SAT) is the problem of deciding if there is a truth assignment under which a given propositional formula (in conjunctive normal form) evaluates to true. It is a canonical NPcomplete problem and it holds a central position in the field of computational complexity. SAT problem is also important in many practical applications such as electronic design automation, software and hardware verification, artificial intelligence, and operational reesearch. Thanks to recent advances in propositional solving technology, SAT solvers are becoming the tool for atacking more and more practical problems. This lecture will introduce the basic algoritms and data structures used in modern SAT solvers. 
Mladen Nikolić, The Faculty of Mathematics, University of Belgrade
Title: New Measures of Similarity of Graph nodes and Whole GraphsAbstract:
A number of methods for computing graph similarity, already exists. One approach is to estimate similarity of graph nodes. Method of Decoupled Similarities is a new method for calculating similarity of graph nodes. On some problems, this method exhibits advantages over already existing ones, but it can also be used to solve problems that existing methods can not solve. It's most important advantage is that it enables construction of measure of similarity of whole graphs based on calculated similarities of their nodes. First results are very encouraging.