Jan Johannsen

Hi, welcome to my homepage!!

Research

• Propositional Proof Complexity. The study of the complexity of proofs of propositional tautologies in various proof systems is motivated by complexity theory, as well as by efficieny questions in automated theorem proving and satisfiability testing. I am interested most in the classical Resolution system and its refinements and extensions, which are closely related to the most common algorithms for boolean satisfiability testing.
  Together with Antonina Kolokolova I wrote the Proof Complexity Theme Song.
• Implicit Computational Complexity. In this area we search for machine-independent, resource-free characterizations of computational complexity classes, mostly using logical concepts and methods. I am especially interested in small classes below polynomial time which are closer to practical feasability.
• Temporal Logic and Model Checking. I am interested in the application of satisfiability methods in verification, in particular in Bounded Model Checking, as well as complexity and succinctness questions related to temporal and modal logics.
• Bounded Arithmetic. Theories of Bounded Arithmetic are theories of first- and second-order arithmetic that have a tight connection to computational complexity classes as well as to propositional proof systems. I am especially interested in applications of model-theoretic methods in this area.

Projects

• Pro.Platz - Programming language aspects of sublinear space complexity classes
• μ-Sabre - SAT-based verification of regular properties

My papers

Some unpublished notes

List of talks

Teaching

• Temporallogik (WS 2005/06) [Temporal Logic]
• Algorithmen für das SAT-Problem (WS 2002/03, SS 2005) [SAT algorithms]
• Komplexitätstheorie (WS 1999/2000, WS 2004/05) [Complexity Theory]
• Approximative und Probabilistische Algorithmen (WS 2003/04) [Randomized algorithms]
• Effiziente Algorithmen (SS 2002, SS 2003) [Efficient algorithms]
• Computergestütztes symbolisches Rechnen (WS 2001/02) [Symbolic Computation (Gröbner Bases)]
• Rechnergestütztes Beweisen (WS 2001/02) [Computer assisted Proofs]
• Approximationsverfahren für Optimierungsprobleme (WS 2000/01) [Approximation Algorithms for Optimization Problems]

Other stuff

My Erdös number is 3, e.g. through the path JJ - Toni Pitassi - Michael Saks - PE. Also, my Erdös number of the second kind (where only two-authored papers count) is 4, through the path JJ - Chris Pollett - Jeff Remmel - Janos Komlos - PE.

I participate in the Great Internet Mersenne Prime Search. Take a look at my results.

Fight Spam! Click Here!

Personal

I am awfully interested in any kind of good music, particularly in Jazz. I have recently started to play the tenor saxophone. Furthermore, I love cooking, especially of Asian (Indian and Thai) food.

How to contact me...

E-mail: MIT MAUSZEIGER LESBAR MACHEN! jan . johannsen { Klammeraffe } ifi PUNKT lmu PUNKT de or POINT MOUSE TO READ! jan . johannsen { AtSign } gmail DOT com

Phone: +49 89 2180 9140

Fax: +49 89 2180 9142

surface mail: Institut für Informatik · LFE Theoretische Informatik · Ludwig-Maximilians-Universität München · Oettingenstraße 67 · 80538 München · Germany

Office: 1.60

Mit dem Urteil vom 12. Mai 1998 hat das Landgericht Hamburg entschieden, daß man durch das Anbringen eines Links die Inhalte der verlinkten Seite ggf. mit zu verantworten hat. Dies kann, so das Landgericht, nur dadurch verhindert werden, indem man sich ausdrücklich von diesen Inhalten distanziert. Ich erkläre ausdrücklich, daß ich keinerlei Einfluß auf die Gestaltung und die Inhalte der Seiten habe, die man von dieser oder einer anderen meiner Webseiten über Links erreichen kann. Deshalb distanziere ich mich hiermit ausdrücklich von allen Inhalten aller von meinen Webseiten aus über Links erreichbaren Seiten und mache mir deren Inhalte nicht zu eigen.