Certifying properties of an efficient functional program for computing Gröbner bases

DOI10.1016/J.JSC.2007.07.016zbMATH Open1159.13016OpenAlexW2002003982MaRDI QIDQ1012152FDOQ1012152

J. Santiago Jorge, Jose L. Freire, Victor M. Gulias

Publication date: 14 April 2009

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jsc.2007.07.016

Recommendations

• Computer Aided Systems Theory – EUROCAST 2005
• Artificial Intelligence and Symbolic Computation
• Gröbner bases of modules and Faugère's \(F_4\) algorithm in Isabelle/HOL
• A generic and executable formalization of signature-based Gröbner basis algorithms
• scientific article; zbMATH DE number 1303350

zbMATH Keywords

functional programmingformal methodssoftware verificationBuchberger's algorithmtheorem proversGröbner bases

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30) Gröbner bases; other bases for ideals and modules (e.g., Janet and border bases) (13P10)

Cites Work

• A new efficient algorithm for computing Gröbner bases \((F_4)\)
• An algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal
• A faster way to count the solutions of inhomogeneous systems of algebraic equations, with applications to cyclic \(n\)-roots
• Title not available (Why is that?)
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Title not available (Why is that?)
• Title not available (Why is that?)
• The calculus of constructions
• Artificial Intelligence and Symbolic Computation
• Constructing recursion operators in intuitionistic type theory
• A machine-checked implementation of Buchberger's algorithm
• VoDKA: Developing a Video-on-Demand Server using Distributed Functional Programming

Cited In (3)

• A generic and executable formalization of signature-based Gröbner basis algorithms
• Mathematical Theory Exploration in Theorema: Reduction Rings
• A verified common lisp implementation of Buchberger's algorithm in ACL2

Uses Software

• ACL2
• Coq
• FGb
• VoDKA
• PoSSo
• OCaml
• Caml

This page was built for publication: Certifying properties of an efficient functional program for computing Gröbner bases

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1012152)