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

Development

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.

Research

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.

Video

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.

Lisboa!

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.

Awards

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
LEO-II | CASC-J5

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

Publications

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

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
pdf|bibtex

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
pdf|bibtex

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
pdf|bibtex

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

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

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.
ps|pdf|bibtex

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

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