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 9162, Ole Johan Dahls hus (Ifi2)

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 Semicolon project on semantic interoperability for institutions of the Norwegian public sector.

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.

Publications

Journal Articles

C.M. Hansen, R. Antonsen, M. Giese, A. Waaler. Incremental Variable Splitting. Journal of Symbolic Computation, appeared online 2011.

M. Giese, R.B. Bratvold. Probabilistic Modeling for Decision Support in Integrated Operations. SPE Economics & Management 3(3): 173–185. SPE-127761-PA. 2011. (bibtex entry)

W. Ahrendt, B. Beckert, M. Giese, P. Rümmer. Practical Aspects of Automated Deduction for Program Verification. Künstliche Intelligenz, 24(1):43–49, Springer 2010. (bibtex entry)

M. Giese. Superposition-based Equality Handling for Analytic Tableaux. Journal of Automated Reasoning, 38(1–3):127–153, April 2007. (bibtex entry).

W. Ahrendt, T. Baar, B. Beckert, R. Bubel, M. Giese, R. Hähnle, W. Menzel, W. Mostowski, A. Roth, S. Schlager, and P. H. Schmitt. The KeY Tool. Software and Systems Modeling 4(1), 2005.

B. Beckert, M. Giese, E. Habermalz, R. Hähnle, A. Roth, P. Rümmer, S. 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

M. Giese, J.I. Ornæs, L. Overå, I. Svensson, A. Waaler. Using Semantic Technology to Autogenerate Reports: Case Study of Daily Drilling Reports Proc. SPE Intelligent Energy Conference, Utrecht 2012, SPE 150225. To appear 2012.

M. Ivanovska, M. Giese. A Logic-based Approach to Decision Making. NIK 2011, Tromsø. (long version)

M. Ivanovska, M. Giese. Probabilistic Logic with Conditional Independence Formulae (short paper). European Conf. on Artificial Intelligence, ECAI 2010, Lisbon. (bibtex entry). Long Version.

M. Ivanovska, M. Giese. Probabilistic Logic with Conditional Independence Formulae. European Starting AI Researcher Symposium, STAIRS 2010, Lisbon. (bibtex entry)

M. Giese, R.B. Bratvold. Probabilistic Modeling for Decision Support in Integrated Operations. Proc. SPE Intelligent Energy Conference, Utrecht, 2010, SPE 127761. (bibtex entry)

M. Giese, B. Buchberger. 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)

M. Giese. Taclets and the KeY prover. ENTCS volume of UITP03 workshop. (bibtex entry)

M. Giese, R. Hähnle, D. Larsson. Rule-Based Simplification of OCL Constraints. UML2004 workshop on OCL and Model Driven Engineering, Lisbon. (bibtex entry)

M. Giese, R. Heldal. From Informal to Formal Specifications in UML. Proceedings of UML2004, Lisbon. (bibtex entry)

M. Giese. Taclets and the KeY Prover. Workshop on User Interfaces for Theorem Provers, UITP 2003. (bibtex entry)

M. Giese. Simplification Rules for Constrained Formula Tableaux. Proceedings of Tableaux 2003. (bibtex entry)

M. Giese, R. Hähnle. Tableaux + Constraints. Tableaux 2003 position paper. (bibtex entry)

M. Giese. A Model Generation Style Completeness Proof for Constraint Tableaux with Superposition. Proceedings of Tableaux 2002. (bibtex entry)

W. Ahrendt, T. Baar, B. Beckert, M. Giese, R. Hähnle, W. Menzel, W. Mostowski and P. H. Schmitt. The KeY System: Integrating Object-Oriented Design and Formal Methods. Proceedings of FASE at ETAPS 2002. (bibtex entry)

M. Giese. Incremental Closure of Free Variable Tableaux. Presented at the Intl. Joint Conf. on Automated Reasoning, IJCAR 2001 Siena, Italy, 2001. (bibtex entry)

W. Ahrendt, T. Baar, B. Beckert, M. Giese, E. Habermalz, R. Hähnle, W. Menzel, P. 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)

M. Giese. A First-Order Simplification Rule with Constraints. Presented at the Int. Workshop on First-Order Theorem Proving, St. Andrews, Scotland, 2000. (bibtex entry)

M. 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)

Book Chapters, Editions, Theses, and Tech Reports

M. Ivanovska, M. Giese. A Logic-based Approach to Decision Making. Research Report 441, Dept. of Informatics, University of Oslo, Norway. (bibtex)

M. Giese, A. Waaler, eds. Automated Reasoning with Analytic Tableaux and Related Methods. Special issue of Logical Methods in Computer Science. 2011.

M. Giese, A. Ireland, L. Kovacs, eds. Invariant Generation. Special issue of Journal of Symbolic Computation, Vol. 5, Issue 11, November 2010.

M. Giese, A. 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)

M. Giese, B. Buchberger. Towards Practical Reflection for Formal Mathematics, extended abstract. In Proceedings of Austria-Japan Workshop on Symbolic Computation and Software Verification, RISC Report 07-09.

M. Giese, T. Jebelean, eds. Proceedings of WING 2007, Workshop on Invariant Generation, Hagenberg, Austria. RISC Report 07-07. (bibtex entry)

M. 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)

W. Ahrendt, T. Baar, B. Beckert, R. Bubel, M. Giese, R. Hähnle, W. Menzel, W. Mostowski, A. Roth, S. Schlager, and P. 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)

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

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, 2001.

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

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.

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.

The Homepage of Martin Giese