48 found
Order:
See also
Christoph Benzmueller
Freie Universität Berlin
  1.  27
    Computer Science and Metaphysics: A Cross-Fertilization.Edward N. Zalta, Christoph Benzmüller & Daniel Kirchner - 2019 - Open Philosophy 2 (1):230-251.
    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 of computer science, since the new computational techniques that led to (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  2.  15
    The Higher-Order Prover LEO-II.Christoph Benzmüller, Nik Sultana, Lawrence C. Paulson & Frank Theiß - 2015 - Journal of Automated Reasoning 55 (4):389-404.
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark   5 citations  
  3. Quantified Multimodal Logics in Simple Type Theory.Christoph Benzmüller & Lawrence C. Paulson - 2013 - Logica Universalis 7 (1):7-20.
    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.
    Direct download (7 more)  
     
    Export citation  
     
    Bookmark   6 citations  
  4. Higher-Order Semantics and Extensionality.Christoph Benzmüller, Chad E. Brown & Michael Kohlhase - 2004 - Journal of Symbolic Logic 69 (4):1027 - 1088.
    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-order calculi with respect to these model classes.
    Direct download (8 more)  
     
    Export citation  
     
    Bookmark   13 citations  
  5.  13
    Mechanizing Principia Logico-Metaphysica in Functional Type Theory.Daniel Kirchner, Christoph Benzmüller & Edward N. Zalta - 2019 - Review of Symbolic Logic:1-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 deeply-rooted and known paradox is reintroduced in AOT when the logic of complex terms (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  6.  27
    Cut-Elimination for Quantified Conditional Logic.Christoph Benzmüller - 2017 - Journal of Philosophical Logic 46 (3):333-353.
    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.
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  7.  18
    Mechanizing Principia Logico-Metaphysica in Functional Type-Theory.Daniel Kirchner, Christoph Benzmüller & Edward N. Zalta - 2020 - Review of Symbolic Logic 13 (1):206-218.
    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-rooted and known paradox is reintroduced in AOT when the logic of complex terms is (...)
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  8.  84
    Mechanizing Principia Logico-Metaphysica in Functional Type Theory.Daniel Kirchner, Christoph Benzmüller & Edward N. Zalta - manuscript
    *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 Isabelle/HOL. Initial experiments within this framework reveal a crucial but overlooked fact: a (...)
    Direct download (4 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  9.  8
    Can Computers Help to Sharpen Our Understanding of Ontological Arguments?Christoph Benzmüller & David Fuenmayor - 2018 - In Mathematics and Reality, Proceedings of the 11th All India Students' Conference on Science Spiritual Quest, 6-7 October, 2018, IIT Bhubaneswar, Bhubaneswar, India. India: The Bhaktivedanta Institute. pp. 195226.
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  10.  8
    Analysis of an Ontological Proof Proposed by Leibniz.Matthias Bentert, Christoph Benzmüller, David Streit & Bruno Woltzenlogel Paleo - 2016 - In Charles Tandy (ed.), Death and Anti-Death, Volume 14: Four Decades After Michael Polanyi, Three Centuries After G.W. Leibniz. Ria University Press.
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark   2 citations  
  11.  7
    Embedding and Automating Conditional Logics in Classical Higher-Order Logic.Christoph Benzmüller, Dov Gabbay, Valerio Genovese & Daniele Rispoli - 2012 - Annals of Mathematics and Artificial Intelligence 66 (1-4):257-271.
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark   4 citations  
  12.  11
    Combining and Automating Classical and Non-Classical Logics in Classical Higher-Order Logic.Christoph Benzmüller - 2011 - Annals of Mathematics and Artificial Intelligence) 62 (1-2):103-128.
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark   4 citations  
  13.  16
    Computational Metaphysics: New Insights on Gödel's Ontological Argument and Modal Collapse.Christoph Benzmüller - unknown
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  14.  75
    Comparing Approaches To Resolution Based Higher-Order Theorem Proving.Christoph Benzmüller - 2002 - Synthese 133 (1):203-335.
    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 parallels and differences of the extensionality treatment of these approachesand demonstrate that extensional higher-order resolution is the sole approach thatcan completely avoid additional (...)
    Direct download (6 more)  
     
    Export citation  
     
    Bookmark   3 citations  
  15. Experiments in Computational Metaphysics: Gödel’s Proof of God’s Existence.Christoph Benzmüller & Bruno Woltzenlogel Paleo - 2017 - Savijnanam: Scientific Exploration for a Spiritual Paradigm. Journal of the Bhaktivedanta Institute 9:43-57.
    No categories
     
    Export citation  
     
    Bookmark   1 citation  
  16.  9
    Assertion-Level Proof Representation with Under-Specification.Serge Autexier, Christoph Benzmüller, Armin Fiedler, Helmut Horacek & Bao Quoc Vo - 2004 - Electronic Notes in Theoretical Computer Science 93:5-23.
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark   5 citations  
  17.  9
    Sweet SIXTEEN: Automation Via Embedding Into Classical Higher-Order Logic.Alexander Steen & Christoph Benzmüller - 2016 - Logic and Logical Philosophy 25 (4):535-554.
    Direct download  
     
    Export citation  
     
    Bookmark   1 citation  
  18.  8
    Automated Reasoning with Complex Ethical Theories--A Case Study Towards Responsible AI.David Fuenmayor & Christoph Benzmüller - unknown
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark  
  19.  7
    Computer Supported Mathematics with Ωmega.Jörg Siekmann, Christoph Benzmüller & Serge Autexier - 2006 - Journal of Applied Logic 4 (4):533-559.
  20.  13
    Proof Step Analysis for Proof Tutoring -- A Learning Approach to Granularity.Marvin Schiller, Dominik Dietrich & Christoph Benzmüller - 2008 - Teaching Mathematics and Computer Science 6 (2):325-343.
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark   2 citations  
  21.  31
    Formalisation and Evaluation of Alan Gewirth's Proof for the Principle of Generic Consistency in Isabelle/HOL.David Fuenmayor & Christoph Benzmüller - unknown
    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.
    Direct download  
     
    Export citation  
     
    Bookmark  
  22.  2
    Computer-Supported Analysis of Positive Properties, Ultrafilters and Modal Collapse in Variants of Gödel's Ontological Argument.Christoph Benzmüller & David Fuenmayor - 2020 - Bulletin of the Section of Logic 49 (2).
    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 analysis is the utilization of (...)
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  23.  9
    Combined Reasoning by Automated Cooperation.Christoph Benzmüller, Volker Sorge, Mateja Jamnik & Manfred Kerber - 2008 - Journal of Applied Logic 6 (3):318-342.
    Direct download (5 more)  
     
    Export citation  
     
    Bookmark   2 citations  
  24.  6
    Natural Language Dialog with a Tutor System for Mathematical Proofs.Christoph Benzmüller, Helmut Horacek, Ivana Kruijff-Korbayova, Manfred Pinkal, Jörg Siekmann & Magdalena Wolska - 2007 - In Ruqian Lu, Jörg Siekmann & Carsten Ullrich (eds.), Cognitive Systems. Springer. pp. 1-14.
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark   2 citations  
  25.  41
    Axiomatizing Category Theory in Free Logic.Christoph Benzmüller & Dana Scott - manuscript
    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 automated reasoning tools integrated with Isabelle/HOL. We also address the (...)
    Direct download  
     
    Export citation  
     
    Bookmark  
  26.  8
    Sigma: An Integrated Development Environment for Formal Ontology.Adam Pease & Christoph Benzmüller - 2013 - AI Communications 26 (1):79-97.
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark   1 citation  
  27.  3
    The Curious Inference of Boolos in MIZAR and OMEGA.Christoph Benzmüller & Chad Brown - 2007 - In Roman Matuszewski & Anna Zalewska (eds.), From Insight to Proof -- Festschrift in Honour of Andrzej Trybulec. The University of Bialystok, Polen. pp. 299-388.
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark   2 citations  
  28.  7
    Interactive Theorem Proving with Tasks.Malte Hübner, Serge Autexier, Christoph Benzmüller & Andreas Meier - 2004 - Electronic Notes in Theoretical Computer Science 103 (C):161-181.
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark   2 citations  
  29.  8
    Agent Based Mathematical Reasoning.Christoph Benzmüller, Mateja Jamnik, Manfred Kerber & Volker Sorge - 1999 - Electronic Notes in Theoretical Computer Science, Elsevier 23 (3):21-33.
    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.
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark   2 citations  
  30.  20
    Automatic Learning of Proof Methods in Proof Planning.Mateja Jamnik, Manfred Kerber, Martin Pollet & Christoph Benzmüller - 2003 - Logic Journal of the IGPL 11 (6):647-673.
    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 approach within the ΩMEGA proof planning system, which we call (...)
    Direct download (3 more)  
     
    Export citation  
     
    Bookmark   1 citation  
  31.  5
    Organisation, Transformation, and Propagation of Mathematical Knowledge in Omega.Serge Autexier, Christoph Benzmüller, Dominik Dietrich & Marc Wagner - 2008 - Mathematics in Computer Science 2 (2):253-277.
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark   1 citation  
  32.  8
    Bridging Theorem Proving and Mathematical Knowledge Retrieval.Christoph Benzmüller, Andreas Meier & Volker Sorge - 2004 - In Dieter Hutter & Werner Stephan (eds.), Mechanizing Mathematical Reasoning: Essays in Honor of Jörg Siekmann on the Occasion of His 60th Birthday. Springer. pp. 277-296.
    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 to adjust for a (...)
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark   1 citation  
  33.  4
    Integrating TPS and OMEGA.Christoph Benzmüller, Matt Bishop & Volker Sorge - 1999 - Journal of Universal Computer Science 5 (3):188-207.
    This paper reports on the integration of the higher-order theorem proving environment TPS [Andrews96] into the mathematical assistant OMEGA [Omega97]. TPS can be called from OMEGA either as a black box or as an interactive system. In black box mode, the user has control over the parameters which control proof search in TPS; in interactive mode, all features of the TPS-system are available to the user. If the subproblem which is passed to TPS contains concepts defined in OMEGA’s database of (...)
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark   1 citation  
  34.  8
    Computational Hermeneutics: Using Computers to Interpret Philosophical Arguments.David Fuenmayor & Christoph Benzmüller - unknown
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  35.  3
    Computational Metaphysics.Christoph Benzmüller, Max Wisniewski & Alexander Steen - unknown
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark  
  36.  8
    Higher-Order Aspects and Context in SUMO.Christoph Benzmüller & Adam Pease - 2012 - Journal of Web Semantics 12:104-117.
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark  
  37.  15
    Jacques Herbrand: Life, Logic, and Automated Deduction.Claus-Peter Wirth, Jörg Siekmann, Christoph Benzmüller & Serge Autexier - 2009 - In Dov Gabbay (ed.), The Handbook of the History of Logic. Elsevier. pp. 195-254.
  38.  5
    Editorial: Towards Computer Aided Mathematics.Christoph Benzmüller - 2006 - Journal of Applied Logic 4 (4):359-365.
    Direct download  
     
    Export citation  
     
    Bookmark  
  39.  5
    Omega.Christoph Benzmüller, Armin Fiedler, Andreas Meier, Martin Pollet & Jörg Siekmann - 2006 - In Freek Wiedijk (ed.), The Seventeen Provers of the World. Springer. pp. 127-141.
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark  
  40.  5
    Verifying the Modal Logic Cube is an Easy Task.Christoph Benzmüller - 2010 - In Simon Siegler & Nathan Wasser (eds.), Verification, Induction, Termination Analysis - Festschrift for Christoph Walther on the Occasion of His 60th Birthday. Springer. pp. 117-128.
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark  
  41.  1
    A Computational-Hermeneutic Approach for Conceptual Explicitation.Christoph Benzmüller & David Fuenmayor - 2019 - In Matthieu Fontaine, Cristina Barés-Gómez, Francisco Salguero-Lamillar, Lorenzo Magnani & Ángel Nepomuceno-Fernández (eds.), Model-Based Reasoning in Science and Technology. Springer Verlag.
    We present a computer-supported approach for the logical analysis and conceptual explicitation of argumentative discourse. Computational hermeneutics harnesses recent progresses in automated reasoning for higher-order logics and aims at formalizing natural-language argumentative discourse using flexible combinations of expressive non-classical logics. In doing so, it allows us to render explicit the tacit conceptualizations implicit in argumentative discursive practices. Our approach operates on networks of structured arguments and is iterative and two-layered. At one layer we search for logically correct formalizations for each (...)
    No categories
    Direct download (2 more)  
     
    Export citation  
     
    Bookmark  
  42.  7
    Towards Computer Aided Mathematics.Christoph Benzmüller - 2006 - Journal of Applied Logic 4 (4):359-365.
  43.  4
    Preface: Proceedings of the 8th Workshop on User Interfaces for Theorem Provers.Serge Autexier & Christoph Benzmüller - 2009 - Electronic Notes in Theoretical Computer Science 226 (1):1-2.
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark  
  44.  3
    Cumulative Habilitation Script.Christoph Benzmüller - 2006 - Saarland University, Germany.
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark  
  45. Reasoning in Simple Type Theory — Festschrift in Honor of Peter B. Andrews on His 70th Birthday, Studies in Logic, Vol. 17. [REVIEW]Christoph Benzmüller, Chad E. Brown, Jörg Siekmann & Richard Statman - 2010 - Bulletin of Symbolic Logic 16 (3):409-411.
  46.  2
    The Calculemus Final Report.Christoph Benzmüller & Corinna Hahn - 2004 - Saarland University, Germany.
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark  
  47.  1
    The Calculemus Midterm Report.Christoph Benzmüller & Corinna Hahn (eds.) - 2003 - Saarland University, Germany.
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark  
  48.  18
    Lectures on Jacques Herbrand as a Logician.Claus-Peter Wirth, Jörg Siekmann, Christoph Benzmüller & Serge Autexier - 2009 - Seki Publications (Issn 1437-4447).
    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 to the Loewenheim-Skolem-Theorem, we carefully investigate Herbrand’s (...)
    No categories
    Direct download  
     
    Export citation  
     
    Bookmark