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ć .


  1. Pavle Subotic, Amazon

    Title: Debugging Large Scale Logic Programs

    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.


  1. Marc Bezem, Institute for Informatics, University of Bergen, Norway

    Title: The Univalence Axiom in Dependent Type Theory

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


  1. Aleksandar Zeljić, Uppsala University

    Title: A Model-Constructing Approach to Solving Bit-Vector Constraints

    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.


  1. Julien Narboux, University of Strasbourg

    Title: GeoCoq, foundations of geometry formalized in Coq

    In this talk we will give an overview of the GeoCoq library developed by our team in Strasbourg ( ). 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.


  1. Tetsuo Ida, University of Tsukuba

    Title: Computational Origami System Eos

    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.

  2. Mircea Marin, West University of Timisoara

    Title: Solving, Reasoning, and Programming in Common Logic

    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.


  1. Pavle Subotić, University College London

    Title: Synthesizing Analyzers from Datalog

    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++.


  1. Marc Bezem, Institute for Informatics, University of Bergen, Norway

    Title: Coquand's site semantics of coherent logic

    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.


  1. Bojan Petrović, Haklab Belgrade

    Informal Verification

    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.


  1. Marc Bezem, Institute for Informatics, University of Bergen, Norway

    Title: Homotopy Type Theory

    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:


  1. Sana Stojanović, Faculty of Mathematics, University of Belgrade

    Title: A Vernacular for Coherent Logic and Automated Generation of Machine Verifiable and Readable Proofs

    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).

  2. Mirko Stojadinović, Faculty of Mathematics, University of Belgrade

    Title: Instance-based Selection of CSP Solvers using Short Training

    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

    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.


  1. Aleksandar Zeljic, Department of Information Technology, Uppsala University, Sweden

    Title: Approximations for Model Construction

    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 fo