Isabelle/HOL 中模的 Gröbner 基与 Faugère 的 $F_4$ 算法
计算机科学中的逻辑
2018-05-02 v1 符号计算
摘要
我们给出 Isabelle/HOL 中 Gröbner 基的一个优雅、通用且广泛的形式化。该形式化涵盖了该理论的所有要点（多项式约化、S-多项式、Buchberger 算法、Buchberger 避免无用对的判据），但也包含更高级的特性如约化 Gröbner 基。特别亮点是对 Faugère 基于矩阵的 算法的首次形式化，以及整个理论是针对模与子模而非环与理想表述的这一事实。所有形式化算法均可翻译为在 concrete 数据结构上运行的可执行代码，从而实现（约化）Gröbner 基与合冲模的认证计算。
引用
@article{arxiv.1805.00304,
title = {Gr\"obner Bases of Modules and Faug\`ere's $F_4$ Algorithm in Isabelle/HOL},
author = {Alexander Maletzky and Fabian Immler},
journal= {arXiv preprint arXiv:1805.00304},
year = {2018}
}
备注
extended version of paper submitted to CICM2018