René Thiemann

Homepages 🌐

• http://cl-informatik.uibk.ac.at/users/thiemann/

E-Mails 📧

• ta.ca.kbiu@nnameiht.ener

Entries

2025

First-Order Rewriting

by René Thiemann, Christian Sternagel, Christina Kirk, Martin Avanzini, Bertram Felgenhauer, Julian Nagele, Thomas Sternagel, Sarah Winkler and Akihisa Yamada

Apr 13

2024

A Preprocessor for Linear Diophantine Equalities and Inequalities

by René Thiemann

Jun 13

Sorted Terms

by Akihisa Yamada and René Thiemann

May 27

Verifying a Decision Procedure for Pattern Completeness

by René Thiemann and Akihisa Yamada

May 27

Undecidability Results on Orienting Single Rewrite Rules

by René Thiemann, Fabian Mitterwallner and Aart Middeldorp

Apr 25

2023

A Verified Efficient Implementation of the Weighted Path Order

by René Thiemann and Elias Wenninger

Jun 01

2022

A Verified Translation of Multitape Turing Machines into Singletape Turing Machines

by Christian Dalvit and René Thiemann

Nov 30

Clique is not solvable by monotone circuits of polynomial size

by René Thiemann

May 08

The Generalized Multiset Ordering is NP-Complete

by René Thiemann and Lukas Schmidinger

Apr 20

Duality of Linear Programming

by René Thiemann

Feb 03

2021

Regular Tree Relations

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

Dec 15

Factorization of Polynomials with Algebraic Coefficients

by Manuel Eberl and René Thiemann

Nov 08

A Formalization of Weighted Path Orders and Recursive Path Orders

by Christian Sternagel, René Thiemann and Akihisa Yamada

Sep 16

Solving Cubic and Quartic Equations

by René Thiemann

Sep 03

Two algorithms based on modular arithmetic: lattice basis reduction and Hermite normal form computation

by Ralph Bottesch, Jose Divasón and René Thiemann

Mar 12

The Sunflower Lemma of Erdős and Rado

by René Thiemann

Feb 25

2020

A Formalization of Knuth–Bendix Orders

by Christian Sternagel and René Thiemann

May 13

2019

Linear Inequalities

by Ralph Bottesch, Alban Reynaud and René Thiemann

Jun 21

Farkas' Lemma and Motzkin's Transposition Theorem

by Ralph Bottesch, Max W. Haslbeck and René Thiemann

Jan 17

2018

An Incremental Simplex Algorithm with Unsatisfiable Core Generation

by Filip Marić, Mirko Spasić and René Thiemann

Aug 24

A verified factorization algorithm for integer polynomials with polynomial complexity

by Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann and Akihisa Yamada

Feb 06

First-Order Terms

by Christian Sternagel and René Thiemann

Feb 06

A verified LLL algorithm

by Ralph Bottesch, Jose Divasón, Max W. Haslbeck, Sebastiaan J. C. Joosten, René Thiemann and Akihisa Yamada

Feb 02

2017

Stochastic Matrices and the Perron-Frobenius Theorem

by René Thiemann

Nov 22

Subresultants

by Sebastiaan J. C. Joosten, René Thiemann and Akihisa Yamada

Apr 06

2016

The Factorization Algorithm of Berlekamp and Zassenhaus

by Jose Divasón, Sebastiaan J. C. Joosten, René Thiemann and Akihisa Yamada

Oct 14

Perron-Frobenius Theorem for Spectral Radius Analysis

by Jose Divasón, Ondřej Kunčar, René Thiemann and Akihisa Yamada

May 20

Polynomial Interpolation

by René Thiemann and Akihisa Yamada

Jan 29

Polynomial Factorization

by René Thiemann and Akihisa Yamada

Jan 29

2015

Algebraic Numbers in Isabelle/HOL

by René Thiemann, Akihisa Yamada and Sebastiaan J. C. Joosten

Dec 22

Matrices, Jordan Normal Forms, and Spectral Radius Theory

by René Thiemann and Akihisa Yamada

Aug 21

Deriving class instances for datatypes

by Christian Sternagel and René Thiemann

Mar 11

2014

Lifting Definition Option

by René Thiemann

Oct 13

XML

by Christian Sternagel, René Thiemann and Akihisa Yamada

Oct 03

Certification Monads

by Christian Sternagel and René Thiemann

Oct 03

Haskell's Show Class in Isabelle/HOL

by Christian Sternagel and René Thiemann

Jul 29

Mutually Recursive Partial Functions

by René Thiemann

Feb 18

Implementing field extensions of the form Q[sqrt(b)]

by René Thiemann

Feb 06

2013

Computing N-th Roots using the Babylonian Method

by René Thiemann

Jan 03

2012

Generating linear orders for datatypes

by René Thiemann

Aug 07

Executable Transitive Closures

by René Thiemann

Feb 29

2011

Executable Transitive Closures of Finite Relations

by Christian Sternagel and René Thiemann

Mar 14

2010

Executable Multivariate Polynomials

by Christian Sternagel, René Thiemann, Alexander Maletzky, Fabian Immler, Florian Haftmann, Andreas Lochbihler and Alexander Bentkamp

Aug 10

Executable Matrix Operations on Matrices of Arbitrary Dimensions

by Christian Sternagel and René Thiemann

Jun 17

Abstract Rewriting

by Christian Sternagel and René Thiemann

Jun 14