9 citations · 15 across the 13 of their papers we have counts for
13 papers
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…
f4ncgb: High Performance Gröbner Basis Computations in Free Algebras
Maximilian Heisinger, Clemens Hofstadler
We present f4ncgb, a new open-source C++ library for Gröbner basis computations in free algebras, which transfers recent advancements in commutative Gröbner basis software to the n…
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…
Symmetries of Dependency Quantified Boolean Formulas
Clemens Hofstadler, Manuel Kauers, Martina Seidl
Symmetries have been exploited successfully within the realms of SAT and QBF to improve solver performance in practical applications and to devise more powerful proof systems. As a…
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…
Signature Gröbner bases in free algebras over rings
Clemens Hofstadler, Thibaut Verron
We generalize signature Gröbner bases, previously studied in the free algebra over a field or polynomial rings over a ring, to ideals in the mixed algebra $R[x_1,...,x_k]\langle y_…
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…
Universal truth of operator statements via ideal membership
Clemens Hofstadler, Clemens G. Raab, Georg Regensburger
We introduce a framework for proving statements about linear operators by verification of ideal membership in a free algebra. More specifically, arbitrary first-order statements ab…
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…
Algebraic proof methods for identities of matrices and operators: improvements of Hartwig's triple reverse order law
Dragana S. Cvetković-Ilić, Clemens Hofstadler, Jamal Hossein Poor +3
When improving results about generalized inverses, the aim often is to do this in the most general setting possible by eliminating superfluous assumptions and by simplifying some o…
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,…