The Homepage of Martin Giese

Who am I?

I work as a post-doc researcher in the OMS Group at the Department of Informatics of the University of Oslo, Norway.

Address

Martin Giese
Institutt for informatikk
Postboks 1080 Blindern
N-0316 Oslo
Norway

Office: room 3302, Informatikkbygningen

Email: martingi (at) ifi (dot) uio (dot) no
Tel: +47-22852737
Fax: +47-22852401
Mobile: +47-41383148

Current Work

I am currently working for the CODIO project on collaborative decision making for integrated operations. In particular, I'm investigating how probabilistic logics may be used to achieve a tight integration between Bayesian decision networks and ontologies based on description logics.

In Spring 2008, I am teaching a course on logic. See here for previous teaching activities.

In 2009 I will organize TABLEAUX 2009, the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods in Oslo, together with Arild Waaler.

Since May 2008, I am editor of the Newsletter of the Association for Automated Reasoning.

Other topics I am interested in include:

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

These are also the main topics of my PhD thesis, which I finished in 2002 at Karlsruhe University. I wrote an automated theorem prover called PrInS, about which you can read more here.

I am also the author of the pst-blur and pst-slpe LaTeX packages, which add some fancy features to PSTricks, and of the Java Pretty Printer Library (jpplib), which helps in printing structured data using indentation.

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

Paper

Journal Articles

• Martin Giese. Superposition-based Equality Handling for Analytic Tableaux. Journal of Automated Reasoning, 38(1-3):127-153, April 2007. (bibtex entry).
• Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Richard Bubel, Martin Giese, Reiner Hähnle, Wolfram Menzel, Wojciech Mostowski, Andreas Roth, Steffen Schlager, and Peter H. Schmitt. The KeY Tool. Software and Systems Modeling 4(1), 2005.
• Bernhard Beckert, Martin Giese, Elmar Habermalz, Reiner Hähnle, Andreas Roth, Philipp Rümmer, Steffen Schlager. Taclets: a new paradigm for writing theorem provers. Revista De La Real Academia De Ciencias Exactas, Físicas Y Naturales, Serie A: Matemáticas, 98 (1),2004. (bibtex entry)

Conference and Workshop papers

• Martin Giese. Towards Practical Reflection for Formal Mathematics. In work-in-progress proceedings of Calculemus/MKM 2007, RISC Report 07-06. (bibtex entry)
• B. Beckert, M. Giese, R. Hähnle, V. Klebanov, P. Rümmer, S. Schlager, P. H. Schmitt. The KeY System 1.0 (Deduction Component). System abstract in Proceedings of CADE-21, Bremen. (bibtex entry)
• M. Giese. Saturation up to Redundancy for Tableau and Sequent Calculi. Proceedings of LPAR06, Phnom Penh. (bibtex entry)
• M. Giese. A Calculus for Type Predicates and Type Coercion. Proceedings of Tableaux 2005, Koblenz. (bibtex entry)
• M. Giese, D. Larsson. Simplifying Transformations of OCL Constraints. Proceedings of Models 2005, Montego Bay. (bibtex entry)
• Martin Giese. Taclets and the KeY prover. ENTCS volume of UITP03 workshop. (bibtex entry)
• Martin Giese, Reiner Hähnle, Daniel Larsson. Rule-Based Simplification of OCL Constraints. UML2004 workshop on OCL and Model Driven Engineering, Lisbon. (bibtex entry)
• Martin Giese, Rogardt Heldal. From Informal to Formal Specifications in UML. Proceedings of UML2004, Lisbon. (bibtex entry)
• Martin Giese. Taclets and the KeY Prover. Workshop on User Interfaces for Theorem Provers, UITP 2003. (bibtex entry)
• Martin Giese. Simplification Rules for Constrained Formula Tableaux. Proceedings of Tableaux 2003. (bibtex entry)
• Martin Giese, Reiner Hähnle. Tableaux + Constraints. Tableaux 2003 position paper. (bibtex entry)
• Martin Giese. A Model Generation Style Completeness Proof for Constraint Tableaux with Superposition. Proceedings of Tableaux 2002. (bibtex entry)
• 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. (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)
• Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Martin Giese, Elmar Habermalz, Reiner Hähnle, Wolfram Menzel, Peter H. Schmitt. The KeY Approach: Integrating Object Oriented Design and Formal Verification. Proceedings, 8th European Workshop on Logics in AI (JELIA), Malaga, Spain, September 2000. (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)
• Martin Giese and Wolfgang 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)

Book Chapters, Editions, Theses, and Tech Reports

• Martin Giese, Arild Waaler, eds. Proceedings of the 18th Intl. Conf. on Automated Reasoning with Analytic Tableaux and Related Methods, Oslo, Norway, July 6-10, 2009. (bibtex entry)
• Martin Giese. Towards Practical Reflection for Formal Mathematics, extended abstract. In Proceedings of Austria-Japan Workshop on Symbolic Computation and Software Verification, RISC Report 07-09.
• Martin Giese, Tudor Jebelean, eds. Proceedings of WING 2007, Workshop on Invariant Generation, Hagenberg, Austria. RISC Report 07-07. (bibtex entry)
• Martin Giese. First-order logic. Chapter in B. Beckert, R. Hähnle, and P. H. Schmitt, Verification of Object-Oriented Software: The KeY Approach. Springer, 2007. (bibtex entry)
• Wolfgang Ahrendt, Thomas Baar, Bernhard Beckert, Richard Bubel, Martin Giese, Reiner Hähnle, Wolfram Menzel, Wojciech Mostowski, Andreas Roth, Steffen Schlager, and Peter H. Schmitt. The KeY Tool. Department of Computing Science, Chalmers University and Göteborg University, Technical Report in Computing Science No. 2003-5, February 2003.(bibtex Entry)
• Martin Giese. Proof Search Without Backtracking for Free Variable Tableaux. PhD thesis. Fakultät für Informatik, Universität Karlruhe, July 2002. (bibtex entry). This thesis is published electronically.
• Martin 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, 2001.
• Martin Giese. Integriertes automatisches und interaktives Beweisen: Die Kalkülebene. Diplomarbeit, Fakultät für Informatik, Universität Karlsruhe, 76128 Karlsruhe, Germany, 1998. (bibtex Entry)
• Martin Giese, David Kempe and Arno 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.
• Martin Giese. Partielle Monomorphie algebraischer Spezifikationen: Definition und Nachweis. Studienarbeit, Fakultät für Informatik, Universität Karlsruhe, 76128 Karlsruhe, Germany, 1996.
• Martin Giese and Arno 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.