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.17.0.tar.gz
sha512=923ab0126c3389e1e8e2cb8460a437c8252f69b2ed3c876a5c66025bd4ee3d683fcf1a818ff1a5f00e4025e4b5e27aae59556c1fa6bfebc939684c022b5e983f

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-10-06

Published: 07 Oct 2023

Dependencies (1)

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

Dev Dependencies

None

Used by

None

Conflicts

None