•  7
    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
  •  1
    Who Finds the Short Proof?
    with David Fuenmayor, Alexander Steen, and Geoff Sutcliffe
    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.
  •  22
    Symbolic Ai and Gödel's Ontological Argument
    Zygon 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
  •  11
    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
  •  12
  •  20
    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
  •  202
    Mechanizing principia logico-metaphysica in functional type-theory
    Review 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
  •  8
    Computational Metaphysics
    with Max Wisniewski and Alexander Steen
  •  13
    A Computational-Hermeneutic Approach for Conceptual Explicitation
    with David Fuenmayor
    In 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
  •  75
    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
  •  29
    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
  •  49
    An 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.
  •  25
    Lectures on Jacques Herbrand as a Logician
    with Claus-Peter Wirth, Jörg Siekmann, and Serge Autexier
    Seki 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
  •  23
    Jacques Herbrand: life, logic, and automated deduction
    with Claus-Peter Wirth, Jörg Siekmann, and Serge Autexier
    In Dov Gabbay (ed.), The Handbook of the History of Logic, Elsevier. pp. 195-254. 2009.
  •  17
    Proof Step Analysis for Proof Tutoring -- A Learning Approach to Granularity
    with Marvin Schiller and Dominik Dietrich
    Teaching Mathematics and Computer Science 6 (2): 325-343. 2008.
  •  16
    Computer supported mathematics with Ωmega
    with Jörg Siekmann and Serge Autexier
    Journal of Applied Logic 4 (4): 533-559. 2006.
  •  15
    Sweet SIXTEEN: Automation via Embedding into Classical Higher-Order Logic
    with Alexander Steen
    Logic and Logical Philosophy 25 (4): 535-554. 2016.
  •  17
    Sigma: An Integrated Development Environment for Formal Ontology
    with Adam Pease
    AI Communications 26 (1): 79-97. 2013.
  •  12
    Interactive Theorem Proving with Tasks
    with Malte Hübner, Serge Autexier, and Andreas Meier
    Electronic Notes in Theoretical Computer Science 103 (C): 161-181. 2004.
  •  24
    Automatic Learning of Proof Methods in Proof Planning
    with Mateja Jamnik, Manfred Kerber, and Martin Pollet
    Logic 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
  •  22
    The Higher-Order Prover LEO-II
    with Nik Sultana, Lawrence C. Paulson, and Frank Theiß
    Journal of Automated Reasoning 55 (4): 389-404. 2015.
  •  7
    The Calculemus Midterm Report (edited book)
    with Corinna Hahn
    Saarland University, Germany. 2003.