•  311
    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
  •  148
    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
  •  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
  •  88
    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
  •  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
  •  75
    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 illustratethe…Read more
  •  41
    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
  •  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.
  •  27
    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.
  •  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
  •  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
  •  19
    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
  •  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
  •  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
  •  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.
  •  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.
  •  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.
  •  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
  •  11
    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.
  •  9
    Combined reasoning by automated cooperation
    with Volker Sorge, Mateja Jamnik, and Manfred Kerber
    Journal of Applied Logic 6 (3): 318-342. 2008.
  •  9
    Sweet SIXTEEN: Automation via Embedding into Classical Higher-Order Logic
    with Alexander Steen
    Logic and Logical Philosophy 25 (4): 535-554. 2016.
  •  9
    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.
  •  8
    Accessing knowledge of a single knowledge source with different client applications often requires the help of mediator systems as middleware components. In the domain of theorem proving large efforts have been made to formalize knowledge for mathematics and verification issues, and to structure it in databases. But these databases are either specialized for a single client, or if the knowledge is stored in a general database, the services this database can provide are usually limited and hard t…Read more
  •  8
    Higher-order Aspects and Context in SUMO
    with Adam Pease
    Journal of Web Semantics 12 104-117. 2012.
  •  8
    Agent based Mathematical Reasoning
    with Mateja Jamnik, Manfred Kerber, and Volker Sorge
    Electronic Notes in Theoretical Computer Science, Elsevier 23 (3): 21-33. 1999.
    In this contribution we propose an agent architecture for theorem proving which we intend to investigate in depth in the future. The work reported in this paper is in an early state, and by no means finished. We present and discuss our proposal in order to get feedback from the Calculemus community.
  •  8
    Sigma: An Integrated Development Environment for Formal Ontology
    with Adam Pease
    AI Communications 26 (1): 79-97. 2013.