- Contacts/Reaching LIFO
- Teaching

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

# LIFO Research Report for Year 2009

## 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.

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

University of Orléans | INSA Centre Val de Loire