Links' Seminars and Public Events |
Thu, July 6, 2017 all day | ANR Headwork: General Meeting Rennes |
Fri, June 16, 2017 all day | 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 Inria Lille |
Thu, June 15, 2017 all day | 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 Inria Lille |
Fri, June 9, 2017 10:30 am 12:30 pm | 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, June 6, 2017 to Fri, June 9, 2017 all day | Visit of Jean-Marc Talbot, Université de Marseille |
Fri, June 2, 2017 all day | Visit of Floris Geerts, University of Antwerp |
Fri, April 21, 2017 all day | Visit of Florent Capelli, London University |
Fri, March 24, 2017 all day | Visit of Charles Paperman, Université Paris 7 Université Paris 7 www.liafa.univ-paris-diderot.fr/~paperman/ INRIA Institut National Recherche Informatique Automatique 40 Avenue Halley, 59650 Villeneuve d'Ascq, France |
Wed, March 15, 2017 10:30 am 12:00 pm | Emmanuel Filliot, Université Libre de Bruxelles: "Automata, Logic and Algebra for Word Transductions" This talk will survey old and recent results about word transductions, i.e. functions mapping (finite) words to words. Connections between automata models (transducers), logic and algebra will be presented. Starting with rational functions, defined by (one-way) finite transducers, and the canonical model of bimachines introduced by Reutenauer and Schützenberger, the talk will also target the more expressive class of functions defined by two-way transducers and their equivalent MSO-based formalism. "Lille-Salle B21" |
Wed, March 15, 2017 all day | Visit of Emmanuel Filliot, Université Libre de Bruxelles |
Wed, February 1, 2017 11:00 am 12:30 pm | Pierre Bourhis: The Chase Inria Lille |
Fri, January 20, 2017 10:30 am 12:30 pm | Pierre Bourhis: "Tree Automata for Reasoning in Databases and Artificial Intelligence" In database management, one of the principal task is to optimize the queries to evaluate them efficiently. It is in particular the case for recursive queries for which their evaluation can lead to crawl all the database. In particular, one of the main question is to minimize the queries in order to avoid to evaluate useless parts of the query. The core theoretical question around this line of work is the problem of inclusion of a query in another. Interestedly, this question is related to an important question in IA which is to answer a query when the data is incomplete but rules are given to derive new information. This problem is called certain query answering. In both context, if both problem are undecidable in general, there are fragments based on guardedness that are decidable due to the fact there exists witness of the problems that have a bounded tree width and that their encoding in trees is regular. Furthermore, the queries can be translated in MSO. In both contexts, Courcelle’s Theorems imply the decidability of both problems. I will present to the different results on the translation of logic class of formula for our problems into tree automata to obtain tight bounds to the problems of inclusion of recursive queries or certain query answering. Inria Lille |
Wed, January 11, 2017 2:15 pm 3:25 pm | Michael vanden Boom, Oxford University : Decidable fixpoint logics Fixpoint logics can express dynamic, recursive properties, but often fail to have decidable satisfiability. A notable exception to this is the family of well-behaved "guarded" fixpoint logics, which subsume a variety of query languages and integrity constraints of interest in databases and knowledge representation. In this talk, I will survey some recent results about these logics. Lille B21 |
Mon, January 9, 2017 to Fri, January 13, 2017 all day | Visite Michael vanden Boom, Oxford University |