
311Computers may help us to better understand (not just verify) arguments. In this article we defend this claim by showcasing the application of a new, computerassisted interpretive method to an exemplary naturallanguage 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 interactiveautomated proof ass…Read more

148HigherOrder Semantics and ExtensionalityJournal of Symbolic Logic 69 (4). 2004.In this paper we reexamine the semantics of classical higherorder logic with the purpose of clarifying the role of extensionality. To reach this goal, we distinguish nine classes of higherorder 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 (machineoriented) higherord…Read more

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

88Higherorder semantics and extensionalityJournal of Symbolic Logic 69 (4): 10271088. 2004.In this paper we reexamine the semantics of classical higherorder logic with the purpose of clarifying the role of extensionality. To reach this goal, we distinguish nine classes of higherorder 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 higherorder calculi with respect to these model classes

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

75Comparing Approaches To Resolution Based HigherOrder Theorem ProvingSynthese 133 (1): 203335. 2002.We investigate several approaches to resolution based automated theoremproving in classical higherorder logic (based on Church's simply typedcalculus) and discuss their requirements with respect to Henkincompleteness and full extensionality. In particular we focus on Andrews'higherorder resolution (Andrews 1971), Huet's constrained resolution (Huet1972), higherorder Eresolution, and extensional higherorder resolution(Benzmüller and Kohlhase 1997). With the help of examples we illustratethe…Read more

41Starting 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 higherorder logic. The modeling and formal analysis of our axiom sets has been significantly supported by series of experiments with automate…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.

27CutElimination for Quantified Conditional LogicJournal of Philosophical Logic 46 (3): 333353. 2017.A semantic embedding of quantified conditional logic in classical higherorder logic is utilized for reducing cutelimination 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 cutelimination is still open. However, special attention has to be payed to cutsimulation, which may render cutelimination as a pointless criterion.

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

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

19Multimodal and intuitionistic logics in simple type theoryLogic Journal of the IGPL 18 (6): 881892. 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 nonclassical logics. We report some experiments using the higherorder automated theorem prover LEOII

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

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

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

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

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

11Combining and Automating Classical and NonClassical Logics in Classical HigherOrder LogicAnnals of Mathematics and Artificial Intelligence) 62 (12): 103128. 2011.

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

9Assertionlevel Proof Representation with UnderSpecificationElectronic Notes in Theoretical Computer Science 93 523. 2004.

8Bridging Theorem Proving and Mathematical Knowledge RetrievalIn Dieter Hutter & Werner Stephan (eds.), Mechanizing Mathematical Reasoning: Essays in Honor of Jörg Siekmann on the Occasion of His 60th Birthday, Springer. pp. 277296. 2004.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

8Agent based Mathematical ReasoningElectronic Notes in Theoretical Computer Science, Elsevier 23 (3): 2133. 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.

8Sigma: An Integrated Development Environment for Formal OntologyAI Communications 26 (1): 7997. 2013.
Zehnruthenplan, Brandenburg, Germany
Areas of Specialization
Metaphysics and Epistemology 
Science, Logic, and Mathematics 
Areas of Interest
Metaphysics and Epistemology 
Science, Logic, and Mathematics 