An Integrated Development of Buchberger's Algorithm in Coq

Henrik Persson (1)

1 LEMME - Software and mathematics

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.

Mots clés: BUCHBERGER'S ALGORITHM; THEOREM PROVING; COMPUTER ALGEBRA; INTEGRATED PROGRAMMING LOGIC; COQ; AGDA

Domaines: Autre [cs.OH]

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