package coq-buchberger

  1. Overview
  2. No Docs
Verified implementation in Coq of Buchberger's algorithm for computing Gröbner bases

Install

Dune Dependency

github.com Edit opam file Versions (12)

Authors

  1. L
    Laurent Théry
  2. H
    Henrik Persson

Maintainers

  1. P
    palmskog@gmail.com

Sources

buchberger-8.18.0.tar.gz
sha512=ce7afdfe719c06776f97939663235cba639e12ea85bd9ddb90599ce27763e0b4495aa6c05b92725ee414c4b2076243984ab96fafb080f0ec8689f07bf040367d

Description

A verified implementation of Buchberger's algorithm in Coq, which computes the Gröbner basis associated with a polynomial ideal. Also includes a constructive proof of Dickson's lemma.

Tags

category:Mathematics/Algebra category:Miscellaneous/Extracted Programs/Combinatorics keyword:Gröbner basis keyword:polynomial ideal keyword:Buchberger's algorithm logpath:Buchberger date:2023-12-28

Published: 28 Dec 2023

Dependencies (1)

  1. coq >= "8.17" & < "8.20"

Dev Dependencies

None

Used by

None

Conflicts

None