-
10A Simplified Variant of Gödel’s Ontological ArgumentIn Vestrucci Andrea (ed.), Beyond Babel: Religion and Linguistic Pluralism, Springer Verlag. pp. 271-286. 2023.A simplified variant of Gödel’s ontological argument is presented. The simplified argument is valid already in basic modal logics K or KT, it does not suffer from modal collapse, and it avoids the rather complex predicates of essence (Ess.) and necessary existence (NE) as used by Gödel. The variant presented has been obtained as a side result of a series of theory simplification experiments conducted in interaction with a modern proof assistant system. The starting point for these experiments wa…Read more
-
8On Gödel and the Nonexistence of Time – Gödel und die Nichtexistenz der Zeit: Kurt Gödel essay competition 2021 – Kurt-Gödel-Preis 2021 (edited book)Springer Berlin Heidelberg. 2023.
-
29Analysis of an Ontological Proof Proposed by LeibnizIn Charles Tandy (ed.), Death and Anti-Death, Volume 14: Four Decades After Michael Polanyi, Three Centuries After G.W. Leibniz, Ria University Press. 2016.
-
3Who Finds the Short Proof?Logic Journal of the IGPL. forthcoming.This paper reports on an exploration of Boolos’ Curious Inference, using higher-order automated theorem provers (ATPs). Surprisingly, only suitable shorthand notations had to be provided by hand for ATPs to find a short proof. The higher-order lemmas required for constructing a short proof are automatically discovered by the ATPs. Given the observations and suggestions in this paper, full proof automation of Boolos’ and related examples now seems to be within reach of higher-order ATPs.
-
22Symbolic Ai and Gödel's Ontological ArgumentZygon 57 (4): 953-962. 2022.Over the past decade, variants of Gödel's ontological arguments have been critically examined using modern symbolic AI technology. Computers have unearthed new insights about them and even contributed to the exploration of new, simplified variants of the argument, which now need to be further investigated by theologians and philosophers. In this article, I provide a brief, informal overview of these contributions and engage in a discussion of the possible future role of AI technology for the rig…Read more
-
Logic and Argumentation: Fourth International Conference, CLAR 2021, Hangzhou, China, October 20–22 (edited book)Springer. 2021.
-
29Wider den Reduktionismus -- Ausgewählte Beiträge zum Kurt Gödel Preis 2019 (edited book)Springer Nature Switzerland. 2021.Die Autorinnen und Autoren präsentieren in diesem Buch Argumente, die die Unmöglichkeit des Reduktionismus aus philosophischer, naturwissenschaftlicher bzw. mathematisch-logischer Perspektive zu begründen suchen. Der Reduktionismus behauptet, dass Eigenschaften auch von komplexen Systemen vollständig auf ihre Bestandteile zurückgeführt werden können. Diese Position ist einflussreich, aber umstritten. Im Jahr 2019 hat der Kurt Gödel Freundeskreis einen Essaywettbewerb veranstaltet, um schlagende …Read more
-
18Designing normative theories for ethical and legal reasoning: LogiKEy framework, methodology, and tool supportArtificial Intelligence 287 103348. 2020.
-
24Computer-supported Analysis of Positive Properties, Ultrafilters and Modal Collapse in Variants of Gödel's Ontological ArgumentBulletin of the Section of Logic 49 (2). 2020.Three variants of Kurt Gödel's ontological argument, proposed by Dana Scott, C. Anthony Anderson and Melvin Fitting, are encoded and rigorously assessed on the computer. In contrast to Scott's version of Gödel's argument the two variants contributed by Anderson and Fitting avoid modal collapse. Although they appear quite different on a cursory reading they are in fact closely related. This has been revealed in the computer-supported formal analysis presented in this article. Key to our formal an…Read more
-
224Mechanizing principia logico-metaphysica in functional type-theoryReview of Symbolic Logic 13 (1): 206-218. 2018.Principia Logico-Metaphysica contains a foundational logical theory for metaphysics, mathematics, and the sciences. It includes a canonical development of Abstract Object Theory [AOT], a metaphysical theory that distinguishes between ordinary and abstract objects.This article reports on recent work in which AOT has been successfully represented and partly automated in the proof assistant system Isabelle/HOL. Initial experiments within this framework reveal a crucial but overlooked fact: a deeply…Read more
-
18A Computational-Hermeneutic Approach for Conceptual ExplicitationIn Matthieu Fontaine, Cristina Barés-Gómez, Francisco Salguero-Lamillar, Lorenzo Magnani & Ángel Nepomuceno-Fernández (eds.), Model-Based Reasoning in Science and Technology: Inferential Models for Logic, Language, Cognition and Computation, Springer Verlag. 2019.We present a computer-supported approach for the logical analysis and conceptual explicitation of argumentative discourse. Computational hermeneutics harnesses recent progresses in automated reasoning for higher-order logics and aims at formalizing natural-language argumentative discourse using flexible combinations of expressive non-classical logics. In doing so, it allows us to render explicit the tacit conceptualizations implicit in argumentative discursive practices. Our approach operates on…Read more
-
80Computer Science and Metaphysics: A Cross-FertilizationOpen Philosophy 2 (1): 230-251. 2019.Computational philosophy is the use of mechanized computational techniques to unearth philosophical insights that are either difficult or impossible to find using traditional philosophical methods. Computational metaphysics is computational philosophy with a focus on metaphysics. In this paper, we (a) develop results in modal metaphysics whose discovery was computer assisted, and (b) conclude that these results work not only to the obvious benefit of philosophy but also, less obviously, to the b…Read more
-
31Mechanizing principia logico-metaphysica in functional type theoryReview of Symbolic Logic 1-13. 2019.Principia Logico-Metaphysica contains a foundational logical theory for metaphysics, mathematics, and the sciences. It includes a canonical development of Abstract Object Theory [AOT], a metaphysical theory that distinguishes between ordinary and abstract objects. This article reports on recent work in which AOT has been successfully represented and partly automated in the proof assistant system Isabelle/HOL. Initial experiments within this framework reveal a crucial but overlooked fact: a deepl…Read more
-
54An ambitious ethical theory ---Alan Gewirth's "Principle of Generic Consistency"--- is encoded and analysed in Isabelle/HOL. Gewirth's theory has stirred much attention in philosophy and ethics and has been proposed as a potential means to bound the impact of artificial general intelligence.
-
19Can Computers Help to Sharpen our Understanding of Ontological Arguments?In Christoph Benzmüller & David Fuenmayor (eds.), Mathematics and Reality, Proceedings of the 11th All India Students' Conference on Science Spiritual Quest, 6-7 October, 2018, IIT Bhubaneswar, Bhubaneswar, India, The Bhaktivedanta Institute. pp. 195226. 2018.
-
26Lectures on Jacques Herbrand as a LogicianSeki Publications (Issn 1437-4447). 2009.We give some lectures on the work on formal logic of Jacques Herbrand, and sketch his life and his influence on automated theorem proving. The intended audience ranges from students interested in logic over historians to logicians. Besides the well-known correction of Herbrand’s False Lemma by Goedel and Dreben, we also present the hardly known unpublished correction of Heijenoort and its consequences on Herbrand’s Modus Ponens Elimination. Besides Herbrand’s Fundamental Theorem and its relation…Read more
-
20Proof Step Analysis for Proof Tutoring -- A Learning Approach to GranularityTeaching Mathematics and Computer Science 6 (2): 325-343. 2008.
-
16Sweet SIXTEEN: Automation via Embedding into Classical Higher-Order LogicLogic and Logical Philosophy 25 (4): 535-554. 2016.
-
27Jacques Herbrand: life, logic, and automated deductionIn Dov Gabbay (ed.), The Handbook of the History of Logic, Elsevier. pp. 195-254. 2009.
-
13Interactive Theorem Proving with TasksElectronic Notes in Theoretical Computer Science 103 (C): 161-181. 2004.
-
30Automatic Learning of Proof Methods in Proof PlanningLogic Journal of the IGPL 11 (6): 647-673. 2003.In this paper we present an approach to automated learning within mathematical reasoning systems. In particular, the approach enables proof planning systems to automatically learn new proof methods from well-chosen examples of proofs which use a similar reasoning pattern to prove related theorems. Our approach consists of an abstract representation for methods and a machine learning technique which can learn methods using this representation formalism. We present an implementation of the approac…Read more
-
20Sigma: An Integrated Development Environment for Formal OntologyAI Communications 26 (1): 79-97. 2013.
-
12Verifying the Modal Logic Cube is an Easy TaskIn Simon Siegler & Nathan Wasser (eds.), Verification, Induction, Termination Analysis - Festschrift for Christoph Walther on the Occasion of His 60th Birthday, Springer. pp. 117-128. 2010.
Zehnruthenplan, Brandenburg, Germany
Areas of Specialization
Metaphysics and Epistemology |
Science, Logic, and Mathematics |
Areas of Interest
Metaphysics and Epistemology |
Science, Logic, and Mathematics |