Clique is not solvable by monotone circuits of polynomial size
by René Thiemann
René Thiemann
2022
The Generalized Multiset Ordering is NP-Complete
by René Thiemann and Lukas Schmidinger
2021
Regular Tree Relations
by Alexander Lochmann, Bertram Felgenhauer, Christian Sternagel, René Thiemann and Thomas Sternagel
Factorization of Polynomials with Algebraic Coefficients
by Manuel Eberl and René Thiemann
A Formalization of Weighted Path Orders and Recursive Path Orders
by Christian Sternagel, René Thiemann and Akihisa Yamada
Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation
by Ralph Bottesch, Jose Divasón and René Thiemann
2020
A Formalization of Knuth–Bendix Orders
by Christian Sternagel and René Thiemann
2019
Linear Inequalities
by Ralph Bottesch, Alban Reynaud and René Thiemann
Farkas' Lemma and Motzkin's Transposition Theorem
by Ralph Bottesch, Max W. Haslbeck and René Thiemann
2018
An Incremental Simplex Algorithm with Unsatisfiable Core Generation
by Filip Marić, Mirko Spasić and René Thiemann
A verified factorization algorithm for integer polynomials with polynomial complexity
by Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann and Akihisa Yamada
A verified LLL algorithm
by Ralph Bottesch, Jose Divasón, Maximilian P. L. Haslbeck, Sebastiaan J. C. Joosten, René Thiemann and Akihisa Yamada
2017
Stochastic Matrices and the Perron-Frobenius Theorem
by René Thiemann
Subresultants
by Sebastiaan J. C. Joosten, René Thiemann and Akihisa Yamada
2016
The Factorization Algorithm of Berlekamp and Zassenhaus
by Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann and Akihisa Yamada
Perron-Frobenius Theorem for Spectral Radius Analysis
by Jose Divasón, Ondřej Kunčar, René Thiemann and Akihisa Yamada
2015
Algebraic Numbers in Isabelle/HOL
by René Thiemann, Akihisa Yamada and Sebastiaan J. C. Joosten
Matrices, Jordan Normal Forms, and Spectral Radius Theory
by René Thiemann and Akihisa Yamada
Deriving class instances for datatypes
by Christian Sternagel and René Thiemann
2014
Certification Monads
by Christian Sternagel and René Thiemann
Haskell's Show Class in Isabelle/HOL
by Christian Sternagel and René Thiemann
Implementing field extensions of the form Q[sqrt(b)]
by René Thiemann
2013
Computing N-th Roots using the Babylonian Method
by René Thiemann
2012
2011
Executable Transitive Closures of Finite Relations
by Christian Sternagel and René Thiemann
2010
Executable Multivariate Polynomials
by Christian Sternagel, René Thiemann, Alexander Maletzky, Fabian Immler, Florian Haftmann, Andreas Lochbihler and Alexander Bentkamp
Executable Matrix Operations on Matrices of Arbitrary Dimensions
by Christian Sternagel and René Thiemann