•  660
    Computers may help us to better understand (not just verify) arguments. In this article we defend this claim by showcasing the application of a new, computer-assisted interpretive method to an exemplary natural-language ar- gument with strong ties to metaphysics and religion: E. J. Lowe’s modern variant of St. Anselm’s ontological argument for the existence of God. Our new method, which we call computational hermeneutics, has been particularly conceived for use in interactive-automated proof ass…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
  •  187
    Higher-Order Semantics and Extensionality
    with Chad E. Brown and Michael Kohlhase
    Journal of Symbolic Logic 69 (4). 2004.
    In this paper we re-examine the semantics of classical higher-order logic with the purpose of clarifying the role of extensionality. To reach this goal, we distinguish nine classes of higher-order models with respect to various combinations of Boolean extensionality and three forms of functional extensionality. Furthermore, we develop a methodology of abstract consistency methods (by providing the necessary model existence theorems) needed to analyze completeness of (machine-oriented) higher-ord…Read more
  •  139
    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
  •  101
    We investigate several approaches to resolution based automated theoremproving in classical higher-order logic (based on Church's simply typedλ-calculus) and discuss their requirements with respect to Henkincompleteness and full extensionality. In particular we focus on Andrews' higher-order resolution (Andrews 1971), Huet's constrained resolution (Huet1972), higher-order E-resolution, and extensional higher-order resolution(Benzmüller and Kohlhase 1997). With the help of examples we illustratet…Read more
  •  97
    Higher-order semantics and extensionality
    with Chad E. Brown and Michael Kohlhase
    Journal of Symbolic Logic 69 (4): 1027-1088. 2004.
    In this paper we re-examine the semantics of classical higher-order logic with the purpose of clarifying the role of extensionality. To reach this goal, we distinguish nine classes of higher-order models with respect to various combinations of Boolean extensionality and three forms of functional extensionality. Furthermore, we develop a methodology of abstract consistency methods needed to analyze completeness of higher-order calculi with respect to these model classes
  •  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
  •  61
    Starting from a generalization of the standard axioms for a monoid we present a stepwise development of various, mutually equivalent foundational axiom systems for category theory. Our axiom sets have been formalized in the Isabelle/HOL interactive proof assistant, and this formalization utilizes a semantically correct embedding of free logic in classical higher-order logic. The modeling and formal analysis of our axiom sets has been significantly supported by series of experiments with automate…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.
  •  37
    Cut-Elimination for Quantified Conditional Logic
    Journal of Philosophical Logic 46 (3): 333-353. 2017.
    A semantic embedding of quantified conditional logic in classical higher-order logic is utilized for reducing cut-elimination in the former logic to existing results for the latter logic. The presented embedding approach is adaptable to a wide range of other logics, for many of which cut-elimination is still open. However, special attention has to be payed to cut-simulation, which may render cut-elimination as a pointless criterion.
  •  37
    Multimodal and intuitionistic logics in simple type theory
    with Lawrence Paulson
    Logic Journal of the IGPL 18 (6): 881-892. 2010.
    We study straightforward embeddings of propositional normal multimodal logic and propositional intuitionistic logic in simple type theory. The correctness of these embeddings is easily shown. We give examples to demonstrate that these embeddings provide an effective framework for computational investigations of various non-classical logics. We report some experiments using the higher-order automated theorem prover LEO-II
  •  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
  •  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
  •  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
  •  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.
  •  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.
  •  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
  •  21
    Combining and Automating Classical and Non-Classical Logics in Classical Higher-Order Logic
    Annals of Mathematics and Artificial Intelligence) 62 (1-2): 103-128. 2011.
  •  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
  •  19
    Combined reasoning by automated cooperation
    with Volker Sorge, Mateja Jamnik, and Manfred Kerber
    Journal of Applied Logic 6 (3): 318-342. 2008.
  •  17
    Sigma: An Integrated Development Environment for Formal Ontology
    with Adam Pease
    AI Communications 26 (1): 79-97. 2013.
  •  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
    Assertion-level Proof Representation with Under-Specification
    with Serge Autexier, Armin Fiedler, Helmut Horacek, and Bao Quoc Vo
    Electronic Notes in Theoretical Computer Science 93 5-23. 2004.
  •  15
    Sweet SIXTEEN: Automation via Embedding into Classical Higher-Order Logic
    with Alexander Steen
    Logic and Logical Philosophy 25 (4): 535-554. 2016.
  •  14
    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.