
2Computersupported 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 computersupported formal analysis presented in this article. Key to our formal an…Read more

18Mechanizing principia logicometaphysica in functional typetheoryReview of Symbolic Logic 13 (1): 206218. 2020.Principia LogicoMetaphysica 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

1A ComputationalHermeneutic Approach for Conceptual ExplicitationIn Matthieu Fontaine, Cristina BarésGómez, Francisco SalgueroLamillar, Lorenzo Magnani & Ángel NepomucenoFernández (eds.), ModelBased Reasoning in Science and Technology, Springer Verlag. 2019.We present a computersupported approach for the logical analysis and conceptual explicitation of argumentative discourse. Computational hermeneutics harnesses recent progresses in automated reasoning for higherorder logics and aims at formalizing naturallanguage argumentative discourse using flexible combinations of expressive nonclassical logics. In doing so, it allows us to render explicit the tacit conceptualizations implicit in argumentative discursive practices. Our approach operates on…Read more

27Computer Science and Metaphysics: A CrossFertilizationOpen Philosophy 2 (1): 230251. 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 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

13Mechanizing principia logicometaphysica in functional type theoryReview of Symbolic Logic 113. 2019.Principia LogicoMetaphysica 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

31An 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 LogicoMetaphysica* (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

18Lectures on Jacques Herbrand as a LogicianSeki Publications (Issn 14374447). 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 wellknown 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

13Proof Step Analysis for Proof Tutoring  A Learning Approach to GranularityTeaching Mathematics and Computer Science 6 (2): 325343. 2008.

9Sweet SIXTEEN: Automation via Embedding into Classical HigherOrder LogicLogic and Logical Philosophy 25 (4): 535554. 2016.

15Jacques Herbrand: life, logic, and automated deductionIn Dov Gabbay (ed.), The Handbook of the History of Logic, Elsevier. pp. 195254. 2009.

7Interactive Theorem Proving with TasksElectronic Notes in Theoretical Computer Science 103 (C): 161181. 2004.

20Automatic Learning of Proof Methods in Proof PlanningLogic Journal of the IGPL 11 (6): 647673. 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 wellchosen 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

8Sigma: An Integrated Development Environment for Formal OntologyAI Communications 26 (1): 7997. 2013.

5Verifying the Modal Logic Cube is an Easy TaskIn Simon Siegler & Nathan Wasser (eds.), Verification, Induction, Termination Analysis  Festschrift for Christoph Walther on the Occasion of His 60th Birthday, Springer. pp. 117128. 2010.

3The curious inference of Boolos in MIZAR and OMEGAIn Roman Matuszewski & Anna Zalewska (eds.), From Insight to Proof  Festschrift in Honour of Andrzej Trybulec, The University of Bialystok, Polen. pp. 299388. 2007.

Reasoning in simple type theory — Festschrift in honor of Peter B. Andrews on his 70th birthday, Studies in Logic, vol. 17 (review)Bulletin of Symbolic Logic 16 (3): 409411. 2010.

6Natural Language Dialog with a Tutor System for Mathematical ProofsIn Ruqian Lu, Jörg Siekmann & Carsten Ullrich (eds.), Cognitive Systems, Springer. pp. 114. 2007.

118Quantified Multimodal Logics in Simple Type TheoryLogica Universalis 7 (1): 720. 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 offtheshelf higherorder 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
Zehnruthenplan, Brandenburg, Germany
Areas of Specialization
Metaphysics and Epistemology 
Science, Logic, and Mathematics 
Areas of Interest
Metaphysics and Epistemology 
Science, Logic, and Mathematics 