home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #31 / NN_1992_31.iso / spool / fnet / seminair / 73 < prev    next >
Encoding:
Internet Message Format  |  1992-12-24  |  1.6 KB
  1. Path: sparky!uunet!opl.com!cass.ma02.bull.com!mips2!bull.bull.fr!julienas!seti!dmi.ens.fr
  2. From: lavatel@dmi.ens.fr (Carolina Lavatelli)
  3. Newsgroups: fnet.seminaires
  4. Subject: H. Comon. Completion de systemes de reecriture contraints
  5. Message-ID: <4739@seti.inria.fr>
  6. Date: 17 Dec 92 16:11:07 GMT
  7. Sender: news@seti.inria.fr
  8. Distribution: fnet
  9. Lines: 32
  10. Approved: xleroy@margaux.inria.fr
  11. Jour: 12/01/92
  12. Lieu: Ecole Normale Superieure, Paris
  13.  
  14.  
  15. Seminaire Semantique Preuves et Programmation
  16. ********************
  17.  
  18. TITRE: Completion de systemes de reecriture contraints
  19.  
  20.  
  21. NOM: Hubert Comon, L.R.I. (Orsay)
  22.  
  23.  
  24.  
  25. DATE:  Mardi 12 janvier  a 11 hs. 
  26.  
  27. LIEU:  Salle Verdier (passage vert). Ecole Normale Superieure 
  28. (45, rue d'Ulm. Paris 05).
  29.  
  30. RESUME:  
  31.  
  32. Un systeme de contraintes symboliques est un ensemble de formules
  33. interpretees dans une structure fixe de termes. L'adjonction de telles
  34. contraintes a des regles de reecriture permet d'une part de
  35. representer des ensembles tres grands (ou infinis) de regles et 
  36. d'autre part d'exprimer des strategies au niveau des regles elles-memes. 
  37.  
  38. Je donnerai les exemples des strategies basique et ordonnee, puis je me
  39. concentrerai sur les problemes de completion de systemes de reecriture
  40. contraints par l'appartenance a des langages d'arbres. Les regles de 
  41. deduction habituelles ne suffisant plus (le lemme des paires critiques 
  42. n'est plus vrai), la logique est enrichie par l'introduction de variables 
  43. "de second ordre" et les regles de deduction correspondantes. Je montrerai 
  44. finalement que les contraintes de second ordre qu'il faut considerer sont 
  45. effectivement decidables. 
  46.