ARGO

Automated reasoning group

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 e-mail to Vesna Marinković or Predrag Janičić .

13.2.2023.

Anna Petiurenko , Pedagogical University of Cracow, Poland
Title: 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, France
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
Title: Lightweight Typestate Analysis
Abstract:
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
Title: Dynamic Analysis and Test Generation for JavaScript
Abstract:
JavaScript has become one of the most prevalent programming languages. Unfortunately, some of the unique properties that contribute to this popularity also make JavaScript programs prone to errors and difficult for program analyses to reason about. These properties include the highly dynamic nature of the language, a set of unusual language features, a lack of encapsulation mechanisms, and the “no crash” philosophy. The goal of this talk is to present different dynamic program analyses and test generation techniques for improving the correctness, reliability, performance, and security of JavaScript-based software.
Pavle Subotić, Amazon
Title: Towards Verification of React Applications
Abstract:
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
Title: Monitoring of Cyber-Physical Systems for Correctness and Robustness
Abstract:
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
Title: Rational Inference Relations from Maximal Consistent Subsets Selection
Abstract:
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
Title: Extending First-order Theorem Prover to Higher-order Logic
Abstract:
Decades of work have gone into developing efficient proof calculi, data structures, algorithms, and heuristics for first-order automatic theorem proving. Higher-order provers lag behind in terms of efficiency. Instead of developing a new higher-order prover from the ground up, we propose to start with the state-of-the-art superposition-based prover E and gradually enrich it with higher-order features. We explain how to extend the prover’s data structures, algorithms, and heuristics to λ-free higher-order 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 higher-order logic

11.10.2018.

Pavle Subotic, Amazon
Title: Debugging Large Scale Logic Programs
Abstract:
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.3.2018.

Marc Bezem, Institute for Informatics, University of Bergen, Norway
Title: The Univalence Axiom in Dependent Type Theory
Abstract:
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 Model-Constructing Approach to Solving Bit-Vector Constraints
Abstract:
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.3.2017.

Julien Narboux, University of Strasbourg
Title: GeoCoq, foundations of geometry formalized in Coq
Abstract:
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 Eos
Abstract:
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
Title: Solving, Reasoning, and Programming in Common Logic
Abstract:
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
Title: Synthesizing Analyzers from Datalog
Abstract:
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
Title: Coquand's site semantics of coherent logic
Abstract:
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 Belgrade
Informal Verification
Abstract:
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, non-institutional setting.

22.07.2014.
24.07.2014.

Marc Bezem, Institute for Informatics, University of Bergen, Norway
Title: Homotopy Type Theory
Abstract:
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ć, Faculty of Mathematics, University of Belgrade
Title: A Vernacular for Coherent Logic and Automated Generation of Machine Verifiable and Readable Proofs
Abstract:
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: Instance-based Selection of CSP Solvers using Short Training
Abstract:
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 k-nearest 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 state-of-the-art tools used in comparison, and is comparable to classical methods that use long timeout during the training phase.
Title: Air Traffic Controller Shift Scheduling by Reduction to CSP, SAT and SAT-related Problems
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 SAT-related 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 Construction
Abstract:
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
Title: Combinatorial approaches in incidence projective geometry
Abstract:
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: Semi-interactive proofs within Tarski's geometry
Abstract:
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
Title: Guiding Craig Interpolation with Domain-specific Abstractions
Abstract:
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
Title: Phase Transitions in Random Constraint Satisfaction Problems: A Personal Perspective
Abstract:
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
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 constructions
Abstract:
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, December
Title: Tarski's and Hilbert's geometry
Abstract:

20.09.2012.

Tihomir Gvero, Ecole Polytechnique Federale de Lausanne (EPFL)
Title: Fast Code Completion using Type Inhabitation
Abstract:
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
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, Zhang
Abstract:
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 logic
Abstract:
Programs of a purely functional programing language / terms of lambda calculus are in relation to formal proofs in (intuitionistic) logic through the Curry-Howard 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 Finding
Abstract:
In this talk design and evaluation of LAV will be presented. LAV is a new open-source 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 first-order 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 logic
Abstract:
Programs of a purely functional programing language / terms of lambda calculus are in relation to formal proofs in (intuitionistic) logic through the Curry-Howard 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 GATP
Abstract:
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 algebra
Abstract:
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 curvature
Abstract:
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 Challenges
Abstract:
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 conference
Abstract:
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 science
Abstract:
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 versa
Abstract:
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 problems
Abstract:
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 learning
Abstract:
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 sensory-cognitive 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 group
Abstract:
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 bases
Abstract:
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 SAT
Abstract:
In order to be used in real-world 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 2010
Abstract:
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 FLoC
Abstract:
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 Matching
Abstract:
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 reasoning
Abstract:
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 Theory
Abstract:
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 solver
Abstract:
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 geometry
Abstract:
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 Proving
Abstract:
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 tutorial
Abstract:
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 statistics
Abstract:
In this talk the notions of the p-value 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: Instance-based machine learning
Abstract:
This talk will present methods of instance-based machine learning. These methods delay processing of training examples until they must label a new query instance. Significant representatives of these methods are: k-Nearest Neighbour Learning, Locally Weighted Linear Regression, Radial Basis Functions and Case-based 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 logic
Abstract:
In this talk we will be briefly discuss existing theorem provers for coherent logic (fragment of first-order 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 comparison
Abstract:
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 skills
Abstract:
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 Networks
Abstract:
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 DHT-Based 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 level
Abstract:
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 Serbian-English corpus of texts related to education, finance, health and law (SELFEH - Serbian-English 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 Valencia
Abstract:
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 reasoning
Abstract:
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 TPHOLs2009
Abstract:
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 higher-order logics.
Mladen Nikolić, Faculty of Mathematics, University of Belgrade
Title: Introduction to geostatistics
Abstract:
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 assistant
Abstract:
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 code
Abstract:
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: n-Gram characterization and prediction of genomic islands
Abstract:
A novel, n-gram-based 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 n-gram frequency distribution and a Zipf-like analysis of overrepresented and underrepresented n-grams identified by a statistic based on the maximal order Markov model. The method is applied to strain-specific 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.

N-gram-based characterization of GIs gave rise to a method for GIs' prediction. N-gram 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 n-grams 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: n-Gram characterization of genomic islands in bacterial genomes, Computer methods and programs in biomedicine, 93 (2009) 241-256.
[2] 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ć
Title: UDITA: Unified Declarative & Imperative Test Abstractions
Abstract:
Test abstractions are high-level 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 non-deterministic 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 proving
Abstract:
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 making
Abstract:
In this work, we propose a novel approach for argumentation-based 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 0-1 Mixed Integer Programs
Abstract:
In this paper we propose a new hybrid heuristic for solving 0-1 mixed integer programs based on the variable neighbourhood decomposition search principle. It combines variable neighbourhood search with general-purpose 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 well-known 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 process
Abstract:
The process of drug discovery is an iterative process which can be seen as a multi-objective 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 SAT
Abstract:
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 Logic
Abstract:
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 Structures
Abstract:
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 non-natural 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 learning
Abstract:
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 SAT
Abstract:
In this talk, a uniform approach for reducing hard problems to SAT will be presented. The approach uses the idea of operator overloading in object-oriented 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 NP-complete problems, can be addressed in a similar same way.

30.01.2009. - 31.01.2009.

Second Workshop on Formal and Automated Theorem Proving and Applications

24.12.2008.

Staša Vujičić, The Faculty of Mathematics, University of Belgrade
Title: Tutorial: Genetic algorithms
Abstract:
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 Operator
Abstract:
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 package
Abstract:
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 improvement
Abstract:
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 solvers
Abstract:
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 report
Abstract:
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 modelling
Abstract:
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 Solvers
Abstract:
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 Geometry
Abstract:
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 Survey
Abstract: 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
  Title: Intelligent Geometrical Software
2. Vesna Pavlović, Sana Stojanović, The Faculty of Mathematics, University of Belgrade
  Title: Formalization and Automation of Euclidean Geometry
3. 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 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ć, The Faculty of Mathematics, University of Belgrade
Title: Tutorial: XML databases
Abstract:
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: data-centric and document-centric. When dealing with data-centric 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 XML-enabled databases. Document-centric 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:
1. A logical unit of an NXD is an XML document or its rooted part, and it corresponds to a row in a relational database.
2. It includes at least the following components: elements, attributes, textual data (PCDATA), and document order.
3. 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 systems
Abstract:
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 Algorithms
Abstract:
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 One-Element Sets of Propositional Connectives
Abstract:
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 one-element set of propositional connectives to be functionally complete. These conditions provide a simple and elegant characterization of functionally complete one-element sets of propositional connectives (of arbitrary arity).

29.01.2008. - 01.02.2008.

Workshop on Formal Theorem Proving
1. Filip Marić, The Faculty of Mathematics, University of Belgrade
  Title: Formal Verification of SAT Solvers
2. 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 Methods
Abstract:
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 Wen-Tsus Wu. Algebraic methods proved to be very powerful, able to prove hundreds of non-trivial 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 encoding
Abstract:
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 Theory
Abstract:
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 C
Abstract:
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 run-time by dynamic analysis of the program being executed, and before run-time 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 flow-sensitive and inter-procedural, and it deals with both statically and dynamically allocated buffers. Its architecture is flexible and pluggable. For instance, the system uses an external and easy-extendable knowledge database that stores all the reasoning rules so they are not hard-coded within the system. Also, for checking generated correctness and incorrectness conditions, any external automated theorem prover that follows SMT-LIB 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 approach
Abstract:
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 k-GD-SAT problem
Abstract:
k-GD-SAT 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 k-SAT 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 k-GD-SAT problem - i.e. that k-GD-SAT has a sharp threshold for every value of parameter p and thus (keeping in mind that k-SAT problem is a subclass of the k-GD-SAT 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 Isabelle
Abstract:
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, LIRA-Lab, 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 Learning
Abstract:
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 Vapnik-Chervonenkis (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 ArgoLib
Abstract:
Satisfiability Modulo Theories (SMT) problem is a decision problem for logical formulas with respect to combinations of background theories expressed in classical first-order 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 test-input generation using imperative predicates
Abstract:
Korat is tool for constraint-based generation of structurally complex test inputs. Korat performs bounded-exhaustive 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 non-isomorphic 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 solvers
Abstract:
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 NP-complete 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 Graphs
Abstract:
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.

ARGO

Automated reasoning group

≡ Navigation

Argo Seminar: Announcements