Previous Next Contents

7   Année 1998-99

Groupe de travail géré par par D. Janin

   


* 21 Septembre A. Arnold
  La hiérarchie du mu-calcul sur les arbres binaires est infine


* 28 Septembre A. Middeldorp (Tsukuba, Japon)
  A deterministic Lazy Naroowing Calculus
  Résumé : In this talk we summarize recent joint work with Satoshi Okui on the completeness of the lazy narrowing calculus LNC. LNC consists of five simple inference rules that simulate the complicated narrowing operation. Contrary to what has been stated in the literature, we show that LNC lacks strong completeness, so selection functions to cut down the search space are not applicable. We establish an interesting connection between strong completeness of LNC and completeness of basic narrowing. We also address the eager variable elimination problem. It is known that many redundant derivations can be avoided if the variable elimination rule, one of the inference rules of LNC, is given precedence over the other inference rules. We prove the completeness of a restricted variant of eager variable elimination in the case of left-linear confluent rewrite systems. We show that for left-linear confluent constructor systems all non-determinism between the inference rules of LNC can be removed without losing completeness, provided we interpret equality as strict equality. For the subclass of orthogonal constructor systems the resulting calculus LNC_d is shown to have the nice property that solutions computed by different derivations starting from the same goal are incomparable.

If time permits we conclude with an overview of very recent completeness results for LCNC, the extension of LNC for conditional rewrite systems, which were obtained jointly with Mohamed Hamada and Taro Suzuki.

In this talk no specific knowledge of rewriting or narrowing is assumed.


* 5 Octobre Présentation des activités du groupe de travail
   


* 12 Octobre P. Weil
  Langages d'ensembles partiellement ordonnes serie-parallele


* 19 Octobre Ph. Narbel
  Les substitutions itérées et les automorphismes de surface
  Résumé : Il s'agira de montrer comment les substitutions itérées -- étudiées entre autres sous le nom de D0L-systèmes -- peuvent se représenter géométriquement, puis comment il est alors possible d'obtenir des résultats constructifs et algorithmiques liés à la classification classique (dite de Nielsen-Thurston) des automorphismes des surfaces, i.e. des transformations bi-continues bijectives des surfaces sur elles-mêmes.


* 26 Octobre B. Lesaec
  Représentation de graphes planaires en couches


* 2 Novembre C. Paul
  Algorithmes de décomposition modulaire


* 9 Novembre J.M. Le Bars (Caen, meilleur papier étudiant LICS'98)
  Lois 0-1 en logique


* 30 Novembre B. Courcelle
  Graphes uniformement creux et élimination des quantifications sur les ensembles d'arcs


* 7 Décembre B. Courcelle
  Graphes bipartis convexes


* 14 Décembre I. Walukiewicz
  On the guarded fragment of first order logic and its extension with fixpoints
  Résumé : Guarded fragment (GF), introduced by Andreka, van Benthem and Nemeti, is a fragment of first order logic that "behaves like modal logic". The fragment is defined by syntactically restricting the use of quantifiers. Nevertheless GF contains more than just formulas resulting from the translation of modal formulas. For example, in GF there is no restriction on the arity of relations in GF.

Andreka, van Benthem and Nemeti has shown that satisfiability problem for GF is decidable and that GF has some desirable properties like small model theorem, interpolation theorem and characterisation of the expressive power in terms of modified Ehrenfeucht-Fraisse games. Graedel has shown that satisfiability of formulas in GF (and its extension LGF) is complete for 2EXPTIME and it is complete for EXPTIME if the signature is fixed.

We consider the extension of LGF with fixpoint operators (of arbitrary arity). It turns that the satisfiability problem for this logic is still in 2EXPTIME and it is in EXPTIME if the signature is fixed. This way we have an extension of the mu-calculus with bigger expressive power but with the same complexity of the decision procedure.


* 11 Janvier H. Jacquet
  Une approche catégorique de la réécriture de sommets dans les graphes


* 18 Janvier G. Sénizergues
  T(A)=T(B) : le probleme de l'equivalence des transducteurs a pile deterministes de X* dans un groupe lineaire


* 25 Janvier E. Sopena
  Homomorphismes et Colorations de Graphes Orientés
  Résumé : Un homomorphisme d'un graphe G vers un graphe G' est une application f:V(G)¾® V(G') qui préserve les arêtes : xyÎ E(G) f(x)f(y)Î E(G'). On observe alors facilement qu'un graphe G est k-coloriable si et seulement s'il admet un homomorphisme vers le graphe complet à k sommets. Si l'on considère maintenant les graphes orientés antisymétriques, la notion d'homomorphisme induit de la même façon la notion de coloration de graphe orienté : une k-coloration d'un graphe orienté H est une application c:V(H)¾®{1,2,...,k} telle que
(i) xyÎ E(H) c(x)¹ c(y) et
(ii) xy,ztÎ E(H), c(x)=c(t) c(y)¹ c(z).
Nous allons présenter les principaux résultats obtenus jusqu'ici sur les homomorphismes et colorations de graphes orientés. Nous présenterons également quelques questions ouvertes.


* 8 Février I. Klimann (LIAFA, Paris VII)
  De nouvelles structures pour resoudre des problemes d'(A,B)-invariance
  Résumé : On cherche a trouver le sup de l'ensemble {X| AX £ X+B et X£ K} dans divers cadres (langages, series), ou A, B et K sont des parametres fixes ayant une certaine regularite. Pour cela, on introduit de nouveaux outils melant automates (pour les langages) ou representations lineaires (pour les series) a des formules booleennes.


* 15 Février M. Robson
  Un Majorant du seuil de 3-coloriabilité


* 8 mars V. Dussaux
  Problemes lies aux cartes partielles et caracterisation des cartes toriques


* 15 mars A. Raspaud
  Coloration des graphes mixtes


* 22 mars E. Godard
  Classes de graphes reconnaissable par calculs locaux


* 29 mars N. Bidoit
  Hierarchie de langages de requetes temporelles lineaires


* 31 mai G. Lenzi
  Sur la structure de la logique monadique du second ordre sur l'arbre binaire


* 7 juin B. Lesaec
  Reconnaissance forte pour les langages rationnels


Previous Next Contents