Die ehemalige offizielle Homepage von Martin Giese

Click here for the english version of this page.

Ich bin Mitarbeiter am Lehrstuhl Prof. W. Menzel des Instituts für Logik, Komplexität und Deduktionssysteme an der Universität Karlsruhe.

Adresse

Aktuelle Arbeit

Im Rahmen des KeY Projekts am ILKD bin ich für das Deduktionssystem zuständig.

Insbesondere interessiere ich mich für:

• Backtracking-freie Tableau-Beweisprozeduren für Prädikatenlogik,
• Gleichheitsbehandlung in Tableaux,
• Integration von interaktivem und automatischem Theorembeweisen,
• Beweiserimplementierung in Java.

Auch bin ich zur Zeit an der Betreuung zweier Diplomarbeiten zum Thema Pretty-Printing beteiligt: Wie man automatisch generierte Parser und Pretty-Printer synchronisiert, wie man schöne Einrückungen bekommt, und wie das ganze als Java Implementierung aussehen kann.

Ferner habe ich im Sommersemester 2001 die Übungen zur Vorlesung "Berechenbarkeit" von Prof. Menzel gehalten. Näheres dazu hier.

Es gibt auch eine kleine Sammlung von Ideen (auf englisch), die ich gerne weiter verfolgen würde, wenn ich denn Zeit dazu hätte.

Papier

Hier finden sich jene internen Arbeitspapiere zum KeY Projekt, die von mir stammen. Nur von den Domains i11/i12 zugreifbar!

Beiträge zu Konferenzen und Workshops

• 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 und Peter H. Schmitt. The KeY System: Integrating Object-Oriented Design and Formal Methods. Proceedings of FASE at ETAPS 2002. (bibtex Eintrag)
• Martin Giese. Incremental Closure of Free Variable Tableaux. Presented at the Intl. Joint Conf. on Automated Reasoning, IJCAR 2001 Siena, Italy, 2001. (bibtex Eintrag)
• Martin Giese. A First-Order Simplification Rule with Constraints. Presented at the Int. Workshop on First-Order Theorem Proving, St. Andrews, Scotland, 2000. (bibtex Eintrag)
• 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 Eintrag)
• 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 Eintrag)

Interne Berichte

• 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.

Meine Diplomarbeit (erste überarbeitete Version vom 25.9.98) in Form von ca. 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)

Meine Studienarbeit (ca. 110kB gzip'ed PostScript).

• M. Giese. Partielle Monomorphie algebraischer Spezifikationen: Definition und Nachweis. Studienarbeit, Fakultät für Informatik, Universität Karlsruhe, 76128 Karlsruhe, Germany, 1996.

Berichte zu einigen Fallstudien die ich als wissenschaftliche Hilfskraft durchgeführt habe:

• 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.

Es gibt auch eine private Homepage!