Syst\`emes holon\^omes et preuve automatique d'identit\'es

Nous pr\'esentons les fondements th\'eoriques de notre implantation de fonctions holon\^omes en plusieurs variables. Pour consid\'erer des probl\`emes mixtes diff\'erence-diff\'erentiels, nous d\'efinissons un cadre alg\'ebrique unificateur. Les techniques utilis\'ees pour implanter les riches propri\'et\'es de cl\^oture des fonctions holon\^omes, notamment la diagonale, se fondent sur l'\'elimination diff\'erentielle. Ceci nous a conduit \`a implanter un calcul de bases de Gr\"obner diff\'erentielles. De nombreux probl\`emes issus de la combinatoire sont calculables automatiquement par l'holonomie, nous en montrerons quelques exemples.