|
|
* 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 |