Talks

2010

"Semantics-Based Change Impact Analysis for Heterogeneous Collections of Documents" at 19th Clam — Inka — OMRS Workshop (CIAO 2010), RISC, Schloss Hagenberg, Austria, 3-5 August 2010, 2010
"A Tactic Language for Declarative Proofs " at 19th Clam — Inka — OMRS Workshop (CIAO 2010), RISC, Schloss Hagenberg, Austria, 3-5 August 2010, 2010
"Proof Search Formalisms and Grammar Formalisms in OMEGA" at Workshop on Mathematically Intelligent Proof Search (MIPS 2010), CNAM, Paris, France, 2010
"Recent Developments in Omega's Proof Search Programming Language" at Programming Languages for Mechanized Mathematics Systems, CNAM, Paris, France, 2010
"Declarative Specification Tactics as a Lightweight-Formalism for Design Patterns for Formal Specifications" at 20th Workshop on Algebraic Development Techniques (WADT-2010), Schloss Etelseon, Langwedel, Germany, 1-4. July 2010, 2010

2008

(Invited)"Semantics-based Authoring Tools for Mathematical Documents" at Seminar on Formal Mathematics, Bonn, Germany, 31 October, 2008 (Slides)

2007

(Invited)"Das Beweisassistenzsystem OMEGA" at Ringvorlesung der Mathematik, Saarbruecken, Germany, 22 Juni, 2007 (Slides)
(Invited)"Integrating the Text-Editor TeXmacs and the Proof Assistance System OMEGA using PLATO" at LORIA, Nancy, France, 2007 (Slides)

2006

"Integrating the Text-Editor TeXmacs and the Proof Assistance System OMEGA using PLATO" at CHIT/CHAT 06 (Small Types Workshop), Nijmegen, Netherlands, 21-22 December, 2006 (Slides)
"PLATO: A Mediator between Text-Editors and Proof Assistance Systems" at 7th Workshop on User Interfaces for Theorem Provers (UITP'06), Seattle, WA, USA, 21st August, 2006 (Slides)
"The MathServe Framework for Semantic Reasoning Web Services" at 3rd International Joint Conference on Automated Reasoning (IJCAR'06), Seattle, WA, USA, 17-20 August , 2006 (Slides)
"A Formal Correspondence between OMDoc with Alternative Proofs and the LambdaBarMuMuTilde-Calculus" at 5th International Conference on Mathematical Knowledge Management (MKM 2006), Wokingham, UK, 11-12th August, 2006 (Slides)
(Invited)"The New Proof Assistant OMEGA: Developments and Applications " at CISA Seminar, University of Edinburgh, Edinburgh, 20th July, 2006 (Slides)
"The New Proof Assistant OMEGA: Developments and Applications " at Scottish Theorem Proving Meeting, University of Glasgow, Glasgow, June 6th, 2006 (Slides)
"Automated reasoning in large structured theories" at Workshop CIAO'06, Braunshausen, Germany, April 6-7, 2006 (Slides)
"Proof Development and Maintenance (after a brief survey of the new OMEGA System) " at SFB-378 ``C-Tag'', Saarbruecken, Germany, March 17, 2006 (Slides)

2005

"The Deep Inferential Aspects of the CORE Calculus" at ICCL Autumn Workshop - Deep Inference and Proof Theory, Dresden, Germany, December 14-15, 2005 (Slides)
"Architecture of the new OMEGA system + The CORE Calculus" at Theorema-Ultra-Omega'05, Saarland university, Saarbrücken, Germany, November 14-15, 2005 (Slides)
"On the Dynamic Increase of Multiplicities in Matrix Proof Methods for Classical Higher-Order Logic" at 3rd Nancy-Saarbrücken Workshop on Logic, Deduction, LORIA, Nancy, France, October 13-14, 2005 (Slides)
"On the Dynamic Increase of Multiplicities in Matrix Proof Methods for Classical Higher-Order Logic" at Tableaux 2005, Koblenz, Germany, September 14-17, 2005 (Slides)
"The CORE Calculus" at 20th International Conference on Automated Deduction, Tallinn, Estonia, July 22-27, 2005 (Slides)
" Generic Modular Data Structure for Proof Attempts Alternating on Ideas and Granularity" at Fourth International Conference on Mathematical Knowledge Management (MKM'05), International University Bremen, Germany, July 15-17, 2005 (Slides)
"Representing Proof-Planning in the Rho-Calculus" at Second Workshop on the Rho-Calculus, LIX-Ecole polytechnique, Palaiseau, France, May 30, 2005 (Slides)
"Integrating Proof Assistants as Reasoning and Verification Tools into a Scientific WYSIWIG Editor" at Workshop on User Interfaces for Theorem Provers (UITP 2005), Edinburgh, Scotland, April 9, 2005 (Slides)
"Formalising and Analysing Textbook Proofs: The Problem of Under-Specification and Granularity" at CIAO'05 Workshop, Nottingham, UK, April 4-6, 2005 (Slides)
(Invited)"Three Approaches for Guiding the Cooperation of Mathematical Reasoning Systems: Proof Planning, Agent-based Reasoning, and Automated Composition of Reasoning Web Services" at QSL day about Integration of deductive tools, LORIA, Nancy, France, February 10, 2005 (Slides)
"Organisation of Workshops between Nancy & Saarbrücken -- Experiences & Suggestions" at Kick-Off Meeting INTERREG Project III C ``Recherche sans Frontières/Forschen ohne Grenzen'', Saarland university, Saarbrücken, Germany, January 18, 2005 (Slides)

2004

"The CORE Calculus for Contextual Reasoning" at Theoretical Computer Science Seminars, LORIA, Nancy, France, February 9, 2004

2003

"Hierarchical Contextual Reasoning" at Doctoral Thesis Defense, Saarland university, Saarbrücken, Germany, December 19, 2003 (Slides)
(Invited)"Omega: From Proof-Planning towards Mathematical Knowledge Management" at Mathematical Knowledge Management Symposium, Heriott-Watt University, Edinburgh, Scotland, November 25-29, 2003 (Slides)
(Invited)"Formal Software Development in MAYA" at , Labri, Univ. Bordeaux, France, November 13, 2003 (Slides)
"Disproving False Conjectures" at LPAR 2003, Almaty, Kasachstan, September 22-26, 2003 (Slides)
(Invited)"Towards Distributed Mathematical Knowledge Management using MAYA" at MOWGLI-Project Meeting, INRIA, Sophia-Antipolis, France, September 15, 2003 (Slides)
"Hierarchical Contextual Reasoning" at Workshop Theorema-Omega'03, RISC, Hagenberg Castle, Austria, May 24-26, 2003 (Slides)
"Management of Change in MAYA" at Workshop ``Mathematics on the Semantic Web'', Eindhoven, The Netherlands, May 12-14, 2003 (Slides)

2002

"Maintenance of formal Software Development by Stratified Verification" at LPAR 2002, Tbilissi, Georgia, Ocotober 14-18, 2002 (Slides)
"Integrating HOL-CASL into the development graph manager MAYA" at FROCOS 2002, Santa Margherita Ligure, Italy, April, 2002 (Slides)
"Intuitive & Contextual Reasoning or Towards supporting theorem proving on the assertion level" at CIAO 2002, Edinburgh, Scotland, April, 2002 (Slides)

2001

"Intuitive & Contextual Reasoning" at AG Siekmann internal group seminar, Saarland university, Saarbrücken, Germany, December, 2001 (Slides)
"The INKA Development Graph: Bridging the gap between Specifications and Theorem provers" at Deduktionstreffen'01, Karlsruhe, Germany, 2001 (Slides)
"A Proof Planning Framework with explicit Abstractions based on Indexed Formulas" at 4th workshop on strategies in automated deduction (STRATEGIES'01), Siena, Italy, June, 2001 (Slides)
"A Proof Planning Framework with explicit Abstractions based on Indexed Formulas" at CIAO 2001, Genova, Italy, 2001 (Slides)

2000

"Towards a Reasoning Framework" at Theoretical Computer Science Seminar, University of Birmingham, England, November, 2000 (Slides)
"Supporting Evolutionary Formal Software Development" at CIAO 2000, Dagstuhl, Germany, 2000 (Slides)
"The CASL - INKA Interface" at CoFI-tools group meeting at ETAPS 2000, Berlin, Germany, April, 2000 (Slides)

1999

"INKA 5.0" at CIAO 1999, Edinburgh, Scottland, 1999 (Slides)

1998

"Clark Glymour 'Artificial Intelligence is Philosophy' in J.H. Fetzer: Aspects of AI, 1998" at AGS Group Seminar "Philosophical Foundations of AI", Dagstuhl, Germany, 1998
"Different talks about selected topics in Machine Learning" at AGS Group Seminar "Machine Learning", Dagstuhl, Germany, 1998
"Logic as a General Framework for Planning" at Workshop ClamInka 1998, Edinburgh, Scotland, 1998

1997

"Decision Theory" at AGS Group Seminar about "Decision Theory", Dagstuhl, Germany, 1997 (Slides)
"Using Abstractions to Equalize Terms" at Workshop ClamInka 1997, Genova, Italy, 1997 (Slides)

1996

"Using Abstractions to Equalize Terms" at Workshop ClamInka 1996, Edinburgh, Scotland, 1996 (Slides)