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

v8.16.0.tar.gz
sha512=e4dc3757e2ac1129ab767beaf55dfbf38eb678b84c4884968972baccb7d7532503a938093dd5d219b047f6c2c858738ef0f525050814aa2764db5dc53cbb6a9b

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:2022-09-11

Published: 11 Sep 2022

Dependencies (1)

  1. coq >= "8.16" & < "8.17~"

Dev Dependencies

None

Used by

None

Conflicts

None