-
660Computers 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
-
202Mechanizing 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
-
187Higher-Order Semantics and ExtensionalityJournal 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
-
139Quantified Multimodal Logics in Simple Type TheoryLogica 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
-
101Comparing Approaches To Resolution Based Higher-Order Theorem ProvingSynthese 133 (1-2): 203-335. 2002.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
-
97Higher-order semantics and extensionalityJournal 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
-
75Computer 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
-
61Starting 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
-
49An 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.
-
37Cut-Elimination for Quantified Conditional LogicJournal 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.
-
37Multimodal and intuitionistic logics in simple type theoryLogic 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
-
29Mechanizing 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
-
25Lectures 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
-
24Automatic 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
-
23Jacques Herbrand: life, logic, and automated deductionIn Dov Gabbay (ed.), The Handbook of the History of Logic, Elsevier. pp. 195-254. 2009.
-
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
-
21Analysis 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.
-
21Combining and Automating Classical and Non-Classical Logics in Classical Higher-Order LogicAnnals of Mathematics and Artificial Intelligence) 62 (1-2): 103-128. 2011.
-
20Computer-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
-
17Sigma: An Integrated Development Environment for Formal OntologyAI Communications 26 (1): 79-97. 2013.
-
17Proof Step Analysis for Proof Tutoring -- A Learning Approach to GranularityTeaching Mathematics and Computer Science 6 (2): 325-343. 2008.
-
15Can 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.
-
15Assertion-level Proof Representation with Under-SpecificationElectronic Notes in Theoretical Computer Science 93 5-23. 2004.
-
15Sweet SIXTEEN: Automation via Embedding into Classical Higher-Order LogicLogic and Logical Philosophy 25 (4): 535-554. 2016.
Zehnruthenplan, Brandenburg, Germany
Areas of Specialization
Metaphysics and Epistemology |
Science, Logic, and Mathematics |
Areas of Interest
Metaphysics and Epistemology |
Science, Logic, and Mathematics |