Gr\"obner Bases of Modules and Faug\`ere's $F_4$ Algorithm in Isabelle/HOL

TL;DR

This paper provides a comprehensive formalization of Gr"obner bases and Fauger e's $F_4$ algorithm within Isabelle/HOL, covering modules, algorithms, and enabling certified computations.

Contribution

It introduces the first formalization of Fauger e's $F_4$ algorithm in Isabelle/HOL, extending Gr"obner basis theory to modules and submodules.

Findings

Formalization includes polynomial reduction, S-polynomials, Buchberger's algorithm, and criteria.

First-time formalization of Fauger e's $F_4$ algorithm.

Algorithms can be translated into executable code for certified computations.

Abstract

We present an elegant, generic and extensive formalization of Gr\"obner bases in Isabelle/HOL. The formalization covers all of the essentials of the theory (polynomial reduction, S-polynomials, Buchberger's algorithm, Buchberger's criteria for avoiding useless pairs), but also includes more advanced features like reduced Gr\"obner bases. Particular highlights are the first-time formalization of Faug\`ere's matrix-based $F_4$ algorithm and the fact that the entire theory is formulated for modules and submodules rather than rings and ideals. All formalized algorithms can be translated into executable code operating on concrete data structures, enabling the certified computation of (reduced) Gr\"obner bases and syzygy modules.