9 citations · 15 across the 13 of their papers we have counts for
8 papers · 1 filter
Avoiding Big Integers: Parallel Multimodular Algebraic Verification of Arithmetic Circuits
Clemens Hofstadler, Daniela Kaufmann, Chen Chen
Word-level verification of arithmetic circuits with large operands typically relies on arbitrary-precision arithmetic, which can lead to significant computational overhead as word…
Recycling Algebraic Proof Certificates
Daniela Kaufmann, Clemens Hofstadler
Proof certificates can be used to validate the correctness of algebraic derivations. However, in practice, we frequently observed that the exact same proof steps are repeated for d…
Modular Algorithms For Computing Gröbner Bases in Free Algebras
Clemens Hofstadler, Viktor Levandovskyy
In this work, we extend modular techniques for computing Gröbner bases involving rational coefficients to (two-sided) ideals in free algebras. We show that the infinite nature of G…
How to automatise proofs of operator statements: Moore-Penrose inverse -- a case study
Klara Bernauer, Clemens Hofstadler, Georg Regensburger
We describe a recently developed algebraic framework for proving first-order statements about linear operators by computations with noncommutative polynomials. Furthermore, we pres…
Short proofs of ideal membership
Clemens Hofstadler, Thibaut Verron
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…
Computing elements of certain form in ideals to prove properties of operators
Clemens Hofstadler, Clemens G. Raab, Georg Regensburger
Proving statements about linear operators expressed in terms of identities often leads to finding elements of certain form in noncommutative polynomial ideals. We illustrate this b…
Signature Gröbner bases, bases of syzygies and cofactor reconstruction in the free algebra
Clemens Hofstadler, Thibaut Verron
Signature-based algorithms have become a standard approach for computing Gröbner bases in commutative polynomial rings. However, so far, it was not clear how to extend this concept…
Compatible rewriting of noncommutative polynomials for proving operator identities
Cyrille Chenavier, Clemens Hofstadler, Clemens G. Raab +1
The goal of this paper is to prove operator identities using equalities between noncommutative polynomials. In general, a polynomial expression is not valid in terms of operators,…