6 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…