Skip to Main content Skip to Navigation

An Integrated Development of Buchberger's Algorithm in Coq

Henrik Persson 1
1 LEMME - Software and mathematics
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : We present an integrated formal development of Buchberger's algorithm in Coq, that is we prove constructively the existence of Gröbner bases without explicitly writing the algorithm. This formalisation is based on an external formalisation in Coq by Théry, and an integrated abstract development in Agda. We end by discussing some experiences and differences between the two proof-styles and theorem-provers. This report was completed in March 2000.
Document type :
Complete list of metadatas
Contributor : Rapport de Recherche Inria <>
Submitted on : Tuesday, May 23, 2006 - 8:23:01 PM
Last modification on : Saturday, January 27, 2018 - 1:30:58 AM
Document(s) archivé(s) le : Sunday, April 4, 2010 - 11:03:23 PM


  • HAL Id : inria-00072316, version 1



Henrik Persson. An Integrated Development of Buchberger's Algorithm in Coq. RR-4271, INRIA. 2001. ⟨inria-00072316⟩



Record views


Files downloads