Gb: une procédure de décision pour le système Coq
J. Creci and L. Pottier
Dans cet article, nous proposons une tactique pour le système Coq qui, grâce à des outils algébriques tels que les bases de Gröbner et le théorème des zéros de Hilbert, et grâce à la tactique Ring, permet de montrer que des égalités dans un anneau commutatif en impliquent une autre.
Journées Francophones des Langages Applicatifs 2004 (JFLA 2004).