package coq-buchberger

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

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.11.0.tar.gz
sha512=a048ee35574090d2ffa6b8c6a5e4379bb5f7699e0b84c1c4781fb624d151faca02eb9122bae2d21296ba6dbe57adb116edaa1255a5475b1cbafe89d33d364a05

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:2020-05-27

Published: 27 May 2020

Dependencies (1)

  1. coq >= "8.7" & < "8.13~"

Dev Dependencies

None

Used by

None

Conflicts

None