- Dipl. Inf. Frank Theiß

"Have no way as way, have no form as form, have no limitation as limitation."
Bruce Lee


I am a freelance developer and make - among other things - software. I was a member of the ROTERFADEN team, a Saarbrücken based manufacturer of hand-sewed pocket calendars, where I was responsible for the "e" in eCommerce. I made the TASCHENBEGLEITER KONFIGURATOR, a tool for product customization.

My current focus is on development of industrial software in Linux-based Java EE environments (although I sometimes suspect there are more elegant languages than Java).

I am a Linux head and love grep, sed and shell scripts, and - after all - "Real Men use vi".

Programming languages: Ocaml ("Think more, type less.", OCaml's evil twin at Microsoft is F#), JavaScript (including frameworks such as jQuery), Lisp, Java EE, PHP, SQL.


I am doing research in the area of formal methods and artificial intelligence, with a focus on Automated Theorem Proving. My current project is LEO-II, a theorem prover for Higher-Order Logic. LEO-II is the winner of the THF division at CASC-J5 in 2010. I am also the author of the OCaml TPTP parser used in Satallax and contributed tiny bits to the TPTP ecosystem.

Beyond pure theorem proving, I have experience in the fields of Ontology Engineering, eLearning and Computer Algebra Systems.


I love doing live video performances and visual installations in clubs and at parties. It started quite a while ago with first experiments with ASCII graphics on green monitors in the legendary Untn and Super 8 installations at the party series "C'est dur la Culture".

Later I moved on to a laptop-and-video-mixer based setup - using OpenTZT - and had the chance to perform at occasions like Electricity Festival in Saarbrücken or at the Fête de Clôture of "Kulturhauptstadt Luxemburg" with such great people as Amon Tobin (Ninja Tune), and VJing took me as far as to the Lounge in Lisbon to perform with the tra$hconverters.


Here are some Lo-Fi loops from Lisboa I made for VJing. Technique is very simple, it's stop motion with my cell phone camera, and that's it. Feel free to use them.

There are also some clips on Vimeo.


Saarländischer Website Award 2011 Silver
The online shop for ROTERFADEN TASCHENBEGLEITER won the second place in the competition.
Saarländischer Website Award | ROTERFADEN TASCHENBEGLEITER

World Champion at CASC-J5
LEO-II is the winner of the THF division at the Cade System Competion 2010.
LEO-II did also participate in the FOF and CNF divisions and performed reasonably well.
5th International Joint Conference on Automated Reasoning (IJCAR)
Edinburgh, United Kingdom, 2010

Woody Bledsoe Travel Award
4th International Joint Conference on Automated Reasoning (IJCAR'08)
Sydney, Australia, 2008
IJCAR 2008


The Higher-Order Prover Leo-II
C. Benzmüller, N. Sultana, L. Paulson, F. Theiß
Journal of Automated Reasoning (JAR)

Progress in the Development of Automated Theorem Proving for Higher-order Logic
G. Sutcliffe, C. Benzmüller, C.E. Brown, and F. Theiss,
22nd Conference on Automated Deduction (CADE)
Montreal, Canada, 2009

LEO-II - A Cooperative Automatic Theorem Prover for Higher-Order Logic
C. Benzmüller, L. Paulson, F. Theiß, A.Fietzke
4th International Joint Conference on Automated Reasoning (IJCAR'08)
Sydney, Australia, 2008

Progress Report on LEO-II - An Automatic Theorem Prover for Higher-Order Logic
C. Benzmüller, L. Paulson, F. Theiß, A.Fietzke
Emerging Trends paper at the
20th International Conference on Theorem Proving in Higher-Order Logics, 2007

The LEO-II Project
C. Benzmüller, L. Paulson, F. Theiß, A.Fietzke
14th Workshop on Automated Reasoning, 2007

Term Indexing for the LEO-II Prover
F. Theiß, C. Benzmüller
6th International Workshop on the Implementation of Logics, 2006

Interfacing to Computer Algebra via Term Indexing
F. Theiß, V. Sorge, M. Pollet
Proceedings of the Calculemus Symposium 2006. Electronic Notes in Theoretical Computer Science, Elsevier.

On the White Box Integration of Computer Algebra Algorithms into a Deduction System
F. Theiß
Diploma Thesis, 2005

Automatic Generation of Algorithms and Tactics
F. Theiß, V. Sorge
Work in progress paper: Calculemus 2002.

Erdős Number

My Erdős number is 4:
Frank Theiß → Christoph Benzmüller → Dov Gabbay → Sharon Shelah → Paul Erdős


This is a selection of institutions, people and companies I have worked with, for or at:


Universität des Saarlandes DFKI University of Cambridge

Web and Design

ROTERFADEN TASCHENBEGLEITER Das Modul mangrig design Friskee Loge Saarbrücken


Kulturhauptstadt Luxemburg 2007 Electricity Festival Unsichtbar tra$hconverters (variz) Amon Tobin (Ninjatune)


Dipl. Inf. Frank Theiß
Tannenstraße 21
66129 Bübingen

mail: kontakt(at)


This website does not collect any personal data.