Jeudi 19 décembre 2024
9h30
Speaker : Daniil Kozhemiachenko (LIS, équipe LIRICA)
Title : Logiques paraconsistantes pour le raisonnement sur l’incertitude
Abstract: Pour etre paraconsistante, une logique doit invalider le principe de l’explosion, soit il doivent exister deux formules A et B telles que A&¬A n’implique pas B. Dans cet expose, nous discutons une logique simple paraconsistante de Belnap et Dunn (BD) ainsi que ses augmentations modales et considerons leurs applications au raisonnement sur l’incertitude. Nous traiterons la notion d’incertitude de deux manieres: d’un cote comme une mesure d’incertitude exprimee par une probabilite ou fonction de croyance; d’autre cote comme elle apparait dans les phrases du langage courant telles que «je crois, que…», «je pense, que…», etc. Pour chacun des deux approches a l’incertitude nous proposons sa formalisation a l’aide de BD.
10h15
Speaker : Benjamin Bergougnoux (LIS, équipe COALA)
Title : Neighborhood operator logics: efficient model checking in terms of width parameters
Abstract: In this talk, I will introduce the family of neighborhood operator (NEO) logics which are extensions of existential MSO with predicates for querying neighborhoods of vertex sets. NEO logics have interesting modeling powers and nice algorithmic applications for several width parameters such as tree-width. NEO logics capture many important graphs problems such as Independent Set, Dominating Set and many of their variants. Moreover, some NEO logics capture CNF-SAT via the signed incidence graphs! We can capture more problems by considering various extensions of NEO logics. For example, we can capture problems with global constraints such as Hamiltonian Cycle via the extension of NEO logics with predicates for checking the connectivity/acyclicity of vertex sets.
In terms of algorithmic applications, NEO logics seem to be the perfect candidates for capturing many problems that can be solved efficiently in terms of width parameters.
This is suggested by the following three results:
- For tree-width, the most powerful NEO logics can be model checked in single exponential time in terms of tree-width as implied by a result of Michal Pilipczuk [MFCS 2011].
- Jan Dreier, Lars Jaffke and I proved that, for an extension of one NEO logic, we can obtain an efficient model-checking algorithm in terms of several width parameters more general than tree-width such as clique-width, rank-width and mim-width [SODA 2023].
- Vera Checkan, Giannos Stamoulis and I are currently proving that the most powerful NEO logic can be solved in single exponential time and polynomial space for tree-depth: the shallow restriction of tree-width. This last result could be interesting in practice where space usage is crucial.
I will present these three results after a friendly introduction on width parameters.
Pause Cafe : 11h00 — 11h30
11h30
Speaker : Lê Thành Dũng (Tito) Nguyễn (LIS, équipe LSC)
Title : Algorithmique des graphes pour la combinatoire des preuves en logique linéaire
Abstract: Je présenterai comment un lien entre les « réseaux de preuve » de la logique linéaire et les couplages parfaits, découvert par Christian Retoré, peut être exploité pour obtenir des résultats de complexité sur des problèmes qui intéressent les logicien⋅nes. En particulier, ces outils ont mené à la réfutation de l’équivalence entre deux variantes non-commutatives de la logique linéaire (pomset logic et système BV), équivalence qui était conjecturée depuis deux décennies.
https://lmcs.episciences.org/6172
https://lmcs.episciences.org/12705