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.14.0.tar.gz
sha512=bb38c3b1e658698fe457a91b8507f19797dbb82214edf58166880c6e0e1fe0b8093b8c67c9dfeac2495db118bf83322139c4518458e63004b7693d58f8b84fd8

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-12-12

Published: 12 Dec 2021

Dependencies (1)

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

Dev Dependencies

None

Used by

None

Conflicts

None