•  2
    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
  •  18
    Mechanizing principia logico-metaphysica in functional type-theory
    Review of Symbolic Logic 13 (1): 206-218. 2020.
    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
  •  3
    Computational Metaphysics
    with Max Wisniewski and Alexander Steen
  •  1
    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, 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
  •  27
    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 develop results in modal metaphysics whose discovery was computer assisted, and conclude that these results work not only to the obvious benefit of philosophy but also, less obviously, to the benefit o…Read more
  •  13
    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
  •  31
    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.
  •  84
    *Principia Logico-Metaphysica* (a developing, online manuscript) contains a foundational logical theory for metaphysics, mathematics, and the sciences. It contains a canonical development of Abstract Object Theory [AOT], a metaphysical theory (inspired by ideas of Ernst Mally, formalized by Zalta) that differentiates 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 Isabell…Read more
  •  18
    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
  •  13
    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.
  •  7
    Computer supported mathematics with Ωmega
    with Jörg Siekmann and Serge Autexier
    Journal of Applied Logic 4 (4): 533-559. 2006.
  •  9
    Sweet SIXTEEN: Automation via Embedding into Classical Higher-Order Logic
    with Alexander Steen
    Logic and Logical Philosophy 25 (4): 535-554. 2016.
  •  15
    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.
  •  7
    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.
  •  20
    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
  •  8
    Sigma: An Integrated Development Environment for Formal Ontology
    with Adam Pease
    AI Communications 26 (1): 79-97. 2013.
  •  1
    The Calculemus Midterm Report (edited book)
    with Corinna Hahn
    Saarland University, Germany. 2003.
  •  15
    The Higher-Order Prover LEO-II
    with Nik Sultana, Lawrence C. Paulson, and Frank Theiß
    Journal of Automated Reasoning 55 (4): 389-404. 2015.
  •  3
    The curious inference of Boolos in MIZAR and OMEGA
    with Chad Brown
    In Roman Matuszewski & Anna Zalewska (eds.), From Insight to Proof -- Festschrift in Honour of Andrzej Trybulec, The University of Bialystok, Polen. pp. 299-388. 2007.
  •  2
    The Calculemus Final Report
    with Corinna Hahn
    Saarland University, Germany. 2004.
  •  6
    Natural Language Dialog with a Tutor System for Mathematical Proofs
    with Helmut Horacek, Ivana Kruijff-Korbayova, Manfred Pinkal, Jörg Siekmann, and Magdalena Wolska
    In Ruqian Lu, Jörg Siekmann & Carsten Ullrich (eds.), Cognitive Systems, Springer. pp. 1-14. 2007.
  •  5
    Omega
    with Armin Fiedler, Andreas Meier, Martin Pollet, and Jörg Siekmann
    In Freek Wiedijk (ed.), The Seventeen Provers of the World, Springer. pp. 127-141. 2006.
  •  118
    Quantified Multimodal Logics in Simple Type Theory
    with Lawrence C. Paulson
    Logica Universalis 7 (1): 7-20. 2013.
    We present an embedding of quantified multimodal logics into simple type theory and prove its soundness and completeness. A correspondence between QKπ models for quantified multimodal logics and Henkin models is established and exploited. Our embedding supports the application of off-the-shelf higher-order theorem provers for reasoning within and about quantified multimodal logics. Moreover, it provides a starting point for further logic embeddings and their combinations in simple type theory