References of "Benzmüller, Christoph 50026622"
     in
Bookmark and Share    
Full Text
Peer Reviewed
See detailFormalisation and Evaluation of Alan Gewirth's Proof for the Principle of Generic Consistency in Isabelle/HOL
Fuenmayor, David; Benzmüller, Christoph UL

in Archive of Formal Proofs (2018)

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 ... [more ▼]

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. [less ▲]

Detailed reference viewed: 83 (0 UL)
Full Text
See detailRecent Successes with a Meta-Logical Approach to Universal Logical Reasoning (Extended Abstract)
Benzmüller, Christoph UL

in Benzmüller, Christoph (Ed.) Formal Methods: Foundations and Applications - 20th Brazilian Symposium SBMF 2017, Recife, Brazil, November 29 - December 1, 2017, Proceedings (2017, November 11)

The quest for a most general framework supporting universal reasoning is very prominently represented in the works of Leibniz. He envisioned a scientia generalis founded on a characteristica universalis ... [more ▼]

The quest for a most general framework supporting universal reasoning is very prominently represented in the works of Leibniz. He envisioned a scientia generalis founded on a characteristica universalis, that is, a most universal formal language in which all knowledge about the world and the sciences can be encoded. A quick study of the survey literature on logical formalisms suggests that quite the opposite to Leibniz’ dream has become reality. Instead of a characteristica universalis, we are today facing a very rich and heterogenous zoo of different logical systems, and instead of converging towards a single superior logic, this logic zoo is further expanding, eventually even at accelerated pace. As a consequence, the unified vision of Leibniz seems farther away than ever before. However, there are also some promising initiatives to counteract these diverging developments. Attempts at unifying approaches to logic include categorial logic algebraic logic and coalgebraic logic. [less ▲]

Detailed reference viewed: 151 (5 UL)
Full Text
See detailMechanizing Principia Logico-Metaphysica in Functional Type Theory
Kirchner, Daniel; Benzmüller, Christoph UL; Zalta, Edward N.

E-print/Working paper (2017)

Principia Logico-Metaphysica proposes a foundational logical theory for metaphysics, mathematics, and the sciences. It contains a canonical development of Abstract Object Theory [AOT], a metaphysical ... [more ▼]

Principia Logico-Metaphysica proposes 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. [less ▲]

Detailed reference viewed: 94 (3 UL)
See detailGCAI 2017: 3rd Global Conference on Artificial Intelligence, Miami, FL, USA, 18-22 October 2017
Benzmüller, Christoph UL; Lisetti, Christine; Theobald, Martin UL

Book published by EPiC Series in Computing, EasyChair (2017)

Detailed reference viewed: 119 (16 UL)
See detailGCAI 2017. 3rd Global Conference on Artificial Intelligence
Benzmüller, Christoph UL; Lisetti, Christine; Theobald, Martin

Book published by EasyChair Proceedings (2017)

Detailed reference viewed: 57 (6 UL)
Full Text
Peer Reviewed
See detailComputer-assisted Reconstruction and Assessment of E. J. Lowe's Modal Ontological Argument
Benzmüller, Christoph UL; Fuenmayor, David

in Archive of Formal Proofs (2017)

Computers may help us to understand --not just verify-- philosophical arguments. By utilizing modern proof assistants in an iterative interpretive process, we can reconstruct and assess an argument by ... [more ▼]

Computers may help us to understand --not just verify-- philosophical arguments. By utilizing modern proof assistants in an iterative interpretive process, we can reconstruct and assess an argument by fully formal means. Through the mechanization of a variant of St. Anselm's ontological argument by E. J. Lowe, which is a paradigmatic example of a natural-language argument with strong ties to metaphysics and religion, we offer an ideal showcase for our computer-assisted interpretive method. [less ▲]

Detailed reference viewed: 64 (1 UL)
Full Text
Peer Reviewed
See detailAutomating Emendations of the Ontological Argument in Intensional Higher-Order Modal Logic
Fuenmayor, David; Benzmüller, Christoph UL

in KI 2017: Advances in Artificial Intelligence 40th Annual German Conference on AI (2017, September)

A shallow semantic embedding of an intensional higher-order modal logic (IHOML) in Isabelle/HOL is presented. IHOML draws on Montague/Gallin intensional logics and has been introduced by Melvin Fitting in ... [more ▼]

A shallow semantic embedding of an intensional higher-order modal logic (IHOML) in Isabelle/HOL is presented. IHOML draws on Montague/Gallin intensional logics and has been introduced by Melvin Fitting in his textbook Types, Tableaus and Gödel’s God in order to discuss his emendation of Gödel’s ontological argument for the existence of God. Utilizing IHOML, the most interesting parts of Fitting’s textbook are formalized, automated and verified in the Isabelle/HOL proof assistant. A particular focus thereby is on three variants of the ontological argument which avoid the modal collapse, which is a strongly criticized side-effect in Gödel’s resp. Scott’s original work. [less ▲]

Detailed reference viewed: 118 (6 UL)
Full Text
See detailImplementation of Carmo and Jones Dyadic Deontic Logic in Isabelle/HOL
Benzmüller, Christoph UL; Farjami, Ali UL; Parent, Xavier UL et al

Scientific Conference (2017, July 06)

A shallow semantical embedding of a dyadic deontic logic (by Carmo and Jones) in Isabelle/HOL is presented. First experiments provide evidence that this logic implementation fruitfully enables interactive ... [more ▼]

A shallow semantical embedding of a dyadic deontic logic (by Carmo and Jones) in Isabelle/HOL is presented. First experiments provide evidence that this logic implementation fruitfully enables interactive and automated reasoning at the meta-level the object-level. [less ▲]

Detailed reference viewed: 138 (19 UL)
Full Text
Peer Reviewed
See detailCapability Discovery for Automated Reasoning Systems
Steen, Alexander UL; Wisniewski, Max; Schurr, Hans-Jörg et al

in IWIL Workshop and LPAR Short Presentations (2017, June 04)

Automated reasoning systems such as theorem provers often employ interaction or cooperation with further reasoning software. Whereas in most cases the concrete choice of cooperating software is, to some ... [more ▼]

Automated reasoning systems such as theorem provers often employ interaction or cooperation with further reasoning software. Whereas in most cases the concrete choice of cooperating software is, to some extent, irrelevant, these systems are nevertheless often rigid in practice due to compatibility issues. In order to support more flexible cooperation schemes, a machine-readable description format for automated reasoning systems' capabilities is proposed. Additionally, a simple HTTP-based protocol for system and capability discovery is outlined. Both the format and the protocol are designed to be simple, extensible and easy to use with none to minor modifications for existing reasoning systems. [less ▲]

Detailed reference viewed: 91 (2 UL)
Full Text
Peer Reviewed
See detailLeo-III Version 1.1 (System description)
Benzmüller, Christoph UL; Steen, Alexander UL; Wisniewski, Max

in IWIL Workshop and LPAR Short Presentations (2017, June 04)

Leo-III is an automated theorem prover for (polymorphic) higher-order logic which supports all common TPTP dialects, including THF, TFF and FOF as well as their rank-1 polymorphic derivatives. It is based ... [more ▼]

Leo-III is an automated theorem prover for (polymorphic) higher-order logic which supports all common TPTP dialects, including THF, TFF and FOF as well as their rank-1 polymorphic derivatives. It is based on a paramodulation calculus with ordering constraints and, in tradition of its predecessor LEO-II, heavily relies on cooperation with external first-order theorem provers. Unlike LEO-II, asynchronous cooperation with typed first-order provers and an agent-based internal cooperation scheme is supported. In this paper, we sketch Leo-III's underlying calculus, survey implementation details and give examples of use. [less ▲]

Detailed reference viewed: 90 (3 UL)
Full Text
Peer Reviewed
See detailGoing Polymorphic - TH1 Reasoning for Leo-III
Steen, Alexander UL; Wisniewski, Max; Benzmüller, Christoph UL

in IWIL Workshop and LPAR Short Presentations (2017, June 04)

While interactive proof assistants for higher-order logic (HOL) commonly admit reasoning within rich type systems, current theorem provers for HOL are mainly based on simply typed lambda-calculi and ... [more ▼]

While interactive proof assistants for higher-order logic (HOL) commonly admit reasoning within rich type systems, current theorem provers for HOL are mainly based on simply typed lambda-calculi and therefore do not allow such flexibility. In this paper, we present modifications to the higher-order automated theorem prover Leo-III for turning it into a reasoning system for rank-1 polymorphic HOL. To that end, a polymorphic version of HOL and a suitable paramodulation-based calculus are sketched. The implementation is evaluated using a set of polymorphic TPTP THF problems. [less ▲]

Detailed reference viewed: 79 (4 UL)
Full Text
Peer Reviewed
See detailTheorem Provers for Every Normal Modal Logic
Gleißner, Tobias; Steen, Alexander UL; Benzmüller, Christoph UL

in Eiter, Thomas; Sands, David (Eds.) LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning (2017, May 04)

We present a procedure for algorithmically embedding problems formulated in higher- order modal logic into classical higher-order logic. The procedure was implemented as a stand-alone tool and can be used ... [more ▼]

We present a procedure for algorithmically embedding problems formulated in higher- order modal logic into classical higher-order logic. The procedure was implemented as a stand-alone tool and can be used as a preprocessor for turning TPTP THF-compliant the- orem provers into provers for various modal logics. The choice of the concrete modal logic is thereby specified within the problem as a meta-logical statement. This specification for- mat as well as the underlying semantics parameters are discussed, and the implementation and the operation of the tool are outlined. By combining our tool with one or more THF-compliant theorem provers we accomplish the most widely applicable modal logic theorem prover available to date, i.e. no other available prover covers more variants of propositional and quantified modal logics. Despite this generality, our approach remains competitive, at least for quantified modal logics, as our experiments demonstrate. [less ▲]

Detailed reference viewed: 101 (2 UL)
Full Text
Peer Reviewed
See detailTypes, Tableaus and Gödel's God in Isabelle/HOL
Fuenmayor, David; Benzmüller, Christoph UL

in Archive of Formal Proofs (2017)

A computer-formalisation of the essential parts of Fitting's textbook "Types, Tableaus and Gödel's God" in Isabelle/HOL is presented. In particular, Fitting's (and Anderson's) variant of the ontological ... [more ▼]

A computer-formalisation of the essential parts of Fitting's textbook "Types, Tableaus and Gödel's God" in Isabelle/HOL is presented. In particular, Fitting's (and Anderson's) variant of the ontological argument is verified and confirmed. This variant avoids the modal collapse, which has been criticised as an undesirable side-effect of Kurt Gödel's (and Dana Scott's) versions of the ontological argument. Fitting's work is employing an intensional higher-order modal logic, which we shallowly embed here in classical higher-order logic. We then utilize the embedded logic for the formalisation of Fitting's argument. (See also the earlier AFP entry ``Gödel's God in Isabelle/HOL''.) [less ▲]

Detailed reference viewed: 61 (2 UL)
See detailUniversal Reasoning, Rational Argumentation and Human-Machine Interaction
Benzmüller, Christoph UL

E-print/Working paper (2017)

Classical higher-order logic, when utilized as a meta-logic in which various other (classical and non-classical) logics can be shallowly embedded, is well suited for realising a universal logic reasoning ... [more ▼]

Classical higher-order logic, when utilized as a meta-logic in which various other (classical and non-classical) logics can be shallowly embedded, is well suited for realising a universal logic reasoning approach. Universal logic reasoning in turn, as envisioned already by Leibniz, may support the rigorous formalisation and deep logical analysis of rational arguments within machines. A respective universal logic reasoning framework is described and a range of exemplary applications are discussed. In the future, universal logic reasoning in combination with appropriate, controlled forms of rational argumentation may serve as a communication layer between humans and intelligent machines. [less ▲]

Detailed reference viewed: 43 (3 UL)
Full Text
Peer Reviewed
See detailComputer-Assisted Analysis of the Anderson-Hájek Controversy
Benzmüller, Christoph UL; Weber, Leon; Woltzenlogel Paleo, Bruno

in Logica Universalis (2017), 11(1), 139-151

A universal reasoning approach based on shallow semantical embeddings of higher-order modal logics into classical higher-order logic is exemplarily employed to analyze several modern variants of the ... [more ▼]

A universal reasoning approach based on shallow semantical embeddings of higher-order modal logics into classical higher-order logic is exemplarily employed to analyze several modern variants of the ontological argument on the computer. Several novel findings are reported which contribute to the clarification of a long-standing dispute between Anderson and Hájek. The technology employed in this work, which to some degree realizes Leibniz’s dream of a characteristica universalis and a calculus ratiocinator for solving philosophical controversies, is ready to be fruitfully adopted in larger scale by philosophers. [less ▲]

Detailed reference viewed: 20 (0 UL)
Full Text
Peer Reviewed
See detailExperiments in Computational Metaphysics: Gödel's Proof of God's Existence
Benzmüller, Christoph UL; Woltzenlogel Paleo, Bruno

in Savijnanam: scientific exploration for a spiritual paradigm. Journal of the Bhaktivedanta Institute (2017), 9

“Computer scientists prove the existence of God” --- variants of this headline appeared in the international press in autumn 2013. Unfortunately, many media reports had only moderate success in ... [more ▼]

“Computer scientists prove the existence of God” --- variants of this headline appeared in the international press in autumn 2013. Unfortunately, many media reports had only moderate success in communicating to the wider public what had actually been achieved and what not. This article outlines the main findings of the authors’ joint work in computational metaphysics. More precisely, the article focuses on their computer-supported analysis of variants and recent emendations of Kurt Gödel’s modern ontological argument for the existence of God. In the conducted experiments, automated theorem provers discovered some interesting and relevant facts. [less ▲]

Detailed reference viewed: 202 (1 UL)
Full Text
Peer Reviewed
See detailCut-Elimination for Quantified Conditional Logic
Benzmüller, Christoph UL

in Journal of Philosophical Logic (2017), 46(3), 333353

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 ... [more ▼]

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. [less ▲]

Detailed reference viewed: 88 (0 UL)
Full Text
Peer Reviewed
See detailThe Virtues of Automated Theorem Proving in Metaphysics --- A Case Study: E. J. Lowe's Modal Ontological Argument
Fuenmayor, David; Benzmüller, Christoph UL; Steen, Alexander UL et al

in The 2nd World Congress on Logic and Religion -- Book of Abstracts (2017)

Detailed reference viewed: 81 (2 UL)
Full Text
Peer Reviewed
See detailTPTP and Beyond: Representation of Quantified Non-Classical Logics
Wisniewski, Max; Steen, Alexander UL; Benzmüller, Christoph UL

in Benzmüller, Christoph; Otten, Jens (Eds.) ARQNL 2016. Automated Reasoning in Quantified Non-Classical Logics (2016, December)

Detailed reference viewed: 22 (0 UL)
Full Text
Peer Reviewed
See detailTutorial on Reasoning in Expressive Non-Classical Logics with Isabelle/HOL
Steen, Alexander UL; Wisniewski, Max; Benzmüller, Christoph UL

in Benzmüller, Christoph; Sutcliffe, Geoff; Rojas, Raul (Eds.) GCAI 2016, 2nd Global Conference on Artificial Intelligence (2016, September 29)

Detailed reference viewed: 45 (0 UL)