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.13.0.tar.gz
sha512=24df93c460202a2ec6c7bb772a6af3342333388e46fa3589461de4992157fca73d959c3b5037ee85b4b4febab43ad6ff9e1db99f63d73d7995a0d2b4ae38aadd

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:2021-08-01

Published: 01 Aug 2021

Dependencies (1)

  1. coq >= "8.12" & < "8.15~"

Dev Dependencies

None

Used by

None

Conflicts

None