- Contacts/Reaching LIFO
- Teaching
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
Go to Research Reports of Year : 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
Abstract : 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.
Keywords : 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
Abstract : The structures of trees, lists, stacks and queues are usually used in logic programming or constraint logic programming. It is then important to be capable to solve or to decide constraints in these structures. Lists and stacks can be considered as special cases of trees, but it is not the case for queues with left- and right-insert operations. We present in this paper a decision algorithm in the algebra of finite or infinite trees extended with queues. This algorithm gives a result in logic: the completeness and the decidability of the first-order theory of this algebra.
Keywords : trees, queues, quantifier elimination, decidability
RR-2009-04 Constructing brambles
Mathieu Chapelle, Frédéric Mazoit, Ioan Todinca
Abstract : 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.
Keywords : 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
Abstract : 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.
Keywords : XML, Unranked tree languages.
RR-2009-07 Program Calculation in Coq
Julien Tesson, Hideki Hashimoto, Zhenjiang Hu, Frédéric Loulergue, Masato Takeichi
Abstract : 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.
Keywords : Program calculation, Program derivation, Proof assistant, Theory of lists.
LIFO Research Report for Year 2009
RR-2009-01
On a family of cubic graphs containing the flower snarks
JL Fouquet, Henri Thuillier, JM Vanherpe
Date : 2009-01-27
Abstract Download
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
Abstract Download
RR-2009-04
Constructing brambles
Mathieu Chapelle, Frédéric Mazoit, Ioan Todinca
Date : 2009-06-18
Abstract Download
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
Abstract Download
RR-2009-07
Program Calculation in Coq
Julien Tesson, Hideki Hashimoto, Zhenjiang Hu, Frédéric Loulergue, Masato Takeichi
Date : 2009-12-22
Abstract Download
Abstracts of Research Reports
RR-2009-01 On a family of cubic graphs containing the flower snarks
JL Fouquet, Henri Thuillier, JM Vanherpe
Abstract : 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.
Keywords : 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
Abstract : The structures of trees, lists, stacks and queues are usually used in logic programming or constraint logic programming. It is then important to be capable to solve or to decide constraints in these structures. Lists and stacks can be considered as special cases of trees, but it is not the case for queues with left- and right-insert operations. We present in this paper a decision algorithm in the algebra of finite or infinite trees extended with queues. This algorithm gives a result in logic: the completeness and the decidability of the first-order theory of this algebra.
Keywords : trees, queues, quantifier elimination, decidability
RR-2009-04 Constructing brambles
Mathieu Chapelle, Frédéric Mazoit, Ioan Todinca
Abstract : 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.
Keywords : 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
Abstract : 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.
Keywords : XML, Unranked tree languages.
RR-2009-07 Program Calculation in Coq
Julien Tesson, Hideki Hashimoto, Zhenjiang Hu, Frédéric Loulergue, Masato Takeichi
Abstract : 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.
Keywords : Program calculation, Program derivation, Proof assistant, Theory of lists.
University of Orléans | INSA Centre Val de Loire
LIFO - Laboratoire d'Informatique Fondamentale d'Orléans 