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

DOI10.1016/J.JSC.2007.07.016MaRDI QIDQ1012152zbMATH OpenOpenAlexFDO

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

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

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)

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

Cites work

• scientific article; zbMATH DE number 3649988 (Why is no real title available?)
• scientific article; zbMATH DE number 621810 (Why is no real title available?)
• scientific article; zbMATH DE number 217454 (Why is no real title available?)
• A faster way to count the solutions of inhomogeneous systems of algebraic equations, with applications to cyclic \(n\)-roots
• A machine-checked implementation of Buchberger's algorithm
• 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
• Artificial Intelligence and Symbolic Computation
• Constructing recursion operators in intuitionistic type theory
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• The calculus of constructions
• VoDKA: Developing a Video-on-Demand Server using Distributed Functional Programming

Cited in

(5)

• Mathematical theory exploration in Theorema: reduction rings
• A verified common lisp implementation of Buchberger's algorithm in ACL2
• A generic and executable formalization of signature-based Gröbner basis algorithms
• Computer Aided Systems Theory – EUROCAST 2005
• A purely functional computer algebra system embedded in Haskell

Describes a project that uses

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)