Intelligente Werkzeuge zur Erhebung, Bereitstellung, Analyse und
Kommunikation von diversifiziertem, personifiziertem,
interoperablen semantischen Wissen, Deutsches Institut für
Wirtschaftsforschung, Berlin, Germany, 2011.
Der Automatische Theorembeweiser LEO-II, BMW Group, Munich,
Germany, 2011.
Mechanisierung und Automatisierung von Kombinationen klassischer
und nichtklassischer Logiken in klassischer Logik höherer
Stufe, University of Hamburg, Germany, 2011.
Mechanization and Automation of Combinations of Classical and
Non-Classical Logics in Classical Higher Order Logics, Colloquium
New Trends in Computational Logic, TU Dresden, Germany, 2011.
Three presentations at Dagstuhl Seminar 10412 QSTRLib: A Benchmark
Problem Repository for Qualitative Spatial and Temporal Reasoning,
Dagstuhl, Germany, October 10-13, 2010: Reasoning within and about
Combinations of Logics in Simple Type Theory (talk and system
demonstration), Participant Introduction, and QSTRLib Use Case:
Educational Question Answering on Spatial Configurations of
Countries, States, and Cities.
Adaptive Assertion-Level Proofs, The
IJCAR 2010 Workshop on Evaluation Methods for Solvers and Quality
Metrics for Solutions, Edinburgh, UK, July 20, 2010.
Automating Access Control Logics and Multimodal Logics in the
Automatic Higher-Order Theorem Prover LEO-II, Kestrel Institute,
Palo Alto, USA, October 29th, 2008.
LEO-II – A Cooperative Automatic Theorem Prover for
Classical Higher-Order Logic, Microsoft Research, Redmond, USA,
October 2nd, 2008.
Three Approaches for Guiding the Cooperation
of Mathematical Reasoning Systems: Proof
Planning, Agent-based Reasoning, and Autometad Composition of
Reasoning Web Services, QSL Theme
day: Integration of deductive tools. Nancy, France, February 2005.
From Natural Deduction to Sequent
Calculus and back, CALCULEMUS Autumn School 2002, Pisa,
Italy, September 2002.
Tutorial Dialog with a Mathematical
Assistant System, Computer Science Department, The
University of Birmingham, England, July 2002.
Agent-oriented Reasoning with
O-ANTS, Pure and Applied
Logic Seminar, Carnegie Mellon University, Pittsburgh, PA, USA,
November 2001.
Agent-oriented Reasoning with
O-ANTS, Department of Computer Science, Cornell
University, Ithaca, NY, USA, November 2001.
Panel member of the IJCAR 2001 Workshop Future
Directions in Automated Reasoning – Problems and Ideas for a
New Millennium, Siena, Italy, June 2001.
An Agent-based Approach to
Reasoning, Invited talk at the AISB'01 Convention
Agents & Cognition in conjunction with 8th Workshop on
Automated Reasoning: Bridging the Gap between Theory and Practice,
University of York, England, March 2001.
Concurrent Resource Guided
Deduction, Theoretical Computer Science Seminar, School of
Computer Science, The University of Birmingham, Birmingham,
England, January 2001.
Resource Guided Concurrent Deduction
with O-ANTS, Department of
Artificial Intelligence, The University of Edinburgh, Edinburgh,
Scotland, September 2000.
OMEGA, MATHWEB & Friends,
Department of Artificial Intelligence, The University of
Edinburgh, Edinburgh, Scotland, August 2000.
Towards Agent based Theorem Proving and
Proof Planning in OMEGA, Department of Computer Science,
The University of York, York, England, April 2000.
OANTS – An Open Approach at
Combining Interactive and Automated Theorem
Proving, Centre for Agent Research
and Development CARD, Department of Computer Science, Manchester
Metropolitan University, Manchester, England, March 2000.
A two layered Agent Approach for Guiding
Interactive Proofs, Theoretical Computer Science Seminar,
School of Computer Science, The University of Birmingham,
England, January 1999.
Extensional Higher Order Resolution,
Paramodulation and RUE-Resolution, Theoretical Computer
Science Seminar, School of Computer Science, The University of
Birmingham, England, January 1999.
Complete list of Talks
2012
LEO-II –- Eine universelle Logikmaschine, Beuth Hochschule
für Technik, Berlin, Germany, 2012.
Intelligente Werkzeuge zur Erhebung, Bereitstellung, Analyse und
Kommunikation von diversifiziertem, personifiziertem,
interoperablen semantischen Wissen, Deutsches Institut für
Wirtschaftsforschung, Berlin, Germany, 2011.
Der Automatische Theorembeweiser LEO-II, BMW Group, Munich,
Germany, 2011.
Mechanisierung und Automatisierung von Kombinationen klassischer
und nichtklassischer Logiken in klassischer Logik höherer
Stufe, University of Hamburg, Germany, 2011.
Mechanization and Automation of Combinations of Classical and
Non-Classical Logics in Classical Higher Order Logics, Colloquium
New Trends in Computational Logic, TU Dresden, Germany, 2011.
2010
Three presentations at Dagstuhl Seminar 10412 QSTRLib: A Benchmark
Problem Repository for Qualitative Spatial and Temporal Reasoning,
Dagstuhl, Germany, October 10-13, 2010: Reasoning within and about
Combinations of Logics in Simple Type Theory (talk and system
demonstration), Participant Introduction, and QSTRLib Use Case:
Educational Question Answering on Spatial Configurations of
Countries, States, and Cities.
Combining Logics in Simple Type Theory, 11th
International Workshop on Computational Logic in Multi-Agent
Systems (CLIMA XI), Lisbon, Portugal, August, 16th, 2010.
Adaptive Assertion-Level
Proofs, The IJCAR 2010 Workshop on Evaluation
Methods for Solvers and Quality Metrics for Solutions, Edinburgh,
UK, July 20, 2010.
Automating Quantified Multimodal Logics in HOL – My very
first Region Connection Calculus Prover, AAAI 2009 Spring
Symposia, Stanford, March 23-25, 2009.
Automating Access Control Logics and Multimodal Logics in the
Automatic Higher-Order Theorem Prover LEO-II, Kestrel Institute,
Palo Alto, USA, October 29th, 2008.
LEO-II - A Cooperative Automatic Theorem Prover for Classical
Higher-Order Logic, Microsoft Research, Redmond, USA, October 2nd,
2008.
LEO-II - A Cooperative Automatic Theorem Prover for Classical
Higher-Order Logic (System Description), The 4th International
Joint Conference on Automated Reasoning, (IJCAR'08), Sydney,
Australia, August 12-15, 2008.
THF0 - The Core TPTP Language for Classical Higher-Order Logic,
The 4th International Joint Conference on Automated Reasoning,
(IJCAR'08), Sydney, Australia, August 12-15, 2008.
LEO-II Demo, ESHOL Workshop at the 4th International Joint
Conference on Automated Reasoning (IJCAR'08), Sydney, Australia,
August 10, 2008.
Exploring Properties of Normal Multimodal Logics in Simple Type
Theory with LEO-II, Deduktionstreffen, Saarbrücken, Germany,
March 18, 2008.
Exploring Properties of Normal Multimodal Logics in Simple Type
Theory with LEO-II, Automated Reasoning Group Lunch Talk, The
University of Cambridge, England, 4 March 2008.
Some Results of the LEO-II Project, CIAO Workshop, TU Darmstadt,
20 February 2008.
2007
Effiziente Automatisierung von Logik höherer Stufe –
realisierbarer Traum oder ewiger Albtraum? Inaugural Lecture
(Privatdozent) at Saarland University, December 6, 2007.
Progress Report on LEO-II, an Automatic Theorem
Prover for Higher-Order Logic, TPHOLs, Kaiserslautern, Germany,
September 2007.
Progress Report on LEO-II: An Automatic Theorem
Prover for Higher-Order Logic, Automated Reasoning Group Lunch
Talk, The University of Cambridge, England, 3 July 2007.
The LEO-II Project, Automated Reasoning Workshop, London, England,
April 20, 2007.
The LEO-II Project, Deduktionstreffen, Koblenz, Germany, March 25,
2007.
The LEO-II Project, Omega-Ultra-Texmacs Mini Workshop,
Saarbrücken, Germany, March 22, 2007.
Challenges for Automated Theorem Proving in Classical Higher Order
Logics, The University of Edinburgh, Scotland, February 15, 2007.
Term Indexing for the LEO-II Prover, IWIL-6 workshop
at LPAR 2006: The 6th International Workshop on the Implementation
of Logics, Pnom Penh, Cambodia, November 2006.
Logik höherer Stufe: Ein geeignetes Fundament für die
Mathematik und für Formale Methoden?, Universität
Darmstadt, Germany, December 20th.
System Description: LEO – A Resolution based Higher-Order
Theorem Prover, LPAR-05 Workshop: Empirically Successfull
Automated Reasoning in Higher-Order Logic (ESHOL). Wexford Hotel,
Montego Bay, Jamaica, December 2nd.
Combining Proofs of Higher-Order and First-Order Automated Theorem
Provers, LPAR-05 Workshop: Empirically Successfull Automated
Reasoning in Higher-Order Logic (ESHOL). Wexford Hotel, Montego
Bay, Jamaica, December 2nd.
Three Approaches for Guiding the Cooperation
of Mathematical Reasoning Systems: Proof Planning, Agent-based
Reasoning, and Autometad Composition of Reasoning Web
Services, QSL
Theme day: Integration of deductive tools. Nancy, France, February
10th.
2004
OMEGA and
DIALOG, Workshop on Logic, Proofs, and
Programs, Saarbrücken, Germany, November 26th.
CALCULEMUS Quo Vadis?, Special Session at the IJCAR 2004 Workshop
on Computer-Supported Mathematical Theory Development together
with J. Siekmann, J. Calmet, and W. Windsteiger, Cork, Ireland,
July 5.
Agent-oriented Proof Planning, Evaluation of the Collaborative
Research Centre SFB378 Resource-adaptive Cognitive Processes,
Saarbrücken, Germany, June 8th.
Tutorial Dialogs on Mathematical Proofs,
IJCAI-03 Workshop on Knowledge Representation and Automated
Reasoning for E-Learning Systems, Acapulco, Mexico, August
10th.
Agent-oriented Reasoning with O-Ants, Cornell
University, Ithaca, NY, USA, 31th October.
Distributed Assertion Retrieval, First
International Workshop on Mathematical Knowledge Management
RISC-Linz, Schloss Hagenberg, Austria, 24th September.
A lost proof, TPHOLS 2001, Edinburgh, Scotland, 20th
August.
An Agent-oriented approach to reasoning, CALCULEMUS
Workshop 2001, Siena, Italy, June.
Agent-oriented theorem proving and proof planning in
OMEGA, C++ days of SFB 378 Resource adaptive cognitive processes,
Mertesdorf, July.
An Agent based Approach to Reasoning,
Invited talk at AISB'01 Convention Agents & Cognition and
Eighth Workshop on Automated Reasoning: Bridging the Gap between
Theory and Practice, University of York, England, 23th
March.
Agents in OMEGA, meeting in camera of the OMEGA group,
26th February.
Concurrent Resource Guided Deduction,
Theoretical Computer Science Seminar, School of Computer Science,
The University of Birmingham, January 12th.
2000
OMEGA – Ressourcenadaptives Beweisplanen,
meeting in camera of the Special Research Division SFB378, Schloss
Dagstuhl, November 17th.
Tutorielle Kommunikation für ein mathematisches
Assistenzsystem, meeting in camera of the Special Research
Division SFB378, Schloss Dagstuhl, November 17th.
Eine Übersicht zur AG Siekmann, joint talk with
Joerg Siekmann at the German Deduktionstreffen 2000, Saarland
University, Saarbrücken, October 6th.
Towards agent based proof planning, talk at the German
Deduktionstreffen 2000, Saarland University, Saarbrücken,
Oktober 6th.
Resource guided concurrent deduction with OANTS, talk
at the Department of Artificial Intelligence (DREAM-Group), The
University of Edinburgh, Edinburgh, September 13th.
OMEGA, MATHWEB, and Friends, talk at the Department of
Artificial Intelligence (DREAM-Group), The University of
Edinburgh, Edinburgh, August 28th.
Resource Guided Concurrent Deduction, short talk and
poster presentation at the CALCULEMUS Symposium 2000, St. Andrews,
August 7th.
Resource Guided Concurrent Deduction, short talk and
poster presentation at Automated Reasoning Workshop 2000, King's
College, London, England, July 21th.
Resource Guided Concurrent Deduction, poster
presentation at AISB'2000 Convention, Symposium on ‘How to
design a functioning mind', The University of Birmingham,
Birmingham, England, 17-20th April.
Towards Agent based Theorem Proving and Proof Planning
in OMEGA, Department of Computer Science, The University of York,
York, England, April 3th.
System demonstration: OMEGA, O-ANTS, and LEO,
Department of Computer Science, The University of York, York,
England, April 3th.
Poster Presentation (with V. Sorge): Agent based Proof
Planning, Sixth Workshop on Automated Reasoning: Bridging the Gap
between Theory and Practice; in conjunction with AISB'99
Convention, Edinburgh, Scotland, April.
A two layered Agent Approach for Guiding Interactive
Proofs, Theoretical Computer Science Seminar, School of Computer
Science, University of Birmingham, England, January 21th.
System Demonstration: OMEGA – a Mathematical
Assistant, Informatikforum '98 (Max-Planck-Institut für
Informatik, Deutsches Forschungszentrum für Künstliche
Intelligenz und Fachbereich Informatik der Uni d.Saarlandes)
Saarbrücken, Germany, October.
System Demonstration: OMEGA – a Mathematical
Assistant, Deduktionstreffen '98, Munich, Germany, October.
System Demonstration: OMEGA – a Mathematical
Assistant, 8th International Conference on Artificial
Intelligence: Methodology, Systems, Applications (AIMSA'98),
Sozopol, Bulgaria, September.
Constraint Solving in Logig Programming and Automated
Theorem Proving: a comparison, 8th International Conference on
Artificial Intelligence: Methodology, Systems, Applications
(AIMSA'98), Sozopol, Bulgaria, September.
System Demonstration: Integrating TPS with OMEGA,
Workshop Inference Mechanisms in Knowledge-Based Systems: Theory
and Applications, KI 98, Bremen, Germany, September.
Integrating TPS with OMEGA, Workshop Inference
Mechanisms in Knowledge-Based Systems: Theory and Applications, KI
'98, Bremen, Germany, September.
System Demonstration: LEO – A Higher-Order
Theorem Prover, The 15th International Conference on Automated
Deduction, Lindau, Germany, July 9th.
Exploiting past proof experience + Experiments in the
Automatic Selection of Problem-solving Strategies, SAG-WAS'98 der
AG Siekmann, Schlo&suml; Dagstuhl, Germany, May. (Original
work from Matthias Fuchs)
System Demonstration: OMEGA – A mathematical
Assistant, Evaluation of the SFB 378, Max-Planck Institute
für Informatik (MPI), Saarbrücken, April 28th.
Integrating TPS with OMEGA, Oberseminar AG Siekmann,
Universität des Saarlandes, Saarbrücken, Germany, March.
(With V. Sorge)
Model Existence for Higher-Order Logic, Oberseminar AG
Siekmann, Universität des Saarlandes, Saarbrücken,
Germany, January. (with M. Kohlhase)
1997
Extensionale Resolution höherer Stufe,
Forschungskolloquium der Studienstiftung des Deutschen Volkes,
Kochl am See, Germany, October.
Extensionale Resolution höherer Stufe,
Deduktionstreffen der GI, Schloss Dagstuhl, Germany,
September.
Embedding Extensionality in Higher-Order Resolution,
Oberseminar AG Siekmann, Universität des Saarlandes,
Saarbrücken, Germany, July.
Equalizing terms by Difference Reduction and
Abstraction, Automated theorem proving seminar, Department of
Mathematics, Carnegie Mellon Univerity, Pittsburgh, USA,
April.
LEO – Towards Higher-Order
Resolution, Automated Theorem Proving Seminar, Dep. of
Mathematics, Carnegie Mellon Univerity, Pittsburgh, USA,
February.
1996
Ein kategorieller Kalkül ebener und
rämlicher Netze, Sommerakademie der Studienstiftung des
Deutschen Volkes, St. Johann, Südtirol, Italy,
September.