René Thiemann

Homepages 🌐

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

Entries

2024

A Preprocessor for Linear Diophantine Equalities and Inequalities

by René Thiemann 🌐

Jun 13

Verifying a Decision Procedure for Pattern Completeness

by René Thiemann 🌐 and Akihisa Yamada 📧

May 27

Sorted Terms

by Akihisa Yamada 📧 and René Thiemann 🌐

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

First-Order Terms

by Christian Sternagel 📧 and René Thiemann 🌐

Feb 06

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

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