- Renseignements pratiques
- Enseignement
Contact
LIFO - Bâtiment IIIA
Rue Léonard de Vinci
B.P. 6759
F-45067 ORLEANS Cedex 2
Email:
contact.lifo
Tel: +33 (0)2 38 41 99 29
Fax: +33 (0)2 38 41 71 37
Accéder aux Rapports de l'année : 1998 1999 2000 2001 2002 2003 2004 2005 2006 2007 2008 2009 2010 2011 2012 2013 2014 2015 2016 2017 2018
RR-2009-01 On a family of cubic graphs containing the flower snarks
JL Fouquet, Henri Thuillier, JM Vanherpe
Résumé : We consider cubic graphs formed with k > 2 disjoint claws Ci K_{1,3} (0 <= i <= k-1) such that for every integer i modulo k the three vertices of degree 1 of Ci are joined to the three vertices of degree 1 of C{i-1} and joined to the three vertices of degree 1 of C{i+1}. Denote by ti the vertex of degree 3 of Ci and by T the set {t0, t1, t2, ..., tk-1}. In such a way we construct three distinct graphs, namely FS(1,k), FS(2,k) and FS(3,k). The graph FS(j,k) is the graph where the set of vertices V(C0) U V(C1) U ... U V (C{k-1}) - T induce j cycles (note that the graphs FS(2,2p + 1), p > 1, are the Flower snarks defined by Isaacs. We determine the number of perfect matchings of every FS(j,k). A cubic graph G is said to be 2-factor hamiltonian if every 2-factor of G is a hamiltonian cycle. We characterize the graphs FS(j,k) that are 2-factor hamiltonian, (note that FS(1,3) is the "Triplex Graph" of Robertson, Seymour and Thomas). A strong matching M in a graph G is a matching M such that there is no edge of E(G) connecting any two edges of M. A cubic graph having a perfect matching union of two strong matchings is said to be a Jaeger's graph.We characterize the graphs FS(j,k) that are Jaeger's graphs.
Mot(s) Clé(s) : Cubic graphs
RR-2009-02 Un algorithme de décision dans l'algèbre des arbres finis ou infinis et des queues
Thi-Bich-Hanh Dao
Résumé : Les structures des arbres, des listes, des piles et des queues sont souvent utilisées en programmation logique et programmation logique avec contraintes. Il est donc important de pourvoir résoudre ou décider des contraintes dans ces structures. Les listes et les piles peuvent être considérées comme des cas spéciaux des arbres, mais ce n'est pas le cas des queues avec les opérations d'ajout d'un élément à gauche ou à droite. Nous présentons dans ce papier un algorithme de décision dans l'algèbre des arbres finis ou infinis étendus avec des queues. De cet algorithme découle un résultat en logique : la complétude et la décidabilité de la théorie du premier ordre de cet algèbre.
Mot(s) Clé(s) : arbres, queues, élimination de quantificateur, décidabilité
RR-2009-04 Constructing brambles
Mathieu Chapelle, Frédéric Mazoit, Ioan Todinca
Résumé : Given an arbitrary graph G and a number k, it is well-known by a result of Seymour and Thomas that G has treewidth strictly larger than k if and only if it has a bramble of order k+2. Brambles are used in combinatorics as certificates proving that the treewidth of a graph is large. >From an algorithmic point of view there are several algorithms computing tree-decompositions of G of width at most k, if such decompositions exist and the running time is polynomial for constant k. Nevertheless, when the treewidth of the input graph is larger than k, to our knowledge there is no algorithm constructing a bramble of order k+2. We give here such an algorithm, running in O(n^{k+4}) time. Moreover, for classes of graphs with polynomial number of minimal separators, we define a notion of compact brambles and show how to compute compact brambles of order k+2 in polynomial time, not depending on k.
Mot(s) Clé(s) : graph algorithms, graph decompositions, treewidth, brambles, duality theorem
RR-2009-06 Minimal Extensions of Tree Languages: Application to XML Schema Evolution
Jacques Chabin, Mirian Halfeld-Ferrari, Martin A. Musicante, Pierre Réty
Résumé : We give two algorithms to extend a given regular unranked tree language, into a local tree language, and into a single-type tree language. We show that we get the least possible extensions.
Mot(s) Clé(s) : XML, Unranked tree languages.
RR-2009-07 Program Calculation in Coq
Julien Tesson, Hideki Hashimoto, Zhenjiang Hu, Frédéric Loulergue, Masato Takeichi
Résumé : Program calculation, being a programming technique that derives programs from specification by means of formula manipulation, is a challenging activity. It requires human insights and creativity, and needs systems to help human to focus on clever parts of the derivation by automating tedious ones and verifying correctness of transformations. Different from many existing systems, we show in this paper that Coq, a popular theorem prover, provides a cheap way to implement a powerful system to support program calculation, which has not been recognized so far. We design and implement a set of tactics for the Coq proof assistant to help the user to derive programs by program calculation and to write proofs in calculational form. The use of these tactics is demonstrated through program calculations in Coq based on the theory of lists.
Mot(s) Clé(s) : Program calculation, Program derivation, Proof assistant, Theory of lists.
Les rapports de recherche du LIFO en 2009
RR-2009-01
On a family of cubic graphs containing the flower snarks
JL Fouquet, Henri Thuillier, JM Vanherpe
Date : 2009-01-27
Résumé Télécharger
RR-2009-02
Un algorithme de décision dans l'algèbre des arbres finis ou infinis et des queues
Thi-Bich-Hanh Dao
Date : 2009-03-10
Résumé Télécharger
RR-2009-04
Constructing brambles
Mathieu Chapelle, Frédéric Mazoit, Ioan Todinca
Date : 2009-06-18
Résumé Télécharger
RR-2009-06
Minimal Extensions of Tree Languages: Application to XML Schema Evolution
Jacques Chabin, Mirian Halfeld-Ferrari, Martin A. Musicante, Pierre Réty
Date : 2009-12-04
Résumé Télécharger
RR-2009-07
Program Calculation in Coq
Julien Tesson, Hideki Hashimoto, Zhenjiang Hu, Frédéric Loulergue, Masato Takeichi
Date : 2009-12-22
Résumé Télécharger
Résumés des rapports de recherche
RR-2009-01 On a family of cubic graphs containing the flower snarks
JL Fouquet, Henri Thuillier, JM Vanherpe
Résumé : We consider cubic graphs formed with k > 2 disjoint claws Ci K_{1,3} (0 <= i <= k-1) such that for every integer i modulo k the three vertices of degree 1 of Ci are joined to the three vertices of degree 1 of C{i-1} and joined to the three vertices of degree 1 of C{i+1}. Denote by ti the vertex of degree 3 of Ci and by T the set {t0, t1, t2, ..., tk-1}. In such a way we construct three distinct graphs, namely FS(1,k), FS(2,k) and FS(3,k). The graph FS(j,k) is the graph where the set of vertices V(C0) U V(C1) U ... U V (C{k-1}) - T induce j cycles (note that the graphs FS(2,2p + 1), p > 1, are the Flower snarks defined by Isaacs. We determine the number of perfect matchings of every FS(j,k). A cubic graph G is said to be 2-factor hamiltonian if every 2-factor of G is a hamiltonian cycle. We characterize the graphs FS(j,k) that are 2-factor hamiltonian, (note that FS(1,3) is the "Triplex Graph" of Robertson, Seymour and Thomas). A strong matching M in a graph G is a matching M such that there is no edge of E(G) connecting any two edges of M. A cubic graph having a perfect matching union of two strong matchings is said to be a Jaeger's graph.We characterize the graphs FS(j,k) that are Jaeger's graphs.
Mot(s) Clé(s) : Cubic graphs
RR-2009-02 Un algorithme de décision dans l'algèbre des arbres finis ou infinis et des queues
Thi-Bich-Hanh Dao
Résumé : Les structures des arbres, des listes, des piles et des queues sont souvent utilisées en programmation logique et programmation logique avec contraintes. Il est donc important de pourvoir résoudre ou décider des contraintes dans ces structures. Les listes et les piles peuvent être considérées comme des cas spéciaux des arbres, mais ce n'est pas le cas des queues avec les opérations d'ajout d'un élément à gauche ou à droite. Nous présentons dans ce papier un algorithme de décision dans l'algèbre des arbres finis ou infinis étendus avec des queues. De cet algorithme découle un résultat en logique : la complétude et la décidabilité de la théorie du premier ordre de cet algèbre.
Mot(s) Clé(s) : arbres, queues, élimination de quantificateur, décidabilité
RR-2009-04 Constructing brambles
Mathieu Chapelle, Frédéric Mazoit, Ioan Todinca
Résumé : Given an arbitrary graph G and a number k, it is well-known by a result of Seymour and Thomas that G has treewidth strictly larger than k if and only if it has a bramble of order k+2. Brambles are used in combinatorics as certificates proving that the treewidth of a graph is large. >From an algorithmic point of view there are several algorithms computing tree-decompositions of G of width at most k, if such decompositions exist and the running time is polynomial for constant k. Nevertheless, when the treewidth of the input graph is larger than k, to our knowledge there is no algorithm constructing a bramble of order k+2. We give here such an algorithm, running in O(n^{k+4}) time. Moreover, for classes of graphs with polynomial number of minimal separators, we define a notion of compact brambles and show how to compute compact brambles of order k+2 in polynomial time, not depending on k.
Mot(s) Clé(s) : graph algorithms, graph decompositions, treewidth, brambles, duality theorem
RR-2009-06 Minimal Extensions of Tree Languages: Application to XML Schema Evolution
Jacques Chabin, Mirian Halfeld-Ferrari, Martin A. Musicante, Pierre Réty
Résumé : We give two algorithms to extend a given regular unranked tree language, into a local tree language, and into a single-type tree language. We show that we get the least possible extensions.
Mot(s) Clé(s) : XML, Unranked tree languages.
RR-2009-07 Program Calculation in Coq
Julien Tesson, Hideki Hashimoto, Zhenjiang Hu, Frédéric Loulergue, Masato Takeichi
Résumé : Program calculation, being a programming technique that derives programs from specification by means of formula manipulation, is a challenging activity. It requires human insights and creativity, and needs systems to help human to focus on clever parts of the derivation by automating tedious ones and verifying correctness of transformations. Different from many existing systems, we show in this paper that Coq, a popular theorem prover, provides a cheap way to implement a powerful system to support program calculation, which has not been recognized so far. We design and implement a set of tactics for the Coq proof assistant to help the user to derive programs by program calculation and to write proofs in calculational form. The use of these tactics is demonstrated through program calculations in Coq based on the theory of lists.
Mot(s) Clé(s) : Program calculation, Program derivation, Proof assistant, Theory of lists.
Université d'Orléans | INSA Centre Val de Loire
LIFO - Laboratoire d'Informatique Fondamentale d'Orléans 