Buchberger's algorithm: Difference between revisions

Revision as of 06:33, 1 June 2025

Latest revision as of 14:35, 1 June 2025

(One intermediate revision by one other user not shown)

Line 38:

== Implementations ==

In the [[SymPy|SymPy library]] for [[Python (programming language)|Python]], the (improved) Buchberger algorithm is implemented as <code>sympy.polys.polytools.groebner()</code>.<ref>{{cite web |title=Polynomials Manipulation Module Reference - SymPy 1.14.0 documentation |url=https://docs.sympy.org/latest/modules/polys/reference.html#sympy.polys.polytools.groebner |website=docs.sympy.org}}</ref>

There is an implementation of Buchberger’s algorithm that has been proved correct

within the proof assistant [[Coq (proof assistant)|Coq]].<ref>{{cite journal |last1=Théry |first1=Laurent |title=A Machine-Checked Implementation of Buchberger's Algorithm |journal=Journal of Automated Reasoning |date=2001 |volume=26 |issue=2 |pages=107–137 |doi=10.1023/A:1026518331905}}</ref>

== See also ==