Seminars

Links' Seminars and Public Events Add to google calendar
2017
Fri 3rd Nov
10:30 am
12:00 pm
Add event to google
Joanna Ochremiak, Paris 7: "Proof complexity of constraint satisfaction problems"
Many natural computational problems, such as satisfiability and
systems of equations, can be expressed in a unified way as constraint
satisfaction problems (CSPs). In this talk I will show that the usual
reductions preserving the complexity of the constraint satisfaction
problem preserve also its proof complexity. As an application, I will
present two gap theorems, which say that CSPs that admit small size
refutations in some classical proof systems are exactly the constraint
satisfaction problems which can be solved by Datalog.

This is joint work with Albert Atserias.

Show in Google map
B21
Fri 13th Oct
11:00 am
1:00 pm
Add event to google
Dimitri Gallois: On parallel rewriting
Show in Google map
B21
Fri 29th Sep
10:00 am
12:00 pm
Add event to google
Nicolas Bacquey: "An algorithm for deciding the equivalence of tree transducers"
As an extension of word transformations, tree transformations have numerous applications in computer science : XSLT transformations, Unix packages installation and removal, databases queries... Likewise, there are many formal models to describe these transformations. However, the proof of formal properies on these models is often difficult, or even undecidable.
In this talk, I will be interested in one of the simplest model for tree transformations, namely deterministic top-down tree transducers (DTOP). It has been known for a while that the equivalence problem of DTOPs can be solved via an earliest normal form comparison algorithm, that is in 2EXPTIME. However, when applying this algorithm to practical cases, it seemed that the worst case was not bound to happen often, if ever.
I will present a new algorithm for the problem, based on the search of counterexamples via the expansion and unification of a set of rules over states of DTOPs. The most interesting feature of this algorithm is that it runs in exponential time, thus proving that the equivalence problem of DTOPs is in fact EXPTIME-complete.

Show in Google map
Lille B31
Thu 6th Jul
 all day
Add event to google
ANR Headwork: General Meeting
Show in Google map
Rennes
Fri 16th Jun
 all day
Add event to google

09h15-09h45 Coffee Welcome
09h45-10h30 Michel de Rougemont: Approximate integration of streaming graph edges
10h30-11h15 Florent Cappelli: Understanding the complexity of #SAT using knowledge compilation
11h15-11h45 Yann Strozecki: Enumerating maximal solutions of saturation problems
12h00 Lunch
14h00 Discussion libre
16h00 End
Show in Google map
Inria Lille
Thu 15th Jun
 all day
Add event to google
09h15-09h45 Welcome coffee
09h45-10h30 Pierre Bourhis: Introduction of circuit from database queries
10h30-11h15 Jen Keppeler: Answering FO+MOD queries under updates on bounded degree databases
11h15-12h00 Antoine Amarilli: Enumeration of valuation of circuits
12h00-13h30 Lunch + Café
13h30-14h30 Jan Ramon: Question around IA
14h30-15h15 Ahmet Kara: Covers of Query Results
15h15-15h45 Break
15h45-16h30 Alexandre Vigny: Constant delay enumeration for FO queries over
databases with local bounded expansion

20h00 Dinner at Le Palermo
Show in Google map
Inria Lille
Fri 9th Jun
10:30 am
12:30 pm
Add event to google
Valentin Montmirail: "A Recursive Shortcut for CEGAR: Application to the Modal Logic K Satisfiability Problem"
Counter-Example-Guided Abstraction Refinement (CEGAR) has been very successful in model checking.
Since then, it has been applied to many different problems. It is especially proved to be a highly successful practical approach for solving the PSPACE complete QBF problem. In this paper, we propose a new CEGAR-like approach for tackling PSPACE complete problems that we call RECAR (Recursive Explore and Check Abstraction Refinement). We show that this generic approach is sound and complete. Then we propose a specific implementation of the RECAR approach to solve the modal logic K satisfiability problem. We implemented both CEGAR and RECAR approaches for the modal logic K satisfiability problem within the solver MoSaiC. We compared experimentally those approaches to the state-of-the-art solvers for that problem. The RECAR approach outperforms the CEGAR one for that problem and also compares favorably against the state-of-the-art on the benchmarks considered.
"Lille-Salle B21"
Tue 6th Jun
to Fri 9th Jun
 all day
Add event to google
Visit of Jean-Marc Talbot, Université de Marseille

Fri 2nd Jun
 all day
Add event to google
Visit of Floris Geerts, University of Antwerp
Fri 21st Apr
 all day
Add event to google
Visit of Florent Capelli, London University

Lien Permanent pour cet article : https://team.inria.fr/links/fr/seminars/