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 :
Reports
Complete list of metadatas

https://hal.inria.fr/inria-00072316
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
Long-term archiving on : Sunday, April 4, 2010 - 11:03:23 PM

Identifiers

  • HAL Id : inria-00072316, version 1

Collections

Citation

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

Share

Metrics

Record views

91

Files downloads

248