Certifying operator identities via noncommutative Gröbner bases. - Clemens Hofstadler; Clemens G. Raab; Georg Regensburger (ACM Commun. Comput. Algebra, 2019)

Compatible rewriting of noncommutative polynomials for proving operator identities. - Cyrille Chenavier; Clemens Hofstadler; Clemens G. Raab; Georg Regensburger (ISSAC, 2020)

Algebraic proof methods for identities of matrices and operators: Improvements of Hartwig's triple reverse order law. - Dragana S. Cvetkovic-Ilic; Clemens Hofstadler; Jamal Hossein Poor; Jovana Milosevic; Clemens G. Raab; Georg Regensburger (Appl. Math. Comput., 2021)

Signature Gröbner bases, bases of syzygies and cofactor reconstruction in the free algebra. - Clemens Hofstadler; Thibaut Verron (J. Symb. Comput., 2022)

Computing Elements of Certain Form in Ideals to Prove Properties of Operators. - Clemens Hofstadler; Clemens G. Raab; Georg Regensburger (Math. Comput. Sci., 2022)

How to Automatise Proofs of Operator Statements: Moore-Penrose Inverse; A Case Study. - Klara Bernauer; Clemens Hofstadler; Georg Regensburger (CASC, 2023)

Signature Gröbner bases in free algebras over rings. - Clemens Hofstadler; Thibaut Verron (ISSAC, 2023)

Symmetries of Dependency Quantified Boolean Formulas. - Clemens Hofstadler; Manuel Kauers; Martina Seidl (CoRR, 2024)

Short proofs of ideal membership. - Clemens Hofstadler; Thibaut Verron (J. Symb. Comput., 2024)

Guess and Prove: A Hybrid Approach to Linear Polynomial Recovery in Circuit Verification. - Clemens Hofstadler; Daniela Kaufmann (CP, 2025)

Refinement-Based Enumeration of QBF Solutions. - Andreas Plank; Clemens Hofstadler; Maximilian Heisinger; Martina Seidl (JELIA (2), 2025)

Modular Algorithms For Computing Gröbner Bases in Free Algebras. - Clemens Hofstadler; Viktor Levandovskyy (CoRR, 2025)

f4ncgb: High Performance Gröbner Basis Computations in Free Algebras. - Maximilian Heisinger; Clemens Hofstadler (CoRR, 2025)

Recycling Algebraic Proof Certificates. - Daniela Kaufmann; Clemens Hofstadler (CoRR, 2025)