I am a senior lecturer and docent in Computing Science at the
Computing Science Department
University of Göteborg and the Chalmers University of Technology.

• Email: tammet@cs.chalmers.se
• Phone: +46-31-7721053
• Fax: +46-31-165655
• Mailing address: Chalmers Tekniska Högskola, Institutionen för Datavetenskap, S-412 96 Göteborg, Sweden.
• Street address: Eklandagatan 86, 4. floor, room 2451.

Research interests

I like hacking and running the provers. It is exciting: like fishing combined with chess combined with philosophy combined with car races.

My prover Gandalf won the last CASC-15 and CASC-14, the yearly competitions of classical first order automated theorem provers. Click for the competition results for CASC-15 and CASC-14 .

• Gandalf home page
• Overview of research
• Overview of teaching
• The papers
• A short CV.

Current teaching

• Spring 1998: Postgraduate course "Equational Reasoning"
• Spring 1998: Systemprogrammering i C.
• Autumn 1997: Programmeringsprojekt.
• Autumn 1997: Algoritmer.

Some recent ftp-able papers

• T.Tammet. 'Resolution, Inverse method and the Sequent Calculus'.

In 'Computational Logic and Proof Theory', proceedings of the 5th Kurt Gödel Colloquium KCG'97, Vienna. Springer LNCS 1289, pp. 65-83.
• T.Tammet, 'Gandalf',

J. of Automated Reasoning vol 18 No 2 (1997) 199-204.
A brief overview of the old and weak version of Gandalf.
Get the manual of the new version.,
• T.Tammet, J.M.Smith. 'Optimized Encodings of Fragments of Type Theory in First Order Logic',

presented at the BRA TYPES workshop, Torino 1995.
Springer LNCS 1158, pp 265-287, 1996.
• T.Tammet. 'A Resolution Theorem Prover for Intuitionistic Logic' ,

a full version of the shorter 15-page paper presented at CADE-13:
Springer LNCS 1104, pp 2-16, 1996.
• G.Mints, V.Orevkov, T.Tammet. 'Transfer of Sequent Calculus Strategies to Resolution for S4' , In the Proof Theory of Modal Logic, the Applied Logic Series nr 2 of Kluwer Academic Publishers, 1996.
• T.Tammet. 'Completeness of Resolution for Definite Answers' ,

a slightly enlarged version of the paper published in the J. of Logic and Computation, 5(4): pp. 449-471, July 1995.
A techreport-version (Programming Methodology Group report 79, Chalmers University of Technology, 1994, ISSN 0282-2083) is also available.
• T.Tammet. 'Using Resolution for Extending KL-ONE-type Languages', Proceedings of the CIKM'95, ACM Press, 1995.
• T.Tammet. 'Proof Strategies in Linear Logic' ,

J. of Automated Reasoning 12: 273-304, 1994.
Click here to get the C source of the provers.
• T.Tammet. 'Lambda-lifting as an Optimization for Compiling Scheme to C' ,

an unpublished draft paper describing the main aspects of the compilation scheme used by the Hobbit compiler.
Click here to get the compiler itself.
• T.Tammet. 'Resolution methods for decision problems and finite-model building' ,

a Ph.D. thesis, Göteborg University, 1992, ISBN 91-7032-644-4.
NB! Postscript source compressed with gzip.

Free ftp-able software

• Automated theorem provers of the Gandalf family
• Automated theorem provers for linear logic
• C source of a tableau theorem prover and a resolution theorem prover for full propositional linear logic.
• Manual for the prover.
• The paper 'Proof Strategies in Linear Logic' mentioned above.
• Scheme-to-C compiler Hobbit. Hobbit version 4 compiles full Report 4 Scheme. You will almost certainly need the latest version (at least one produced not earlier than March 1995) of Aubrey Jaffer's scm4e2 (see the following) to get Hobbit work OK.
• The newest release of Hobbit, version 4d. Differently from all the older versions, the version 4d is free software covered by the GNU General Public Licence.
• Documentation of hobbit.
• The paper 'Lambda-lifting as an Optimization for Compiling Scheme to C' mentioned above.
• The development version of scm4e2 at ftp-swiss.ai.mit.edu:pub/users/jaffer/scm.zip.
• More information about scm, SLIB, GUILE and JACAL.
• Documentation for SLIB
• Scheme standard, a HTML version of the Revised 4 Scheme Report.
• A Scheme home page at MIT
• Older version (4c) of Hobbit ,
• Yet older version (3d) of Hobbit .