# René Thiemann

## Homepages 🌐

## Entries

### 2024

##### Undecidability Results on Orienting Single Rewrite Rules

by René Thiemann 🌐, Fabian Mitterwallner and Aart Middeldorp 🌐

### 2023

##### A Verified Efficient Implementation of the Weighted Path Order

by René Thiemann 🌐 and Elias Wenninger

### 2022

##### A Verified Translation of Multitape Turing Machines into Singletape Turing Machines

by Christian Dalvit and René Thiemann 🌐

### 2021

##### Regular Tree Relations

by Alexander Lochmann 📧, Bertram Felgenhauer, Christian Sternagel 🌐, René Thiemann 🌐 and Thomas Sternagel

##### 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

### 2019

##### 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 🌐, Max W. Haslbeck 🌐, Sebastiaan J. C. Joosten 🌐, René Thiemann 🌐 and Akihisa Yamada

### 2017

### 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 📧

### 2014

### 2013

### 2012

### 2011

### 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 🌐