A Generic and Executable Formalization of Signature-Based Gr\'obner Basis Algorithms
| Autor: | Alexander Maletzky |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2020 |
| Předmět: |
Computer Science - Symbolic Computation
Algebra and Number Theory Correctness 010102 general mathematics Proof assistant HOL 010103 numerical & computational mathematics computer.file_format 01 natural sciences Signature (logic) Zero (linguistics) Computational Mathematics Gröbner basis Detect and avoid ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION Computer Science::Symbolic Computation Executable 0101 mathematics Algorithm computer Mathematics |
| Popis: | We present a generic and executable formalization of signature-based algorithms (such as Faugere's F 5 ) for computing Grobner bases, as well as their mathematical background, in the Isabelle/HOL proof assistant. Said algorithms are currently the best known algorithms for computing Grobner bases in terms of computational efficiency. The formal development attempts to be as generic as possible, generalizing most known variants of signature-based algorithms, but at the same time the implemented functions are effectively executable on concrete input for efficiently computing mechanically verified Grobner bases. Besides correctness the formalization also proves that under certain conditions the algorithms a-priori detect and avoid all useless reductions to zero, and return minimal signature Grobner bases. To the best of our knowledge, the formalization presented here is the only formalization of signature-based Grobner basis algorithms in existence so far. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|