Skip to Main content Skip to Navigation
Reports

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 metadata

https://hal.inria.fr/inria-00072316
Contributor : Rapport de Recherche Inria Connect in order to contact the contributor
Submitted on : Tuesday, May 23, 2006 - 8:23:01 PM
Last modification on : Friday, February 4, 2022 - 3:18:29 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

60

Files downloads

221