Jacqueline Vauzeilles - Page Académique

au niveau international  
 
Experte pour pour le Ministère des Universités et de la Recherche Italien (MIUR), pour l’évaluation de projets d’intérêt national et experte pour l’évaluation nationale de la recherche (VTR) organisée par le comité italien pour l’évaluation de la recherche (CIVR). Rapporteur de trois thèses et de deux postdoctorats en Italie. 

Responsable pour le site Paris 13 du réseau franco-italien en Logique et Géométrie de la computation (2006-2009).

Responsable du sous-site Paris 13 du site de Paris du TMR "Linear Logic in Computer Science" (1998-2003). 

Partenaire dans un projet ESPRIT de la Communauté Européenne (Working Group - Basic Research) "Logic and Change" (LAC) (1992-1996).

au niveau national  

Déléguée Scientifique à l'AERES (Agence pour l'évaluation de la recherche et de l'enseignement supérieur) à partir du 1er septembre 2009, section 2 (section des unités de recherche) et section 3 (section des formations et des diplômes). Coordinatrice scientifique du processus master de l'AERES.

Directrice-Adjointe Scientifique de l'USAR (Unité Support de L'Agence Nationale pour la Recherche (ANR) pour les programmes non-thématiques, de juin 2007 à août 2009.

Membre du comité de sélection pour deux postes à l'université d'Artois (mai 2009).

Présidente du jury des PEDR (27ème section) en 2008.

Experte pour l'AERES : membre du comité de visite du CRIL (2008), membre des comités de visite de l'AERES des Ecoles Doctorales de Caen et de Rouen (2007), expertise de masters (2007, 2008).

Chargée de Mission à la MSTP (et responsable des masters pour la DSPT 9) de novembre 2006 à juillet 2007.

Membre du Conseil National des Universités (CNU) (nommée : 1999 - 2003, élue : 2003 - 2007). 

Experte auprès de la Mission Scientifique Technique et Pédagogique du ministère de l'éducation nationale (dossiers de master, ACI Nouvelles Interfaces des Mathématiques, PAI, Ecoles Doctorales).

Experte auprès de l'ANR (2005, 2006, 2007)

Membre extérieure du jury d'admissibilité du recrutement CR2 de l'INRIA Lorraine (mai 2003 et mai 2005).

Directrice du LIPN (Laboratoire d'Informatique de l'Université Paris-Nord) (de novembre 1997 à janvier 2004).

Création et responsabilité de l'équipe LCR (Logique, Calcul et Raisonnement du LIPN (1989-2002).

Membre extérieure des Commissions de Spécialistes de Caen (1992-1997) (27ème section), et de ParisX-Nanterre (1992-1995) (25-26-27èmes sections). 

à l'Université Paris 13

Chargée de mission auprès du président de l'Université Paris 13 pour la coordination des réponses de l'Université aux appels d'offres du Grand Emprunt, et pour la concertation avec les partenaires de l'Université (PRES Sorbonne Paris Cité, Campus Condorcet, pôles de compétitivité, collectivités locales, etc.) depuis avril 2010.

Membre du comité d'experts (27ème section) de l'Université Paris 13, depuis avril 2009 et présidente (membre) de comités de sélection pour plusieurs postes en 2009, 2010, 2011.

Membre de la Commission de Spécialistes (27ème section) de l'Université Paris 13 (1989 - 2004 )

Vice-Présidente du Conseil Scientifique de l'Université Paris 13 (septembre 1999 - décembre 2002)

Membre élue du Conseil Scientifique de l'Université Paris 13 (de mars 1998 à mars 2008) et membre de la sous-commission chargée des équivalences (1998 - 2002).

Membre du Bureau de l'Université Paris 13 (septembre 1999 - décembre 2002 et de juin 2006 à mars 2008). Membre Invité Permanent du Conseil d'Administration de l'Université Paris 13 (septembre 1999 - décembre 2002).

Membre du Bureau de l'Ecole Doctorale de mars 2005 à mars 2008. Membre du Conseil de l'Ecole Doctorale Galilée (de novembre 1997 à mars 2008).


Membre nommé de la Cellule des Relations Internationales, de la Commission des Moyens de l'université, de la Commission Paritaire d'Etablissement, du Conseil du Service Commun des Bibliothèques et de la Documentation (1999 - 2002).

Représentante de l'Université Paris 13 dans le comité d'évaluation du CNRS du Laboratoire de Physique des Lasers (2000), dans le comité scientifique du Laboratoire "Ciblage fonctionnel des tumeurs solides ” (2000), dans le comité d'évaluation du CNRS du Laboratoire de Biomatériaux et Polymères de Spécialité (2004).

Membre du comité de pilotage du CIES Jussieu, comme représentante de l'université Paris 13 (1999-2002)

Membre élue du CEVU de l'Université Paris 13 et membre de la sous-commission chargée des habilitations (janvier 1994 - décembre 1998).

Directrice-Adjointe, responsable de la recherche de l'Institut Galilée et à ce titre invitée permanente au Conseil d'Institut, membre de la Commission des Moyens, membre de la commission du personnel, de mars 2004 à mars 2008.

Membre du Conseil Scientifique de l'Institut Galilée (de novembre 1997 à mars 2008).

Membre du Conseil du LIPN depuis son association au CNRS (1992-2007).

Présidente du département d'Informatique de l'Institut Galilée (à ce titre, invitée permanente au Conseil d'Institut et membre de la Commission des Moyens) (novembre 91 - février 94).  

Membre de la Commission du Personnel de l'Institut Galilée (1992-1994)

Directrice-Adjointe, responsable du second cycle de l'Institut Galilée et à ce titre invitée permanente au Conseil d'Institut, membre de la Commission des Moyens, membre de la commission du personnel, de juin 1994 à décembre 1996.                                    

Responsable de la licence d'Informatique (septembre 1991- novembre 1998), et à ce titre, responsable de la demande d'habilitation de cette licence en 1995.

Membre élue du Conseil d'Institut de l'IUT de Villetaneuse (1990-91).

Applications de la logique linéaire

La logique linéaire introduite par Jean-Yves Girard en 1985, est un raffinement à la fois des logiques classique et intuitionniste, qui a permis en particulier de donner un statut logique aux opérations de duplication et d’effacement d’hypothèses. Depuis son introduction, la logique linéaire a eu un rôle sans  cesse croissant dans l’étude et la compréhension de divers problèmes d’informatique. Nous nous sommes particulièrement intéressés aux preuves et réseaux de preuves de la logique linéaire et à diverses applications en programmation logique, planification, linguistique, etc. 

Planification et logique linéaire :
Nous avons utilisé le fragment multiplicatif de la logique linéaire pour formaliser de manière complète et correcte une suite d’actions : dans cette logique, l’affaiblissement et la contraction sont des opérations dont l’usage est contrôlable, ce qui permet de gérer très exactement les ressources. Une suite d’actions est représentée par une preuve dans une théorie de la logique linéaire dont les axiomes sont des séquents de Horn utilisant les connecteurs ⊗ et ⊕ dans le cas d’actions non déterministes, et seulement le connecteur ⊗ dans le cas d’actions déterministes [21,10]. Deux prolongements de ces travaux ont ensuite été étudiés :
∗ Nous avons étudié le problème de la complexité de la recherche de preuve dans de telles théories : il est connu que la logique propositionnelle linéaire de Horn est indécidable dans le cas général (cas des connecteurs ⊗ et ⊕) et a la complexité du problème d’accessibilité dans les réseaux de Petri (cas du connecteur ⊗). Pour restreindre la complexité, nous avons utilisé (dans des travaux en collaboration avec Max Kanovich, université de Moscou) des axiomes tels que le nombre de prédicats apparaissant dans la partie gauche est supérieur ou égal à celui apparaissant dans la partie droite. Cette condition, réalisée dans la formalisation des problèmes de planification usuels, permet de ramener la complexité à EXPTIME (temps exponentiel) dans le cas d’actions non déterministes, et à PSPACE (espace polynomial) dans le cas d’actions déterministes [3].
∗ Nous nous sommes ensuite intéressés aux problèmes de planification comprenant un nombre non borné d’objets fonctionnels identiques. Nous avons montré qu’en utilisant la logique linéaire, on peut diminuer de manière drastique la complexité : on se ramène à une complexité polynomiale, si le problème initial comporte des symétries (objets identiques). On évite l’explosion combinatoire causée par ces symétries en introduisant un objet générique au lieu de noms spécifiques pour chacun des objets réels. On contracte ainsi l’espace de recherche exponentiel sur les objets réels en un espace de recherche polynomial sur un objet générique. Puis on transforme (en temps polynomial) la preuve générique en une preuve réelle du problème initial [16, 2].
∗ Nous avons ensuite étendu nos résultats à la planification temporelle [1]. 

Réseaux taxonomiques et logique linéaire :
Un réseau taxonomique est un graphe orienté permettant de représenter la connaissance. Les noeuds représentent des concepts ou des propriétés d’un ensemble d’individus, alors que les arcs représentent des relations entre concepts. Le réseau peut être vu comme une hiérarchie de concepts ordonnés suivant leur niveau de généralité. De nombreux chercheurs en Intelligence Artificielle ont essayé de formaliser ces réseaux, et les logiques non-monotones ont été développées pour représenter ces réseaux.
Partant de la remarque que bien que la logique linéaire soit une logique monotone, l’implication linéaire a un "comportement non monotone" relativement à la conjonction linéaire multiplicative (connecteur ⊗), nous avons cherché à formaliser les réseaux taxonomiques dans le fragment linéaire comprenant la constante 1, le connecteur ⊗, l’implication linéaire ainsi que le connecteur "bien sûr".
Nous avons d’abord considéré des réseaux avec seulement des arcs défauts et des arcs exceptions ; nous identifions une classe particulière de séquents de ce fragment, les séquents simples et la démonstration de tels séquents nous permet de caractériser les propriétés héritées par un individu particulier. Nous remplaçons ensuite une preuve d’un tel séquent par un réseau linéaire, correspondant exactement à un sous-graphe "maximal correct" du réseau sémantique initial. Enfin nous montrons un résultat d’équivalence avec l’approche plus traditionnelle utilisant la logique des défauts [19].
Nous avons ensuite étendu nos résultats au cas des réseaux avec liens stricts ou avec contre-exceptions [8].
Par la suite, nous avons utilisé les propriétés des connecteurs linéaires pour nous débarasser des contraintes que nous avions imposées quant à la forme des séquents prouvés, de manière à obtenir un système déductif (en logique linéaire). Afin de pouvoir combiner raisonnement classique et raisonnement avec exceptions (réseau taxonomique) nous avons plongé le système précédent dans LU (la Logique Unifiée) [7]. 

Logique linéaire et linguistique :
Nous avons présenté une formalisation logique des Tree-Adjoining Grammar (TAG). Dans TAG, on considère des arbres lexicalisés et deux opérations sont autorisées : la substitution et l’adjonction. L’adjonction consiste en l’insertion d’un arbre à l’intérieur d’un autre, l’opération étant effectuée en un nœud où l’adjonction est autorisée. Nous avons montré qu’on pouvait représenter ces opérations à l’aide d’un fragment de la logique de Lambek (c’est-à-dire du fragment multiplicatif non commutatif de la logique non-commutative intuitionniste). La modélisation des TAG se fait en représentant les arbres initiaux et auxiliaires par des séquents ; la substitution est traduite par la coupure, et une règle d’adjonction est définie sur les séquents afin de formaliser l’adjonction sur les arbres. A une grammaire dans TAG est associée un ensemble de séquents et la clˆoture sous les opérations précédentes de cet ensemble permet de définir le langage engendré : on montre que ce langage est exactement celui obtenu à l’aide des TAG [18, 23]. 

Programmation logique en logique non commutative :
La logique non commutative (NL) a été introduite en 1997 par Paul Ruet et Michele Abrusci ; c’est une extension à la fois de la logique linéaire commutative et de la logique linéaire cyclique de Girard et Yetter (qui est elle-même une extension conservatrice classique du calcul de Lambek, introduit en 1958). Initialement, Paul Ruet a défini cette logique pour la programmation concurrente par contraintes, mais les applications potentielles en sont nombreuses. La programmation en logique linéaire (commutative), introduite par Jean-Marc Andreoli, a été le sujet de nombreuses recherches internationales (D. Miller à Philadelphie, M.Winikoff à Melbourne, par exemple). Nous avons cherché à étendre les résultats d’Andreoli afin de construire un langage de programmation en logique non- commutative. Dans NL il y a deux connecteurs autres que ceux de la logique linéaire, qui sont non commutatifs ; de nouvelles règles permettent de lier les structures commutatives et non-commutatives.
Il existe deux présentations du calcul des séquents de NL, l’une utilisant des ordres partiels (en pratique des ordres série-parallèles), l’autre des variétés d’ordre série-parallèles. Nous avons choisi les séquents avec ordres partiels pour étendre la notion de ”focusing” d’Andreoli. Cette étude et la construction théorique du langage ont été l’objet de la thèse soutenue par Rémi Baudot. 

Programmation logique :
Un des problèmes en programmation logique, était de trouver une interprétation logique ”utile et simple” pour les programmes utilisant la négation par l’échec : seules des réponses partielles avaient jusqu’alors été apportées, car la version trivaluée classique (Kunen) ou celle utilisant la logique linéaire (Cerrito) du complété de Clark ne permettent d’obtenir la complétude que pour une classe restreinte de programmes:
les programmes autorisés. En utilisant la logique trivaluée introduite par Girard en 1973, nous avons défini, de manière analogue, un complété pour lequel nous avons des résultats similaires de correction et de complétude. En particulier, cette logique permet de définir une syntaxe pour la logique utilisée par Kunen. En utilisant la version intuitionniste de cette logique, nous avons pu de plus expliquer certains cas ”d’enlisement” (floundering). D’autre part, la logique intuitionniste trivaluée permet de donner une sémantique pour les programmes avec négation dans la tête des clauses, dans l’hypothèse du monde ouvert. On a alors des résultats de correction et de complétude. Cette recherche a conduit à deux publications [24, 20]. 

Logique unifiée :
Le calcul des séquents LU (Logique Unifiée) introduit par Jean-Yves Girard, est commun aux logiques classique, intuitionniste et linéaire. Chacune des précédentes logiques est un fragment de LU : la preuve de ce résultat s’appuie sur un théorème d’élimination des coupures. La preuve de ce théorème est assez complexe en raison de l’imbrication des trois règles de coupure (une règle linéaire et deux classiques) de LU : l’élimination de certaines coupures classiques introduit des coupures linéaires, alors que l’élimination de certaines coupures linéaires introduit des coupures classiques. Ce résultat d’élimination des coupures a été démontré sous des hypothèses minimales en introduisant une notion de degré qui dépend seulement du nombre d’exponentielles de la formule. Ce résultat généralise des résultats antérieurs de la logique linéaire, et le raffinement concernant les degrés donne de meilleures bornes pour l’élimination des coupures et permet de nombreuses applications comme dans le cas des formules non bien-fondées utilisées dans la démonstration du théorème du point fixe [9].   

Membre de l’équipe de Logique de Paris 7 (U.R.A. CNRS 753) jusqu’en septembre 1989.

Participation, entre 1973 et 1986, aux recherches du groupe de théorie de la démonstration de Paris 7, dirigé par J.-Y. Girard. Les travaux ont essentiellement concerné la logique Π1-2.  

Dans une série d’articles, dont certains en collaboration avec J.Y. Girard, définition des versions fonctorielles des hiérarchies de Veblen et de Bachmann (utilisées traditionnellement pour attacher des ordinaux à des théories, ordinaux mesurant en quelque sorte la force de ces théories) [15, 14 ]. Ces travaux permettent en particulier d’établir le lien exact entre les notions ”classiques” de théorie de la démonstration et la logique [23, 12]. Ensuite, en collaboration avec J.Y. Girard, application des résultats de la logique à des problèmes de récursion généralisée [13]. Ces travaux font l’objet de la thèse d’Etat soutenue à l’Université Paris 7 en 1983. 

Dans un article sur la Ω-logique, extension des résultats d’élimination des coupures et d’interpolation, à la Ω-logique [11].

[1]. M. Kanovitch, J. Vauzeilles : "Linear Logic in Temporal Planning for Actions with Delayed Effects", Theoretical Computer Science, 'Jean-Yves Girard Festschrift', Vol. 412, Issue 20, pp.2072-2092, 2011.

[2]. Max Kanovitch, J. Vauzeilles : “ Polytime strong planning under uncertainty in domains with numerous but identical elements (a ‘generic‘ approach) ", Theoretical Computer Science, Vol. 379, pp. 84-119, 2007.

[3]. Max Kanovitch, J. Vauzeilles : “The Classical AI Planning Problems in the Mirror of Horn Linear Logic : Semantics, Expressibility, Complexity", Mathematical Structures in Computer Science, Vol 11, pp. 1-28, 2001.

[4]. M. Abrusci, C. Fouqueré, J. Vauzeilles : "Tree Adjoining Grammars in a fragment of the Lambek calculus", Computational Linguistics, Vol 99, n°9, pp.209-236, 1999. (Version longue de l'article des Proceedings LACL'96).

[5]. J. Vauzeilles : "Ordinals II : some applications and a functorial approach". Mathematics and Computer Science, S. Grigorieff & M. Nivat (éd.), Annals of Applied Mathematics and Artificial Intelligence n° 16/1-4, Baltzer, pp. 27-58, 1996.

[6]. M. Ferbus and J. Vauzeilles : "Ordinals I : basic notions". Mathematics and Computer Science, S. Grigorieff & M. Nivat (éd.), Annals of Applied Mathematics and Artificial Intelligence n° 16/1-4, Baltzer, pp. 1-26, 1996.

[7]. C. Fouqueré and J. Vauzeilles : “Inheritance with exceptions: an attempt at formalization with linear connectives in Unified Logic", Advances in Linear Logic, J.-Y. Girard and Y. Lafont and L. Regnier (éd.), pp.167-196, Cambridge University Press, 1995.

[8]. C. Fouqueré and J. Vauzeilles : "Linear logic and exceptions", Journal of Logic and Computation, Vol. 4, n° 6, pp. 859-875, 1994.

[9]. J. Vauzeilles : "Cut Elimination for the Unified Logic", Annals of Pure and Applied Logic, 1993, vol. 62, p. 1-16.

[10]. M. Masseron, C. Tollu, J. Vauzeilles : "Generating Plans in Linear Logic : I. Actions as proofs". Theoretical Computer Science B, vol. 113, juin 1993, p. 349-370.

[11]. J. Vauzeilles : "Cut-elimination and Interpolation for the Ω-logic", Archiv für Mathematische Logik und Grundlagenforschung, Vol.27, 1988, p.161-175.

[12]. J.Vauzeilles : "Functors and ordinal notations IV : The Howard Ordinal and the functor Λ", Journal of Symbolic Logic, 1985, Vol.50, p.331-338.

[13]. J-Y Girard and J. Vauzeilles : "Les premiers récursivement inaccessible et Mahlo et la théorie des dilatateurs". Archiv für Mathematische Logik und Grundlagen-forschung, Vol.24, 1985, p.167-191.

[14]. J-Y Girard and J. Vauzeilles : "Functors and ordinal notations II : a functorial construction of the Bachmann hierarchy", Journal of Symbolic Logic, 1984, Vol. 49, p.1079-1114.

[15]. J-Y Girard and J. Vauzeilles : "Functors and ordinal notations I : a functorial construction of the Veblen hierarchy", Journal of Symbolic Logic, 1984, Vol. 49, p.713-729.

[16]. M. Kanovitch, J. Vauzeilles : “Coping polynomially with numerous but identical elements within planning problems“, CSL'03 & KGC (Computer Science Logic and Kurt Gödel Colloquium), 25-30 août 2003, Vienne, LNCS 2803 pp. 285-298.

[17]. S. Schwer, J. Vauzeilles : "Calendars inside the framework of finite ordinals category", ECAI-98, Workshop on Spatial and Temporal Reasoning, Brighton, UK, 25 août 98.

[18]. M. Abrusci, C. Fouqueré, J. Vauzeilles : "Tree Adjoining Grammars in Noncommutative Linear Logic". Proceedings LACL'96, Nancy, France, septembre 96, LNCS 1328 pp. 96-117.

[19]. C. Fouqueré, J. Vauzeilles : "Taxonomic Linear Theories", ECSQARU 93, pp. 121-128, Grenade, Espagne, Novembre 93.

[20]. J. Vauzeilles : "Negation as Failure and Intuitionistic Three-Valued Logic". Proceedings International Workshop on Fundamentals of Artificial Intelligence Research, FAIR'91. Ph.Jorrand, J. Kelemen (Eds). Lectures Notes In Computer Science, 1991, p. 227-241.

[21]. M. Masseron, C. Tollu, J. Vauzeilles : "Plan Generation and Linear Logic". Proceedings of FST-TCS 10. Lectures Notes In Computer Science, 1990, p. 63-75.

[22]. C. Fouqueré, J. Vauzeilles : "Linear Logic for Taxonomical Networks and Database Updates", Electronic Notes in Theoretical Computer Science, vol.3, 1996, Proceedings of the Workshop on Linear Logic, Tokyo, Japan, March 1996.

[23].J. Vauzeilles : "Functors and ordinal notations III : dilators and gardens". Proceedings of the Herbrand Symposium, Marseille 1981. Stern (Ed), North Holland, 1982, p.333-364.

[24]. M. Masseron, C. Tollu, J. Vauzeilles : "Planification et Logique Linéaire", Revue d'Intelligence Artificielle. Octobre 1992, p. 285-311 (paru également dans les Proceedings 8ième Congrès Reconnaissance des Formes et Intelligence Artificielle, AFCET, 1991, p. 751-762)

[25]. J. Vauzeilles and A. Strauss : "Intuitionistic three-valued logic and logic programming". Theoretical Informatics and Applications, Vol 25, n° 6, 1991, p.557-587