| Christoph Benzmüller (University of Luxembourg) |
| Mon 17 Jun 2019, 14:00 - 15:00 |
| IF 4.31/4.33 |
If you have a question about this talk, please contact: Allison Kruk (v1atayl6)
Refreshments provided
Title
On Universal Logical Reasoning and Gödel's Ontological Argument
Abstract
Classical higher-order logic, when utilized as a meta-logic in which various other (classical and non-classical) logics can be shallowly embedded, is suitable as a foundation for the development of a universal logical reasoning engine. Such an engine may be employed, as already envisioned by Leibniz, to support the rigorous formalisation and deep logical analysis of rational arguments on the computer.
Recent experiments (with Isabelle/HOL and Leo-III) are discussed in which mechanized computational techniques were used to unearth philosophical insights on Gödel’s ontological argument for the existence of God. A particular focus in these recent experiments is on modal collapse (which excludes contingency) and the question on how it can be avoided in Gödel’s argument.
Further prominent applications of the approach are briefly outlined if time permits. These include formal encodings and assessments of (i) Zalta's Principia Logico-Metaphysica, (ii) Gewirth's Principle of Generic Consistency, (iii) different axiom systems for category theory proposed by MacLane, Scott, Freyd and Scedrov, and (iv) paradoxes in deontic reasoning that are relevant for the modelling of explicit ethical systems.
Biography
Christoph Benzmüller is a professor in artificial intelligence/computer science and mathematics at Freie Universität Berlin (Germany). He is also a visiting scholar of the University of Luxembourg (Luxembourg). Christoph's prior research institutions include the universities of Stanford (USA), Cambridge, Birmingham, Edinburgh (all UK), the Saarland (Germany) and CMU (USA).
Christoph received his PhD (1999) and his Habilitation (2007) from Saarland University, his PhD research was partly conducted at CMU. In 2012, Christoph was awarded with a Heisenberg Research Fellowship of the German National Research Foundation (DFG).
The research activities of Christoph are interfacing the areas of artificial intelligence, philosophy, mathematics, computer science, and natural language. Many of these activities draw on classical higher-order logic (HOL), which has is roots in the work by Russel and Church. Christoph has contributed to the semantics and proof theory of HOL, and together with colleagues and students he has developed the Leo theorem provers for HOL. More recently he has been utilising HOL as a universal meta-logic to automate various non-classical logics in topical application areas, including machine ethics & machine law (responsible AI), rational argumentation, metaphysics, category theory, etc. Recent research also addresses the integration of automated reasoning and machine learning.
Christoph is trustee and vice-president of CADE (Conference on Automated Deduction), board member of AAR (Association of Automated Reasoning), steering committee member of DEON (Society of Deontic Logic and Normative Systems) and former spokesman of the section Deduction Systems of the Gesellschaft für Informatik. He serves in various further functions (chair, editorial board, steering committee, trustee, etc.) for a range of conferences and organisations in artificial intelligence, computer science, philosophy and mathematics.
Prior to his academia career, Christoph Benzmüller was a successful long-distance runner at German national level.