The official Homepage of Martin Giese

Hier steht die deutsche Version dieser Seite.

I work at the Institut für Logik, Komplexität und Deduktionssysteme (i.e. institute for logic, complexity and deduction systems) of the Universität Karlsruhe in the group of Prof. W. Menzel.

Address

Current Work

I am responsible for work on the deduction component that is part of the ongoing KeY project.

I am particularly interested in:

• Tableau-based backtracking-free proof procedures for predicate logic,
• Equality reasoning in tableaux,
• Integration of interactive and automated theorem proving,
• Implementation of proof systems in Java.

I am also more or less involved with the supervision of two diploma thesis on pretty printng: how to synchronise generated parsers and pretty printers, how to get nice indentations, and how to implement that in Java.

In the summer term of 2001, I helped with the computability lecture of Prof. Menzel. See here for details (in German).

I have compiled a little collection of ideas, I should like to investigate if I had time.

Paper

Here are some internal papers I wrote for the KeY project, some of which are in english. Access is restricted to domains i11 and i12 of the Universität Karlsruhe!

Conference and Workshop papers

• Martin Giese. A Model Generation Style Completeness Proof for Constraint Tableaux with Superposition. Proceedings of Tableaux 2002. (bibtex Eintrag)
• Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Reiner Hähnle, Wolfram Menzel, Wojciech Mostowski and Peter H. Schmitt. The KeY System: Integrating Object-Oriented Design and Formal Methods. Proceedings of FASE at ETAPS 2002, to appear. (bibtex entry)
• Martin Giese. Incremental Closure of Free Variable Tableaux. Presented at the Intl. Joint Conf. on Automated Reasoning, IJCAR 2001 Siena, Italy, 2001. (bibtex entry)
• Martin Giese. A First-Order Simplification Rule with Constraints. Presented at the Int. Workshop on First-Order Theorem Proving, St. Andrews, Scotland, 2000. (bibtex entry)
• Martin Giese. Proof Search without Backtracking using Instance Streams. Position paper presented at the Int. Workshop on First-Order Theorem Proving, St. Andrews, Scotland, 2000. (bibtex entry)
• M. Giese and W. Ahrendt. Hilbert's Epsilon terms in Automated Theorem Proving. In Neil V. Murray, editor, Automated Reasoning with Analytic Tableaux and Related Methods, Intl. Conf. (TABLEAUX'99), LNCS 1617, pp. 171-185. Springer, 1999. (bibtex entry)

Technical Reports

• M. Giese. Model Generation Style Completeness Proofs for Constraint Tableaux with Superposition. Technical Report 2001-20, Fakultät für Informatik, Universität Karlsruhe, 76128 Karlsruhe, Germany, 1997.

My diploma thesis (german) as ~540kB gzip'ed PostScript.

• M. Giese. Integriertes automatisches und interaktives Beweisen: Die Kalkülebene. Diplomarbeit, Fakultät für Informatik, Universität Karlsruhe, 76128 Karlsruhe, Germany, 1998. (bibtex Eintrag)

Other things I wrote as a student:

• M. Giese. Partielle Monomorphie algebraischer Spezifikationen: Definition und Nachweis. Studienarbeit, Fakultät für Informatik, Universität Karlsruhe, 76128 Karlsruhe, Germany, 1996.
• M. Giese and A. Schönegge. Any two countable, densely ordered sets without endpoints are isomorphic - a formal proof with KIV. Technical Report 50/95, Fakultät für Informatik, Universität Karlsruhe, 76128 Karlsruhe, Germany, 1995.
• M. Giese, D. Kempe and A. Schönegge. KIV zur Verifikation von ASM-Spezifikationen am Beispiel der DLX-Pipelining Architektur. Technical Report 16/97 Fakultät für Informatik, Universität Karlsruhe, 76128 Karlsruhe, Germany, 1997.

There is also a private homepage, but its content is inherently german.