Professor Dr. habil.
University of Luxembourg, FSTC (Visiting Scholar)
Saarland University, Dep. of CS (Privatdozent)
Arnimallee 7, 14195 Berlin Tel.: +49(0)30 838 52485
|• Preprints: Reasonable Machines: A Research Manifesto, KI2020, and Encoding Legal Balancing: Automating an Abstract Ethico-Legal Value Ontology in Preference Logic, 2020 (submitted)|
|• Preprint: Designing Normative Theories for Ethical and Legal Reasoning: LogiKEy Framework, Methodology, and Tool Support, Artificial Intelligence, 2020|
|• Preprint: A (Simplified) Supreme Being Necessarily Exists, says the Computer: Computationally Explored Variants of Gödel's Ontological Argument, KR 2020, 2020|
|Research Vision, Position Papers|
|● Reasonable Machines: A Research Manifesto, KI, 2020 [details] ● What is a proof? What should it be?, 2019 [details]|
|Universal Logical Reasoning, Shallow Semantical Embeddings and Computational Hermeneutics|
|● Universal (Meta-)Logical Reasoning: Recent Successes, Sci. Comp. Progr., 2019 [details] ● A Computational-Hermeneutic Approach for Conceptual Explicitation, SAPERE, 2019 [details] ● Higher-order Logic as Lingua Franca - Integrating Argumentative Discourse and Deep Logical Analysis, 2020 [details] ● Cut-Elimination for Quantified Conditional Logic, J. Phil. Log., 2017 [details] ● Quantified Multimodal Logics in Simple Type Theory , Log. Univ., 2013 [details]|
|Normative Reasoning and Machine Ethics|
|● Designing Normative Theories for Ethical and Legal Reasoning: LogiKEy Framework, Methodology, and Tool Support, AI Journal, 2020 [details] ● Encoding Legal Balancing: Automating an Abstract Ethico-Legal Value Ontology in Preference Logic, 2020 [details] ● I/O Logic in HOL, J. Appl. Log., 2019 [details] ● A Dyadic Deontic Logic in HOL, DEON, 2018 [details]|
|Computational Metaphysics and the Ontological Argument|
|● A (Simplified) Supreme Being Necessarily Exists, says the Computer: Computationally Explored Variants of Gödel's Ontological Argument, KR, 2020 [details] ● Computer-supported Analysis of Positive Properties, Ultrafilters and Modal Collapse in Variants of Gödel's Ontological Argument, Bulletin of the Section of Logic, 2020 [details] ● Mechanizing Principia Logico-Metaphysica in Functional Type Theory, Rev. Symb. Log., 2020 [details] ● Computer Science and Metaphysics: A Cross-Fertilization, Open Philosophy, 2019 [details] ● The Inconsistency in Gödel's Ontological Argument: A Success Story for AI in Metaphysics, IJCAI, 2016 [details] ● Automating Gödel's Ontological Proof of God's Existence with Higher-order Automated Theorem Provers, ECAI, 2014 [details]|
|Foundations of Maths, Category Theory|
|● Automating Free Logic in HOL, with an Experimental Application in Category Theory, J. Autom. Reason., 2020 [details] ● Computer-supported Exploration of a Categorical Axiomatization of Modeloids, RAMiCS, 2020 [details]|
|Higher-order Logic, Higher-order Automated Theorem Proving|
|● Church's Type Theory, Stanford Encyclopedia of Philosophy, 2019 [details] ● The Higher-Order Prover Leo-III, IJCAR, 2018 [details] ● The Higher-Order Prover Leo-II, J. Autom. Reason., 2015 [details] ● Automation of Higher-Order Logic, Handbook of the History of Logic, 2014 [details] ● Higher-Order Semantics and Extensionality, J. Symb. Log., 2004 [details]|
|Maths Proof Assistants, Natural Language Proof Tutoring, Agent-based Reasoning|
|● OMEGA: Resource-Adaptive Processes in an Automated Reasoning, Cognitive Technologies, 2010 Systems, [details] ● Computer Supported Mathematics with OMEGA, J. Appl. Log., 2006 [details] ● Resource-Bounded Modelling and Analysis of Human-Level Interactive Proofs, Cognitive Technologies, 2010 [details] ● Granularity-Adaptive Proof Presentation, AIED, 2009 [details] ● Mathematical Domain Reasoning Tasks in Natural Language Tutorial Dialog on Proofs, AAAI, 2005 [details] ● Proof Development in OMEGA: The Irrationality of Square Root of 2, 2003 [details]|
In a collaboration with Bruno Woltzenlogel Paleo and others, I have
analysed variants of
Kurt Gödel's ontological
argument for the existence of God on the computer. This work had a media
repercussion on a global scale.
Here is more
information of this line of research.
Our related lecture concept on Computational Metaphysics won the central teaching award of Freie Universität Berlin. More information on the course: lecture course proposal and website/schedule.
|CLAIRE-AI (national contact point), Conference on Automated Deduction, Association for Automated Reasoning, Society of Deontic Logic and Normative Systems, Berlin Mathematics Research Center MATH+, Berlin Mathematical School, Fachgruppe Deduktionssysteme der GI, IFCoLog, Logic Journal of the IGPL, Journal of Applied Logics|
|I was passionate middle and long-distance runner. In the early 90's I lived and trained at the Olympic Centre in Saarbrücken. In 1990 I was German Champion with the men's team in cross-country running. Feel free to beat some of my personal records: 2:25min (1000m), 3:49min (1500m), 8:14min (3000m), 14:13min (5000m), 30:04min (10000m).|