From e9d818ce0dea986a5d1063f0139337715d693f9e Mon Sep 17 00:00:00 2001 From: Cyril Pain-Barre <cyril.pain-barre@lis-lab.fr> Date: Wed, 6 Dec 2023 16:31:25 +0100 Subject: [PATCH] =?UTF-8?q?Ajout=20du=20s=C3=A9minaire=20de=20Alexis=20DE?= =?UTF-8?q?=20COLNET?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- seminar.md | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/seminar.md b/seminar.md index d5f36e8..28646a7 100644 --- a/seminar.md +++ b/seminar.md @@ -1,5 +1,18 @@ # Séminaires +### Mercredi 20 décembre 2023 à 15h + ++ Lieu : Salle de réunion COALA, dans les locaux de l'équipe. + ++ Orateur : Alexis DE COLNET (PostDoctorant, Institute of Logic and Computation, Vienne) + ++ Information(s) diverse(s) : exposé en français + ++ Titre : Compilation de connaissances et Bornes Inférieures pour les Systèmes de Preuve + ++ Résumé : La compilation de connaissances est un domaine de l'informatique qui étudie différentes classes -- ou langages -- de représentations pour les fonctions, et les algorithmes permettant de passer d'une classe à l'autre. On présente les bases de la compilation de connaissances ainsi que certaines classes de représentations -- certains langages -- qui sont la cible des compilateurs en pratique. Puis on montre comment des bornes inférieures sur la taille des représentations pour des fonctions dans certains langages peuvent être converties en bornes inférieures pour des systèmes de preuve. On explique notamment comment on a utilisé cette approche pour prouver des bornes inférieures exponentielles sur les réfutations de CNF spécifiques appelées formules de Tseitin dans deux systèmes de preuve : les réfutations OBDD(∧,r) et les réfutations par résolution régulière. + + ### Mercredi 6 décembre 2023 à 15h + Lieu : Salle de réunion COALA, dans les locaux de l'équipe. -- GitLab