The Homepage of Martin Giese
Who am I?
I work as an associate professor in the
LogID
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 as Assistant Scientific Director of the FP7
EU project Optique which
aims to apply ontology-base data access (OBDA) techniques to real-life
industrial data access challenges.
In 2013, I am giving for the fourth time the
course INF3580
– Semantic Technologies. See here for
previous teaching activities.
In 2009 I organized TABLEAUX 2009, the
International Conference on Automated Reasoning with Analytic Tableaux
and Related Methods in Oslo, together with Arild Waaler.
Since 2010, I am an elected member of the Tableaux Steering Committee
Since May 2008, I am editor of the Newsletter of
the Association for Automated
Reasoning, and since December 2010, I am secretary of AAR and CADE
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 pgf-blur, pst-blur
and pst-slpe
LaTeX packages, which add some fancy features to
PGF/TikZ, resp.
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.
Publications
Journal Articles
- C.M. Hansen, R. Antonsen, M. Giese, A. Waaler.
Incremental
Variable Splitting. Journal of Symbolic Computation,
47(9): 1046–1065, Springer 2012.
(bibtex entry)
- 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
- D. Calvanese, M. Giese, P. Haase, I. Horrocks, T. Hubauer, Y. Ioannidis, E. Jiménez-Ruiz, E. Kharlamov, H. Kllapi, J. Klüwer, M. Koubarakis, S. Lamparter, R. Möller, C. Neuenstadt, T. Nordtveit, Ö. Özcep, R. M. driguez Muro, M. Roshchin, M. Ruzzi, F. Savo, M. Schmidt, A. Soylu, A. Waaler, and D. Zheleznyakov, "Optique: OBDA Solution for Big Data," in Poster track of the Extended Semantic Web Conference, 2013.
- B. Cuenca Grau, M. Giese, I. Horrocks, T. Hubauer, E. Jiménez-Ruiz, E. Kharlamov, M. Schmidt, A. Soylu, and D. Zheleznyakov, "Towards Query Formulation and Query-Driven Ontology Extensions in OBDA," in OWL Experiences and Directions Workshop (OWLED), 2013.
- D. Calvanese, M. Giese, P. Haase, I. Horrocks, T. Hubauer, Y. Ioannidis, E. Jiménez-Ruiz, E. Kharlamov, H. Kllapi, J. Klüwer, M. Koubarakis, S. Lamparter, R. Möller, C. Neuenstadt, T. Nordtveit, Ö. Özcep, R. M. driguez Muro, M. Roshchin, M. Ruzzi, F. Savo, M. Schmidt, A. Soylu, A. Waaler, and D. Zheleznyakov, "The Optique Project: Towards OBDA Systems for Industry (Short Paper)," in OWL Experiences and Directions Workshop (OWLED), 2013.
- D. Hovland, M. Giese, B. Holen. Efficient Rule-Matching for
Automated Coherent Logic. NIK 2012, Bodø.
- M. Ivanovska, M. Giese. A
Probabilistic Logic for Sequences of Decisions. LOFT 2012,
Conf. on Logic and the Foundations of Game and Decision Theory.
- B. Holen, D. Hovland, M. Giese. Efficient Rule-Matching for
Hyper-Tableaux. Intl. Workshop on the Implementation of
Logics, IWIL 2012, Merida, Venezuela, 2012.
- 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.
- 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. Giese, D. Calvanese, I. Horrocks, Y. Ioannidis, H. Klappi, M. Koubarakis, M. Lenzerini, R. Möller, Ö. Özçep, M. Rodriguez Muro, R. Rosati, R. Schlatte, P. Haase, M. Schmidt, A. Soylu, A. Waaler. Scalable End-user Access to Big Data. Chapter in Rajendra Akerkar, ed., Big Data Computing, CRC Press, to appear 2013.
- 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.
[Extract RDFa!]
