Short proofs of ideal membership

A cofactor representation of an ideal element, that is, a representation in terms of the generators, can be considered as a certificate for ideal membership. Such a representation is typically not unique, and some can be a lot more complicated than others. In this work, we consider the problem of co...

Full description

Saved in:
Bibliographic Details
Published in:Journal of symbolic computation 2024-11, Vol.125, p.102325, Article 102325
Main Authors: Hofstadler, Clemens, Verron, Thibaut
Format: Article
Language:English
Subjects:
Automated proofs
Linear programming
Noncommutative polynomials
Proof simplification
Signature Gröbner basis
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:A cofactor representation of an ideal element, that is, a representation in terms of the generators, can be considered as a certificate for ideal membership. Such a representation is typically not unique, and some can be a lot more complicated than others. In this work, we consider the problem of computing sparsest cofactor representations, i.e., representations with a minimal number of terms, of a given element in a polynomial ideal. While we focus on the more general case of noncommutative polynomials, all results also apply to the commutative setting. We show that the problem of computing cofactor representations with a bounded number of terms is decidable and NP-complete. Moreover, we provide a practical algorithm for computing sparse (not necessarily optimal) representations by translating the problem into a linear optimization problem and by exploiting properties of signature-based Gröbner basis algorithms. We show that, for a certain class of ideals, representations computed by this method are actually optimal, and we present experimental data illustrating that it can lead to noticeably sparser cofactor representations.
ISSN:0747-7171
1095-855X
DOI:10.1016/j.jsc.2024.102325