Keywords: Invited Presentations

2018 | |

[100] | (Invited Keynote) tba , 12th All India Students' Conference on Science and Spiritual Quest (AISSQ), IIT Bhubaneswar, India, 2018. (forthcoming) |

[99] | (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. (forthcoming) |

[98] | (Invited Keynote) tba , 14th International Conference on Deontic Logic and Normative Systems (DEON 2018), Utrecht, Netherlands, 2018. (forthcoming) |

[97] | (Invited) A Deontic Logic Reasoning Infrastructure , Special Session on the History and Philosophy of Computing (HaPoC) at the Computability in Europe (CiE) conference, 2018. (forthcoming) |

[96] | (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. |

[95] | 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, movie) |

[94] | (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 | |

[93] | (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) |

[92] | (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. |

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

[90] | (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) |

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

[88] | (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) |

[87] | (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. |

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

[85] | (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. (poster) |

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

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

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

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

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

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

2016 | |

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

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

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

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

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

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

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

[71] | (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) |

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

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

2015 | |

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

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

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

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

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

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

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

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

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

[59] | (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) |

[58] | (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. |

[57] | (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 | |

[56] | (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) |

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

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

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

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

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

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

2013 | |

[49] | (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) |

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

2012 | |

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

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

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

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

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

2011 | |

[42] | (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. |

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

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

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

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

2010 | |

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

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

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

[34] | (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. |

2008 | |

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

[32] | (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) |

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

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

[29] | (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 | |

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

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

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

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

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

2006 | |

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

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

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

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

2005 | |

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

[18] | (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) |

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

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

2004 | |

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

2003 | |

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

2002 | |

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

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

2001 | |

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

[10] | (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) |

[9] | (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. |

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

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

2000 | |

[6] | (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) |

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

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

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

1999 | |

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

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

Powered by bibtexbrowser