Year: .*

2019 | |

[266] | (Invited) On Universal Logical Reasoning and Gödel's Ontological Argument, CISA (Center for Intelligent Systems and their Applications), Edinburgh University School of Informatics, 2019. (Forthcoming) |

[265] | (Invited) Ethisch Intelligente Systeme, DLR Symposium ``Künstliche Intelligenz'': Made in Germany, 2019. (Event Website) |

[264] | Ethisch Intelligente Systeme, Tag der offenen Tür, Dahlem Center for Machine Learning and Robotics, FU Berlin, 2019. (Press) |

[263] | KI und Robotik an der FU Berlin, Kids Presentation for Kronach-Grundschule, 2019. |

[262] | (Invited) Higher-order automated theorem proving --- Why has there been such a resistance?, ANDREI-60: Automating New-era Deductive Reasoning Event In Iberia, 2019. |

[261] | (Invited Featured Scientist) Der Beweis, 71. Science Slam Berlin, SO36 Berlin Kreuzberg, 2019. (YouTube) |

[260] | (Invited Keynote) Computational Metaphysics: New Insights on Gödel's Ontological Argument and Modal Collapse, Formal Methods and Science in Philosophy III, 2019. |

[259] | (Invited Panelist), Panel Discussion on "Laws in LAWS", scientific involvement in the effort to ban LAWS, organised by Future of Life Institute http://futureoflife.org, with Ariel Conn (FLI) and Kate Folb (Hollywood), Konferenzzentrum der Heinrich-Böll-Stiftung, Berlin, 2019. |

[258] | (Invited Panelist), Panel Discussion on "Artificial Intelligence", organised by Nature Research (Springer Nature), with Dean Sanderson (Springer Nature), Oliver Brock (TU Berlin), Dagmar Monett (HWR Berlin), Raul Rojas (FU Berlin), Henry Ford Bau, FU Berlin, 2019. (event flyer) |

[257] | What Kind of Ultrafilter is Gödel's God, Kurt Gödel: Philosophical Views, Workshop at FU Berlin http://christoph-benzmueller.de/2019-Goedel/, 2019. |

2018 | |

[256] | (Invited) Studies in Computational Metaphysics and Computational (Pseudo-)Ethics, Colloquium Cognitive Systems University of Ulm, 2018. (slides) |

[255] | (Invited Keynote) Can computers help to sharpen our understanding of ontological arguments?, 12th All India Students' Conference on Science and Spiritual Quest (AISSQ), IIT Bhubaneswar, India, 2018. (slides, video) |

[254] | (Invited; celebration of Martin Davis' 90th Birthday) A Deontic Logic Reasoning Infrastructure, Special Session on the History and Philosophy of Computing (HaPoC) at the Computability in Europe (CiE) conference, 2018. |

[253] | (Invited Keynote) Experiments in Universal Logical Reasoning --- How to utilise ATPs and SMT solvers for the exploration of axiom systems for category theory in free logic?, 16th International Workshop on Satisfiability Modulo Theories (SMT 2018), Oxford, UK, 2018. |

[252] | (Invited Keynote) A Flexible Infrastructure for Normative Reasoning, 14th International Conference, DEON 2018, Utrecht, The Netherlands, 3-6 July, 2018, 2018. (video) [doi] |

[251] | (Invited) Experiments in Universal Logical Reasoning --- How to utilise ATPs and SMT solvers for the exploration of axiom systems for category theory in free logic?, Institut für Theoretische Informatik, LMU München, 2018. |

[250] | Computational Hermeneutics: Using Computers to Interpret Arguments, Second Chinese Conference on Logic and Argumentation (CLAR 2018), Hangzhou, China, 2018. |

[249] | Some Reflections on a Computer-aided Theory Exploration Study in Category Theory, 3rd Conference on Artificial Intelligence and Theorem Proving (AITP 2018), Aussois, France, 2018. (slides, video) |

[248] | (Invited Lecture) From Computational Metaphysics towards Computational (Pseudo-)\-Ethics, Bath IMI Thematic Semester: Algorithms, Accountability and Ethics in Machine Learning, U Bath, UK, 2018. |

2017 | |

[247] | (Invited Tutorial) Automated Reasoning in Higher-order and Non-classical Logics, Pontifícia Universidade Católica do Rio Grande do Sul (PUCRS), Porto Alegre, Brasil, 2017. (zip-file) |

[246] | (Invited) What has the Mechanisation of Category Theory in Common with Proving God’s Existence?, Pontifícia Universidade Católica do Rio Grande do Sul (PUCRS), 40 Years of Computer Science, 2017. |

[245] | (Invited Keynote) Recent Successes with a Meta-Logical Approach to Universal Logical Reasoning, XX Brazilian Symposium on Formal Methods (SMBF), Recife, Brazil, 2017. (slides) |

[244] | (Invited Keynote) What has the Mechanisation of Category Theory in Common with Proving God’s Existence?, 3. BMG Tag, Berliner Mathematische Gesellschaft e.V., Berlin, 2017. (November) |

[243] | Automating Emendations of the Ontological Argument in Intensional Higher-Order Modal Logic, KI 2017 - 40th German Conference on Artificial Intelligence, 25-29 September 2017 in Dortmund, Germany, 2017. |

[242] | (Invited) Automating Free Logic in HOL, with an Experimental Application in Category Theory, Dagstuhl Seminar 17371: Deduction Beyond First-Order Logic, Dagstuhl, 2017. |

[241] | (Invited Tutorial) Universal Logical Reasoning via Semantical Embeddings in HOL, 2nd CLE Colloquium for Philosophy and History of Formal Sciences (CLE4Science), University of Campinas, Brasil, 2017. (zip-file) |

[240] | (Invited Keynote) Computational Metaphysics: The Virtues of Formal Proofs Beyond Math, 2nd CLE Colloquium for Philosophy and History of Formal Sciences (CLE4Science), University of Campinas, Brasil, 2017. |

[239] | Universal Logic Theorem Proving via Semantical Embeddings in HOL, International Workshop on Logic-Based Formalisms for Legal Reasoning (LBFLR 2017), 2017. (May) |

[238] | (Invited Tutorial) Tutorial on Universal Logic Theorem Proving in HOL, ILIAS group, University of Luxembourg, 2017. (May) |

[237] | (Invited) Computational Metaphysics: The Virtues of Formal Computer Proofs Beyond Maths and Computer Science, S-2: The Ubiquity of Computing: historical and philosophical issues---Commission for Computing HaPoC--- 25th International Congress of History of Science and Technology, Rio de Janeiro, Brasil, 2017. |

[236] | Innovative Teaching of Computational Metaphysics, Session on Innovative & Effective Teaching in History of Science and Technology, 25th International Congress of History of Science and Technology, Rio de Janeiro, Brasil, 2017. |

[235] | (Invited Public Presentation) Calculemus!: Analyse von Kurt Gödel's Gottesbeweis mit dem Computer, URANIA, Berlin, 2017. (June) |

[234] | Davis-Putnam-Logemann-Loveland Algrithmus, Alpen-Adria Universität Klagenfurt, 2017. (April) |

[233] | (Invited) Calculemus! --- Progress in Universal Logic Reasoning and Computational Metaphysics, Alpen-Adria Universität Klagenfurt, 2017. (April) |

[232] | (Invited) Universal Logic Reasoning via Shallow Semantical Embeddings, Workshop on Rational Enterprise Architecture Logic and Reasoning (REAL), University of Luxembourg, 2017. (April) |

[231] | (Invited) Computational Metaphysics: The Virtues of Formal Proofs Beyond Math, ILIAS Distinguished Lectures, University of Luxembourg, 2017. (March) |

[230] | (Invited) Künstliche Intelligenz---Bemerkungen zur Historie und zu aktuellen Entwicklungen, Innovationsregion Lausitz GmbH, Cottbus, 2017. (poster) |

[229] | (Invited) System Demonstration: Interactive and Automated Reasoning in Isabelle/HOL, Workshop: Bettermarks und Mathematische Beweise, bettermarks GmbH, Berlin, 2017. (January) |

2016 | |

[228] | (Invited) Uniform Proofs via Shallow Semantic Embeddings?, Dagstuhl Seminar 15381 --- Universality of Proofs, Dagstuhl, 2016. (slides) |

[227] | Tutorial on Reasoning in Expressive Non-Classical Logics with Isabelle/HOL, Second Global Conference on Artificial Intelligence (GCAI), Berlin, 2016. (course material) |

[226] | An Object-Logic Explanation for the Inconsistency in Gödel's OntologicalTheory, KI 2016 - 39th German Conference on Artificial Intelligence, 26-30 September 2016 in Klagenfurt, Austria, 2016. (slides) |

[225] | Axiomatising Category Theory in Isabelle/HOL, Deduktionstreffen, 26 September 2016 in Klagenfurt, Austria, 2016. (slides) |

[224] | Einsatz von Theorembeweisern in der Lehre, Hochschuldidaktik der Informatik: 7. Fachtagung des GI-Fachbereichs Informatik und Ausbildung/Didaktik der Informatik; 13.-14. September 2016 an der Universität Potsdam, 2016. (slides) |

[223] | (Invited) Computational Metaphysics: The Virtues of Formal Proofs Beyond Maths, Colloquium of the Berlin Mathematical School (BMS Fridays), Berlin, 2016. (slides (without movies)) |

[222] | The OEB Plenary Debate 2016, The global, cross-sector conference and exhibition on technology supported learning and training (OEB), 2016. (panelists,youtube) |

[221] | An Object-Logic Explanation for the Inconsistency in Gödel’s Ontological Theory, 39th German Conference on Artificial Intelligence (KI), 2016. (September) |

[220] | Axiomatizing Category Theory in Free Logic, Deduktionstreffen 2016, 2016. (September) |

[219] | (Poster) The Inconsistency in Gödel's Ontological Argument: A Success Story for AI in Metaphysics, Intl. Congress on Mathematical Software (ICMS 2016), 2016. (poster) |

[218] | Automating Free Logic in Isabelle/HOL, Intl. Congress on Mathematical Software (ICMS 2016), 2016. (slides, Isabelle/HOL_paper_source, Isabelle/HOL_further_experiments) |

[217] | (Invited Panel) Erwachen der Roboter – lernende Maschinen und die Intelligenz der Zukunft, Bundeszentrale für politische Bildung – bpb, Berlin, 2016. |

[216] | Hands-on Higher-order Modal Logics in Isabelle/HOL, UITP 2016, Coimbra, Portugal, 2016. |

[215] | TPTP and Beyond: Representation of Quantified Non-Classical Logics, ARQNL 2016, Coimbra, Portugal, 2016. |

[214] | (Invited) Automatisierung von Gödel's Gottesbeweis im Computer, Auticon GmbH, Berlin, 2016. (June) |

[213] | (Invited Keynote) Künstliche Intelligenz---Wohin geht die Reise?, Shared Services and Outsourcing Woche (http://www.sharedserviceswoche.de/mediacenter), Berlin, 2016. (slides (without movies)) |

[212] | (Invited) Computational Metaphysics, Central Teaching Award Acceptance Speech at FU Berlin, 2016. (slides (without movies)) |

[211] | (Invited Lecture Course) Computational Metaphysics, Thematic trimester 'Current Issues in the Philosophy of Practice of Mathematics and Informatics', Centre International de Mathématiques et d'Informatique de Toulouse (CIMI), France, 2016. (June) |

[210] | (Invited) The Inconsistency in Gödel’s Ontological Argument: An Application of Mathematical Proof Assistants in Metaphysics, Mathematical Logic Seminar, Stanford University, USA, 2016. (slides) |

[209] | (Invited Tutorial) A Universal Logic Theorem Proving Approach, Berkeley-Stanford Circle in Logic and Philosophy, San Francisco, USA, 2016. (February) |

[208] | (Invited) A Success Story of Higher-Order Theorem Proving in Computational Metaphysics, Logic Colloquium, University of California, Berkeley, USA, 2016. (February) |

2015 | |

[207] | (Invited) Experiments in Computational Metaphysics, SRI International, Menlo Park, USA, 2015. (December) |

[206] | (Invited Lecture Course) Higher-Order Modal Logics, Logic Summer School, ANU Canberra, Australia, 2015. (slides) |

[205] | (Invited Keynote) Experiments in Computational Metaphysics, 9th All India Students' Conference on Science and Spiritual Quest (AISSQ), IIT Kharagpur, India, 2015. (slides) |

[204] | (Invited) Experiments in Computational Metaphysics, Computational Logic Seminar (MUGS), Stanford University, USA, 2015. (October) |

[203] | (Invited) Higher-Order Proofs and Models -- Examples from Meta-Logical Reasoning and Metaphysics, Dagstuhl Seminar 15381 --- Deduction: Models and Proofs, 2015. (October) |

[202] | (Invited Keynote) On a (Quite) Universal Theorem Proving Approach and its Application to Metaphysics, Tableaux 2015, Wroclaw, Poland, 2015. (slides) |

[201] | (Invited Lecture Course) Higher-Order Modal Logics: Automation and Applications, The 11th Reasoning Web Summer School, 2015. (slides) |

[200] | (Invited) ''Gottesbeweis'' reloaded --- Analyzing Variants of the Ontological Argument with the Computer, Lange Nacht der Wissenschaften, Berlin, Germany, 2015. (slides) |

[199] | Einführung in die Komplexitätsklassen P und NP, Universität Leipzig, 2015. |

[198] | (Invited) Towards Computational Metaphysics, Universität Leipzig, 2015. |

[197] | (Invited Keynote) Gödel's Ontological Argument Revisited -- Findings from a Computer-supported Analysis, 1st World Congress on Logic and Religion, João Pessoa, Brazil, 2015. (slides) |

[196] | (Invited) Towards Computational Metaphysics --- Bridging between Mathematical Logic, Artificial Intelligence and Philosophy, Berlin Mathematical School, lecture series on 'Bridges between mathematics and its applications', Technical University Berlin, Germany, 2015. |

[195] | Der ABox-Vervollständigungsalgorithmus für ALC, Friedrich-Alexander-Universität, Erlangen-Nürnberg, Germany, 2015. |

[194] | (Invited) Towards Computational Metaphysics --- Techniques and Tools for Knowledge Representation and Reasoning in Expressive Ontologies, Friedrich-Alexander-Universität, Erlangen-Nürnberg, Germany, 2015. |

2014 | |

[193] | (Invited Keynote) On Logic Embeddings and Gödel's God, 21. Jahrestagung der GI-Fachgruppe `Logik in der Informatik', University of Kassel, Germany, 2014. (slides) |

[192] | (Invited Keynote) On Logic Embeddings and Gödel's God, 22nd International Workshop on Algebraic Development Techniques, Sinaia, Romania, 2014. (slides) |

[191] | Automating Gödel's Ontological Proof of God's Existence with Higher-order Automated Theorem Provers, 21st European Conference on Artificial Intelligence (ECAI), Prague, Czech Republic, 2014. (slides) |

[190] | HOL based First-order Modal Logic Provers, ARQNL Workshop at VSL'2014, Vienna, Austria, 2014. (slides) |

[189] | (Invited Tutorial) Higher-Order Automated Theorem Provers, APPA Workshop at VSL'2014, Vienna, Austria, 2014. (slides) |

[188] | Gödel's Unvollständigkeitssätze, Freie Universität Berlin, Germany, 2014. (slides) |

[187] | (Invited) Kurt Gödel's Gottesbeweis auf dem Computer, Fromme Professoren Marburg, Germany, 2014. (slides) |

[186] | (Invited) Gödel's God on the Computer, IT University Copenhagen, Denmark, 2014. |

[185] | (Invited) Gödel's God on the Computer, Informatikkolloquium, The University of Innsbruck, Austria, 2014. |

[184] | (Invited) Kurt Gödel's Gottesbeweis auf dem Computer, Lange Nacht der Wissenschaften, Berlin, Germany, 2014. |

[183] | Gödel's Proof of God's Existence, World Congress on the Square of Opposition VI, Vatican, 2014. (slides) |

2013 | |

[182] | A Top-down Approach to Combining Logics, 5th International Conference on Agents and Artificial Intelligence, Barcelona, Spain, 2013. (slides) |

[181] | HOL based Universal Reasoning, 4th World Congress and School on Universal Logic, Rio de Janeiro, Brazil, 2013. (slides) |

[180] | Cut-free calculi for challenge logics in a lazy way, International Workshop on Algebraic Logic in Computer Science (ALCS 2013), Stellenbosch, South Africa, 2013. (slides) |

[179] | (Invited Keynote) Gödel's God on the Computer, The 10th International Workshop on the Implementation of Logics (IWIL 2013), Stellenbosch, South Africa, 2013. (slides) |

[178] | HOL based First-order Modal Logic Provers, The 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2013), Stellenbosch, South Africa, 2013. (slides) |

[177] | Formalization, Mechanization and Automation of Gödel's Proof of God's Existence, Informatik Kolloquium, Freie Universität Berlin, Germany, 2013. (slides) |

[176] | Automating Quantified Conditional Logics is (relatively) Easy, Deduktionstreffen 2013, Koblenz, Germany, 2013. (slides) |

[175] | Automated Consistency Checking of Expressive Ontologies --- Beware of the Wrong Interpretation of Success!, The 5th International Workshop on Acquisition, Representation and Reasoning with Contextualized Knowledge (ARCOE-LogIC 2013), Corunna, Spain, 2013. (slides) |

[174] | Automating Quantified Conditional Logics in HOL, 23rd International Joint Conference on Artificial Intelligence (IJCAI 2013), Beijing, China, 2013. (poster) |

[173] | The Watson System -- An Overview, Freie Universität Berlin, Germany, 2013. |

[172] | LEO-II version 1.5, Third International Workshop on Proof Exchange for Theorem Proving (PxTP 2013), Lake Placid, NY, USA, 2013. (slides) |

2012 | |

[171] | Gödel's Unvollständigkeitssätze, Freie Universität Berlin, Germany, 2012. (slides) |

[170] | (Invited) Konzepte und Nutzen von Lambda-Ausdrücken in Java 8 (und Scala), Beuth Hochschule für Technik, Berlin, Germany, 2012. (slides) |

[169] | Implementing and Evaluating Provers for First-order Modal Logics, European Conference on Artificial Intelligence (ECAI-2012), Montpellier, France, 2012. (slides) |

[168] | (Invited) LEO-II --- Eine universelle Logikmaschine, Beuth Hochschule für Technik, Berlin, Germany, 2012. |

[167] | (Invited) Automating Expressive Classical and Non-Classical Logics with LEO-II, Computer Science Colloquium, Computer Science Colloquium, Freie Universität Berlin, Germany, 2012. |

[166] | (Invited; retirement celebration of Peter Andrews) Utilizing Higher-order Automated Theorem Provers as Universal Logic Engines, Carnegie Mellon University, USA, 2012. (slides) |

[165] | (Invited) Utilizing Church's Type Theory as a Universal Logic, Collegium Logicum Lecture Series, Kurt Gödel Society, Vienna, Austria, 2012. (slides) |

2011 | |

[164] | (Invited) 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. |

[163] | (Invited) Mechanisierung und Automatisierung von Kombinationen klassischer und nichtklassischer Logiken in klassischer Logik höherer Stufe, University of Hamburg, Germany, 2011. |

[162] | (Invited) Der Automatische Theorembeweiser LEO-II, BMW Group, Munich, Germany, 2011. |

[161] | (Invited) Intelligente Werkzeuge zur Erhebung, Bereitstellung, Analyse und Kommunikation von diversifiziertem, personifiziertem, interoperablen semantischen Wissen, Deutsches Institut für Wirtschaftsforschung, Berlin, Germany, 2011. |

[160] | Quantified Conditional Logics are Fragments of HOL, The International Conference on Non-classical Modal and Predicate Logics Guangzhou, China, 2011. (slides, [movie]) |

[159] | (Invited) Automating Expressive Non-classical Logics and their Combinations in Classical Higher Order Logic, University of Potsdam, Germany, 2011. (slides) |

2010 | |

[158] | Simple Type Theory as Framework for Combining Logics, Contest presentation at the World Congress and School on Universal Logic III (UNILOG'2010), Lisbon, Portugal, 2010. (slides) |

[157] | Progress in Automating Higher-Order Ontology Reasoning, Workshop on Practical Aspects of Automated Reasoning (PAAR-2010), Edinburgh, UK, 2010. (slides) |

[156] | Combining Logics in Simple Type Theory, 11th International Workshop on Computational Logic in Multi-Agent Systems (CLIMA XI), Lisbon, Portugal, 2010. (slides) |

[155] | Ontology Archaeology: Mining a Decade of Effort on the Suggested Upper Ontology, The ECAI-10 Workshop on Automated Reasoning about Context and Ontology Evolution (ARCOE-10), Lisbon, Portugal, 2010. (slides) |

[154] | Reasoning with Embedded Formulas and Modalities in SUMO, The ECAI-10 Workshop on Automated Reasoning about Context and Ontology Evolution (ARCOE-10), Lisbon, Portugal, 2010. (slides) |

[153] | Sigma: An Integrated Development Environment for Logical Theory Development, The ECAI 2010 Workshop on Intelligent Engineering Techniques for Knowledge Bases (IKBET'2010), Lisbon, Portugal, 2010. (slides) |

[152] | (Invited) Combining Logics in Simple Type Theory (and an Application in Ontology Reasoning), SRI International, Menlo Park, USA, 2010. (slides) |

[151] | (Invited) Winner Presentation: LEO-II, CASC-J5, Fifth International Joint Conference on Automated Reasoning (IJCAR 2010), Edinburgh, UK, 2010. (slides) |

[150] | (Invited) Adaptive Assertion-Level Proofs, The IJCAR 2010 Workshop on Evaluation Methods for Solvers and Quality Metrics for Solutions, Edinburgh, UK, 2010. (slides) |

[149] | (Invited) 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., Dagstuhl Seminar 10412: QSTRLib, Schloss Dagstuhl, Germany, 2010. |

2009 | |

[148] | Automating Quantified Multimodal Logics in HOL --- My very first Region Connection Calculus Prover, AAAI 2009 Spring Symposia, Stanford, USA, 2009. |

[147] | Handover of the Festschrift to Peter B. Andrews, CADE-22, Montreal, Canada, 2009. |

[146] | Automating Access Control Logics in Simple Type Theory with LE0-II, 24th IFIP International Information Security Conference, Pafos, Cyprus, 2009. (slides) |

[145] | Granularity-Adaptive Proof Presentation (poster), AIED, 2009. (poster) |

2008 | |

[144] | Some Results of the LEO-II Project, CIAO Workshop, TU Darmstadt, Germany, 2008. |

[143] | Exploring Properties of Normal Multimodal Logics in Simple Type Theory with LEO-II, Automated Reasoning Group Lunch Talk, The University of Cambridge, UK, 2008. |

[142] | Exploring Properties of Normal Multimodal Logics in Simple Type Theory with LEO-II, Deduktionstreffen, Saarbrücken, Germany, 2008. |

[141] | LEO-II Demo, ESHOL Workshop at the 4th International Joint Conference on Automated Reasoning (IJCAR 2008), Sydney, Australia, 2008. (slides) |

[140] | THF0 --- The Core TPTP Language for Classical Higher-Order Logic, The 4th International Joint Conference on Automated Reasoning (IJCAR 2008), Sydney, Australia, 2008. |

[139] | LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description), The 4th International Joint Conference on Automated Reasoning (IJCAR 2008), Sydney, Australia, 2008. (slides) |

[138] | (Invited) Exploring Properties of Multimodal Logics with the Cooperative Automatic Higher-Order Theorem Prover LEO-II, SRI International, Menlo Park, USA, 2008. (slides) |

[137] | LEO-II, A Higher-Order Theorem Prover (poster), VSI, 2008. (poster) |

[136] | (Invited) Tool Support for Formalized Mathematics: Cooperative Higher-Order Theorem Proving with LEO-II, Tutorial Dialogues on Proofs with the DIALOG demonstrator, and the PLATO/OMEGA Proof Assistant Plug-in for TeXmacs, Formal Mathematics Seminar, University of Bonn, Germany, 2008. (slides) |

[135] | (Invited) LEO-II --- A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic, Microsoft Research, Redmond, USA, 2008. |

[134] | (Invited) Automating Access Control Logics and Multimodal Logics in the Automatic Higher-Order Theorem Prover LEO-II, Kestrel Institute, Palo Alto, USA, 2008. |

[133] | (Invited) Automating Access Control Logics and Multimodal Logics in the Automatic Higher-Order Theorem Prover LEO-II, Pure and Applied Logic Seminar, Carnegie Mellon University, Pittsburgh, USA, 2008. (slides) |

2007 | |

[132] | The LEO-II Project, Omega-Ultra-Texmacs Mini Workshop, Saarbrücken, Germany, 2007. |

[131] | The LEO-II Project, Deduktionstreffen, Koblenz, Germany, 2007. |

[130] | The LEO-II Project, Automated Reasoning Workshop, London, UK, 2007. |

[129] | Progress Report on LEO-II: An Automatic Theorem Prover for Higher-Order Logic, Automated Reasoning Group Lunch Talk, The University of Cambridge, UK, 2007. (slides) |

[128] | Progress Report on LEO-II: An Automatic Theorem Prover for Higher-Order Logic, TPHOLs, Kaiserslautern, Germany, 2007. (slides) |

[127] | (Invited) Challenges for Automated Theorem Proving in Classical Higher Order Logics, Heriot-Watt University, Edinburgh, Scotland, 2007. |

[126] | (Invited) Challenges for Automated Theorem Proving in Classical Higher Order Logics, University of St. Andrews, St. Andrews, Scotland, 2007. (slides) |

[125] | (Invited) Challenges for Automated Theorem Proving in Classical Higher Order Logics, The University of Edinburgh, Scotland, 2007. |

[124] | (Invited Lecture Course) Semantics of Higher-Order Logics, IT University Copenhagen, Denmark, 2007. (slides) |

[123] | (Invited) Effiziente Automatisierung von Logik höherer Stufe---Realisierbarer Traum oder ewiger Albtraum?, Inaugural Lecture (Privatdozent) at Saarland University, Germany, 2007. |

[122] | Deep Inference for Automated Proof Tutoring (poster), KI, 2007. (poster) |

[121] | LEO-II, A Higher-Order Theorem Prover (poster), TPHOLs, 2007. (poster) |

[120] | The LEO-II Project (poster), University of Cambridge Project Poster, 2007. (poster) |

[119] | The LEO-II Project (poster), Deduktionstreffen, 2007. (poster) |

[118] | Term Indexing for the LEO-II Prover (poster), Deduktionstreffen, 2007. |

2006 | |

[117] | Dialog mit einem Beweisassistenten in natürlicher Sprache, Ringvorlesung, FR Informatik, Universität des Saarlandes, Germany, 2006. (slides) |

[116] | Underspecification in Math-DIALOG, C-Tag, SFB 378, Saarland University, Germany, 2006. (slides) |

[115] | Cut-Simulation in Impredicative Logics, Third International Joint Conference on Automated Reasoning (IJCAR 2006), LNAI , Seattle, USA, 2006. (slides) |

[114] | 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, 2006. (slides) |

[113] | Judging Granularity for Automated Mathematics Teaching, Short paper at LPAR 2006: 13th International Conference on Logic for Programming Artificial Intelligence and Reasoning, Pnom Penh, Cambodia, 2006. (slides) |

[112] | (Invited Lecture Course) Semantics of Higher-Order Logics, ESSLLI 2006, Malaga, Spain, 2006. (slides) |

[111] | (Invited) Service Oriented Architectures for Mathematics Assistance Systems, Fachhochschule Frankfurt am Main, Germany, 2006. |

[110] | (Invited) Classical Higher-Order Logic --- Semantics, Proof Theory and Automation, University of Potsdam, Germany, 2006. |

[109] | (Invited) Classical Higher-Order Logic --- Theory, Applications and Problems, Saarland University (scientific habilitation talk), Germany, 2006. (slides) |

[108] | Granularity Judgments in Proof Tutoring (poster), KI, 2006. (poster) |

2005 | |

[107] | Can a Higher-Order and a First-Order Theorem Prover Cooperate?, LPAR'04 Conference, Montevideo, Uruguay, 2005. (slides) |

[106] | New Directions in the OMEGA Project, CIAO'05 Workshop, Nottingham, UK, 2005. (slides) |

[105] | Designing a Proof GUI for non-Experts: Evaluation of an Experiment, UITP'05 Workshop (ETAPS Satellite Workshop), Edinburgh, Scotland, 2005. (slides) |

[104] | New Directions in the OMEGA Project, First Saarbrücken-Nancy Workshop on Higher-order Logic and Hybrid Logics, 2005. |

[103] | Mathematical Domain Reasoning Tasks in Tutorial Natural Language Dialog on Proofs, Twentieth National Conference on Artificial Intelligence (AAAI-05), Pittsburgh, Pennsylvania, USA, 2005. (slides) |

[102] | Mathematical Domain Reasoning Tasks in Tutorial Natural Language Dialog on Proofs, Dream Group Reunion, Edinburgh, UK, 2005. (slides) |

[101] | (Invited) A Structured Set of Higher-Order Problems, Dagstuhl Seminar 05431: Deduction and Applications, Schloss Dagstuhl, Germany, 2005. (slides) |

[100] | Mathematical Domain Reasoning Tasks in Tutorial Natural Language Dialog on Proofs, Theorema-Ultra-Omega-Workshop, Saarbrücken, Germany, 2005. (slides) |

[99] | Combining Proofs of Higher-Order and First-Order Automated Theorem Provers, LPAR-05 Workshop: Empirically Successfull Automated Reasoning in Higher-Order Logic (ESHOL), Montego Bay, Jamaica, 2005. |

[98] | System Description: LEO --- A Resolution based Higher-Order Theorem Prover, LPAR-05 Workshop: Empirically Successfull Automated Reasoning in Higher-Order Logic (ESHOL), Montego Bay, Jamaica, 2005. |

[97] | (Invited) Three Approaches for Guiding the Cooperation of Mathematical Reasoning Systems: Proof Planning, Agent-based Reasoning, and Autometad Composition of Reasoning Web Service, QSL Theme day: Integration of deductive tools. Nancy, France, 2005. (slides) |

[96] | (Invited) Can a Higher-Order and a First-Order Theorem Prover Cooperate?, LORIA, Nancy, France, 2005. (slides) |

[95] | (Invited) Logik höherer Stufe: Ein geeignetes Fundament für die Mathematik und für Formale Methoden?, TU Darmstadt, Germany, 2005. |

[94] | OMEGA (poster), Begehung SFB 378, 2005. (poster-1, poster-2, poster-3, poster-4) |

[93] | DIALOG (poster), Begehung SFB 378, 2005. (poster-1, poster-2, poster-3, poster-4) |

2004 | |

[92] | DIALOG: Natural Language-based Interaction with a Mathematical Assistance System, OMEGA talk series, Saarbrücken, Germany, 2004. (slides) |

[91] | Agent-oriented Proof Planning, Evaluation of the Collaborative Research Centre SFB378 Resource-adaptive Cognitive Processes, Saarbrücken, Germany, 2004. |

[90] | Semantics and Automation of Higher-Order Logic,, Workshop on Logic, Proofs, and Programs, Nancy, France, 2004. (slides) |

[89] | 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, 2004. |

[88] | DIALOG: Natural Language-based Interaction with a Mathematical Assistance System, Deduktionstreffen, Saarbrücken, Germany, 2004. (slides) |

[87] | OMEGA and DIALOG, Workshop on Logic, Proofs, and Programs, Saarbrücken, Germany, 2004. |

[86] | (Invited) OMEGA: A Mathematical Assistance System, Automated Reasoning Group, Cambridge University, Cambridge, UK, 2004. (slides) |

2003 | |

[85] | OMEGA, Meeting in camera of the Special Research Centre SFB 378, Dagstuhl, Germany, 2003. (slides) |

[84] | OMEGA - Ein Assistenzsystem für die Mathematik, Open day, Saarland University, Saarbrücken, Germany, 2003. (slides) |

[83] | The CALCULEMUS Research Training Network --- A short Overview, First QPQ Workshop on Deductive Software (QPQ'03), CADE-19, Miami, Florida, USA, 2003. (slides) |

[82] | Tutorial Dialogs on Mathematical Proofs, IJCAI-03 Workshop on Knowledge Representation and Automated Reasoning for E-Learning Systems, Acapulco, Mexico, 2003. (slides) |

[81] | A New Framework for Reasoning Agents, IJCAI-03 Workshop on Agents and Automated Reasoning, Acapulco, Mexico, 2003. (slides) |

[80] | Assertion Application in Theorem Proving and Proof Planning (poster), IJCAI-03 Poster Presentation, Acapulco, Mexico, 2003. (poster) |

[79] | The CALCULEMUS Research Training Network --- A short Overview, CALCULEMUS Symposium 2003, Rome, Italy, 2003. (slides) |

[78] | Bemerkungen zur Semantik und Mechanisierung von Logik hoeherer Stufe, Deduktionstreffen, Augsburg, Germany, 2003. (slides) |

[77] | (Invited) OMEGA --- From Proof Planning towards Mathematical Knowledge Management, MKM Symposium 2003, Edinburgh, Scotland, 2003. (slides) |

[76] | CALCULEMUS Midterm Review Report, Midterm Review of the European Union Research Training Network CALCULEMUS, Saarbrücken, Germany, 2003. (slides) |

[75] | Saarland University Node Report, Midterm Review of the European Union Research Training Network CALCULEMUS, Saarbrücken, Germany, 2003. (slides) |

[74] | CALCULEMUS - Systems for Integrated Deduction and Computation, Mathematics on the Semantic Web, Eindhoven, The Netherlands, 2003. (slides) |

[73] | Proof Development with OMEGA --- Square root of 2 is Irrational, Theorema-Omega'03 Workshop, Schloss Hagenberg, Austria, 2003. (slides) |

2002 | |

[72] | (Invited) Tutorial Dialog with a Mathematical Assistant System, Computer Science Department, The University of Birmingham, UK, 2002. |

[71] | (Invited Tutorial) From Natural Deduction to Sequent Calculus and back, CALCULEMUS Autumn School 2002, Pisa, Italy, 2002. (slides) |

[70] | Agent Based Theorem Proving (poster), AISB, 2002. (poster) |

[69] | Ressource-Adaptive Proof Planning with OMEGA, Meeting in camera of the Special Research Centre SFB 378, Wallerfangen, Germany, 2002. (slides) |

[68] | Tutorial Dialog with a Mathematical Assistant System, Meeting in camera of the Special Research Centre SFB 378, Wallerfangen, Germany, 2002. (slides) |

[67] | Agent based proof search with Indexed Formulas, CALCULEMUS 2002, Marseille, France, 2002. (slides) |

[66] | Tutorial Dialog with a Mathematical Assistant System, Computer Science Department, The University of Birmingham, UK, 2002. (slides) |

[65] | Reasoning Services in the MathWeb-SB for Symbolic Verification of Hybrid Systems, VERIFY'02 Workshop at FLOC 2002, Copenhagen, Denmark, 2002. |

[64] | Proof Development with OMEGA, CADE-18, Copenhagen, Denmark, 2002. (slides) |

[63] | Proof Development with OMEGA: Sqrt(2) is irrational, LPAR 2002, Tbilisi, Georgia,, 2002. (slides) |

2001 | |

[62] | (Invited) Concurrent Resource Guided Deduction, Theoretical Computer Science Seminar, School of Computer Science, The University of Birmingham, Birmingham, UK, 2001. (slides) |

[61] | (Invited Keynote) An Agent-based Approach to Reasoning, AISB'01 Convention Agents and Cognition in conjunction with 8th Workshop on Automated Reasoning: Bridging the Gap between Theory and Practice, University of York, UK, 2001. (slides) |

[60] | (Invited) Panel member of the IJCAR 2001 Workshop Future Directions in Automated Reasoning --- Problems and Ideas for a New Millennium, IJCAR 2001, Siena, Italy, 2001. |

[59] | (Invited) Agent-oriented Reasoning with O-ANTS, Department of Computer Science, Cornell University, Ithaca, NY, USA, 2001. |

[58] | (Invited) Agent-oriented Reasoning with O-ANTS, Pure and Applied Logic Seminar, Carnegie Mellon University, Pittsburgh, PA, USA, 2001. (slides) |

[57] | A Lost Proof (poster), TPHOLs, 2001. (poster) |

[56] | Proof Transformation and Expansion with a Parameterizable Inference Machine (poster), AISB, 2001. (poster) |

[55] | OMEGA (poster), Begehung SFB 378, 2001. (poster) |

[54] | DIALOG (poster), Begehung SFB 378, 2001. (poster) |

[53] | Tutorielle Kommunikation für ein mathematisches Assistenzsystem, Meeting in camera of the Special Research Division SFB378, Schloss Dagstuhl, Germany, 2001. |

[52] | OMEGA --- Ressourcenadaptives Beweisplanen, Meeting in camera of the Special Research Division SFB378, Schloss Dagstuhl, Germany, 2001. |

[51] | Agents in OMEGA, Meeting in camera of the OMEGA group, Saarbrücken, Germany, 2001. |

[50] | Agent-oriented theorem proving and proof planning in OMEGA, C++ days of SFB 378 Resource adaptive cognitive processes, Mertesdorf, Germany, 2001. |

[49] | A lost proof, TPHOLS 2001, Edinburgh, Scotland, 2001. |

[48] | An Agent-oriented approach to reasoning, CALCULEMUS Workshop 2001, Siena, Italy, 2001. |

[47] | Experiments with an Agent-oriented Reasoning System, KI 2001, Wien, Austria, 2001. (slides) |

[46] | Distributed Assertion Retrieval, First International Workshop on Mathematical Knowledge Management RISC-Linz, Schloss Hagenberg, Austria, 2001. (slides) |

2000 | |

[45] | (Invited) 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, UK, 2000. (slides) |

[44] | (Invited) Towards Agent based Theorem Proving and Proof Planning in OMEGA, Department of Computer Science, The University of York, UK, 2000. |

[43] | (Invited) OMEGA, MATHWEB and Friends, Department of Artificial Intelligence, The University of Edinburgh, Edinburgh, Scotland, 2000. |

[42] | (Invited) Resource Guided Concurrent Deduction with O-ANTS, Department of Artificial Intelligence, The University of Edinburgh, Edinburgh, Scotland, 2000. |

[41] | Proof Planning based on a Multi Agent Architecture?">Proof Planning based on a Multi Agent Architecture?, 9th CLAM - INKA - OMRS Workshop (CIAO), Schloss Dagstuhl, Germany, 2000. |

[40] | System demonstration: OMEGA, O-ANTS, and LEO, Department of Computer Science, The University of York, York, UK, 2000. |

[39] | Resource Guided Concurrent Deduction (poster), AISB, 2000. (poster) |

[38] | Resource Guided Concurrent Deduction, Short talk and poster presentation at Automated Reasoning Workshop 2000, King's College, London, UK, 2000. |

[37] | Towards agent based proof planning, Deduktionstreffen, Saarland University, Saarbrücken, Germany, 2000. |

[36] | OANTS --- An open approach at combining Interactive and Automated Theorem Proving, CALCULEMUS Symposium 2000, St. Andrews, Scotland, 2000. (slides) |

[35] | Eine übersicht zur AG Siekmann, Deduktionstreffen, Saarland University, Saarbrücken, Germany, 2000. |

[34] | Agent based proof planning with O-ANTS, Systemdemonstration at the Deduktionstreffen, Saarland University, Saarbrücken, Germany, 2000. (slides) |

1999 | |

[33] | (Invited) Extensional Higher Order Resolution, Paramodulation and RUE-Resolution, Theoretical Computer Science Seminar, School of Computer Science, The University of Birmingham, UK, 1999. (slides) |

[32] | (Invited) A two layered Agent Approach for Guiding Interactive Proofs, Theoretical Computer Science Seminar, School of Computer Science, The University of Birmingham, UK, 1999. |

[31] | Towards Fine-Grained Proof Planning with Critical Agents (poster), AISB, 1999. (poster) |

[30] | Agent based Proof Planning (poster), Poster at the 6th Workshop on Automated Reasoning: Bridging the Gap between Theory and Practice; in conjunction with AISB'99 Convention, Edinburgh, Scotland, 1999. |

[29] | On Automated Higher-Theorem Proving and Henkin Completeness, Forschungskolloquium der Studienstiftung des Deutschen Volkes, Berlin, Germany, 1999. (slides) |

[28] | Extensional Higher-Order Paramodulation and RUE-Resolution, 16th Conference on Automated Deduction, Trento, Italy, 1999. (slides) |

[27] | Agent Based Mathematical Reasoning, CALCULEMUS Workshop, Trento, Italy, 1999. (slides) |

[26] | Gleichheit und Extensionalität im automatischen Beweisen in Logik höherer Stufe, Promotionskolloquium, Saarbrücken, Germany,, 1999. |

[25] | Critical Agents Supporting Interactive Theorem Proving, 9th Portuguese Conference on Artificial Intelligence, Evora, Portugal, 1999. (slides) |

[24] | Ressourcenadaptive Vorschlagsagenten im Interaktiven Beweisen, Kollegiatentag im Rahmen der Herbstschule Kognitionswissenschaft, Saarbrücken, Germany, 1999. |

[23] | Ist KI eine empirische Wissenschaft?, SAG-WAS der AG Siekmann, Schloss Dagstuhl, Germany, 1999. |

1998 | |

[22] | LEO -- A Higher Order Theorem Prover, CADE, 1998. (poster) |

[21] | Model Existence for Higher-Order Logic, Oberseminar AG Siekmann, Saarland University, Saarbrücken, Germany, 1998. |

[20] | Integrating TPS with OMEGA, Oberseminar AG Siekmann, Saarland University, Saarbrücken, Germany, 1998. |

[19] | System Demonstration: OMEGA --- A mathematical Assistant, Evaluation of the SFB 378, Max-Planck Institute für Informatik (MPI), Saarbrücken, Germany, 1998. |

[18] | Exploiting past proof experience + Experiments in the Automatic Selection of Problem-solving Strategies, SAG-WAS'98 der AG Siekmann, Schloss Dagstuhl, Germany, 1998. |

[17] | LEO --- A Higher-Order Theorem Prover, The 15th International Conference on Automated Deduction, Lindau, Germany, 1998. |

[16] | System Demonstration: LEO --- A Higher-Order Theorem Prover, The 15th International Conference on Automated Deduction, Lindau, Germany, 1998. |

[15] | Integrating TPS with OMEGA, Workshop Inference Mechanisms in Knowledge-Based Systems: Theory and Applications, KI'98, Bremen, Germany, 1998. |

[14] | System Demonstration: Integrating TPS with OMEGA, Workshop Inference Mechanisms in Knowledge-Based Systems: Theory and Applications, KI'98, Bremen, Germany, 1998. |

[13] | Constraint Solving in Logig Programming and Automated Theorem Proving: a comparison, 8th International Conference on Artificial Intelligence: Methodology, Systems, Applications (AIMSA'98), Sozopol, Bulgaria, 1998. |

[12] | System Demonstration: OMEGA --- a Mathematical Assistant, 8th International Conference on Artificial Intelligence: Methodology, Systems, Applications (AIMSA'98), Sozopol, Bulgaria, 1998. |

[11] | System Demonstration: OMEGA --- a Mathematical Assistant, Deduktionstreffen, Munich, Germany, 1998. |

[10] | 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 des Saarlandes) Saarbrücken, Germany, 1998. |

1997 | |

[9] | LEO --- Towards Higher-Order Resolution, Automated theorem proving seminar, Department of Mathematics, Carnegie Mellon Univerity, Pittsburgh, USA, 1997. (slides) |

[8] | Equalizing terms by Difference Reduction and Abstraction, Automated theorem proving seminar, Department of Mathematics, Carnegie Mellon Univerity, Pittsburgh, USA, 1997. |

[7] | Embedding Extensionality in Higher-Order Resolution, Oberseminar AG Siekmann, Saarland University, Saarbrücken, Germany, 1997. |

[6] | Extensionale Resolution höherer Stufe, Deduktionstreffen, Schloss Dagstuhl, Germany, 1997. |

[5] | Extensionale Resolution höherer Stufe, Forschungskolloquium der Studienstiftung des Deutschen Volkes, Kochl am See, Germany, 1997. |

1996 | |

[4] | Higher-Order Resolution and Extensionality, Oberseminar AG Siekmann, Saarland University, Saarbrücken, Germany, 1996. (slides) |

[3] | Ein kategorieller Kalkül ebener und räumlicher Netze, Sommerakademie der Studienstiftung des Deutschen Volkes, St. Johann, Südtirol, Italy, 1996. |

1995 | |

[2] | HO-Differenzreduzierung, Oberseminar AG Siekmann, Saarland University, Saarbrücken, Germany, 1995. |

[1] | Towards Higher-Order Theorem Proving with equality, Deduktionstreffen, Saarland University, Saarbrücken, Germany, 1995. (slides) |

Powered by bibtexbrowser