References of "Benzmüller, Christoph 50026622"
     in
Bookmark and Share    
Full Text
Peer Reviewed
See detailAutomating Free Logic in HOL, with an Experimental Application in Category Theory
Benzmüller, Christoph UL; Scott, Dana

in Journal of Automated Reasoning (2019)

A shallow semantical embedding of free logic in classical higher-order logic is presented, which enables the off-the-shelf application of higher-order interactive and automated theorem provers for the ... [more ▼]

A shallow semantical embedding of free logic in classical higher-order logic is presented, which enables the off-the-shelf application of higher-order interactive and automated theorem provers for the formalisation andverification of free logic theories. Subsequently, this approach is applied to aselected domain of mathematics: starting from a generalization of the standardaxioms for a monoid we present a stepwise development of various, mutuallyequivalent foundational axiom systems for category theory. As a side-effect ofthis work some (minor) issues in a prominent category theory textbook havebeen revealed.The purpose of this article is not to claim any novel results in category the-ory, but to demonstrate an elegant way to “implement” and utilize interactiveand automated reasoning in free logic, and to present illustrative experiments. [less ▲]

Detailed reference viewed: 26 (0 UL)
Full Text
Peer Reviewed
See detailUniversal (Meta-)Logical Reasoning: Recent Successes
Benzmüller, Christoph UL

in Science of Computer Programming (2018)

Classical higher-order logic, when utilized as a meta-logic in which various other (classical and non-classical) logics can be shallowly embedded, is suitable as a foundation for the development of a ... [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 suitable as a foundation for the development of a universal logical reasoning engine. Such an engine may be employed, as already envisioned by Leibniz, to support the rigorous formalisation and deep logical analysis of rational arguments on the computer. A respective universal logical reasoning framework is described in this article and a range of successful first applications in philosophy, artificial intelligence and mathematics are surveyed. [less ▲]

Detailed reference viewed: 33 (0 UL)
Full Text
See detailI/O Logic in HOL
Farjami, Ali UL; Meder, Paul Joseph Yves UL; Parent, Xavier UL et al

Scientific Conference (2018, September 17)

A shallow semantical embedding of Input/Output logic in classical higher-order logic is presented, and shown to be faithful (sound an complete). This embedding has been implemented in the higher-order ... [more ▼]

A shallow semantical embedding of Input/Output logic in classical higher-order logic is presented, and shown to be faithful (sound an complete). This embedding has been implemented in the higher-order proof assistant Isabelle/HOL. We provide an empirical regulative framework for assessing General Data Protection Regulation. [less ▲]

Detailed reference viewed: 50 (15 UL)
Full Text
Peer Reviewed
See detailAqvist's Dyadic Deontic Logic E in HOL
Benzmüller, Christoph UL; Farjami, Ali UL; Parent, Xavier UL

Scientific Conference (2018, September 17)

We devise a shallow semantical embedding of \AA{}qvist's dyadic deontic logic {\bf E} in classical higher-order logic. This embedding is encoded in Isabelle/HOL, which turns this system into a proof ... [more ▼]

We devise a shallow semantical embedding of \AA{}qvist's dyadic deontic logic {\bf E} in classical higher-order logic. This embedding is encoded in Isabelle/HOL, which turns this system into a proof assistant for deontic logic reasoning. The experiments with this environment provide evidence that this logic \textit{implementation} fruitfully enables interactive and automated reasoning at the meta-level and the object-level. [less ▲]

Detailed reference viewed: 45 (13 UL)
Full Text
Peer Reviewed
See detailA Dyadic Deontic Logic in HOL
Benzmüller, Christoph UL; Farjami, Ali UL; Parent, Xavier UL

in Broersen, Jan; Condoravdi, Cleo; Nair, Shyam (Eds.) et al Deontic Logic and Normative Systems --- 14th International Conference, DEON 2018, Utrecht, The Netherlands, 3-6 July, 2018 (2018, June 11)

A shallow semantical embedding of a dyadic deontic logic by Carmo and Jones in classical higher-order logic is presented. This embedding is proven sound and complete, that is, faithful. The work presented ... [more ▼]

A shallow semantical embedding of a dyadic deontic logic by Carmo and Jones in classical higher-order logic is presented. This embedding is proven sound and complete, that is, faithful. The work presented here provides the theoretical foundation for the implementation and automation of dyadic deontic logic within off-the-shelf higher-order theorem provers and proof assistants. [less ▲]

Detailed reference viewed: 22 (11 UL)
Full Text
Peer Reviewed
See detailImplementation of Dyadic Deontic Logic E in Isabelle/HOL
Benzmüller, Christoph UL; Farjami, Ali UL; Parent, Xavier UL

Scientific Conference (2018, May 04)

We have devised a shallow semantical embedding of a dyadic deontic logic (by B.Hansson and \AA{}qvist) in classical higher-order logic. This embedding has been encoded in Isabelle/HOL, which turns this ... [more ▼]

We have devised a shallow semantical embedding of a dyadic deontic logic (by B.Hansson and \AA{}qvist) in classical higher-order logic. This embedding has been encoded in Isabelle/HOL, which turns this system into a proof assistant for deontic logic reasoning. The experiments with this environment provide evidence that this logic \textit{implementation} fruitfully enables interactive and automated reasoning at the meta-level and the object-level. [less ▲]

Detailed reference viewed: 29 (4 UL)
Full Text
See detailFaithful Semantical Embedding of a Dyadic Deontic Logic in HOL
Benzmüller, Christoph UL; Farjami, Ali UL; Parent, Xavier UL

Report (2018)

A shallow semantical embedding of a dyadic deontic logic by Carmo and Jones in classical higher-order logic is presented. This embedding is proven sound and complete, that is, faithful. The work presented ... [more ▼]

A shallow semantical embedding of a dyadic deontic logic by Carmo and Jones in classical higher-order logic is presented. This embedding is proven sound and complete, that is, faithful. The work presented here provides the theoretical foundation for the implementation and automation of dyadic deontic logic within off-the-shelf higher-order theorem provers and proof assistants. [less ▲]

Detailed reference viewed: 47 (5 UL)
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: 25 (0 UL)
Full Text
Peer Reviewed
See detailMechanizing Principia Logico-Metaphysica in Functional Type Theory (Extended Abstract)
Kirchner, Daniel; Benzmüller, Christoph UL; Zalta, Edward N.

in 3rd Conference on Artificial Intelligence and Theorem Proving (AITP 2018), Book of Abstracts (2018)

Detailed reference viewed: 12 (0 UL)
Full Text
Peer Reviewed
See detailAxiom Systems for Category Theory in Free Logic
Benzmüller, Christoph UL; Scott, Dana S.

in Archive of Formal Proofs (2018)

Detailed reference viewed: 20 (0 UL)
Full Text
Peer Reviewed
See detailSome Reflections on a Computer-aided Theory Exploration Study in Category Theory (Extended Abstract)
Benzmüller, Christoph UL; Scott, Dana S.

in 3rd Conference on Artificial Intelligence and Theorem Proving (AITP 2018), Book of Abstracts (2018)

Detailed reference viewed: 11 (0 UL)
Full Text
Peer Reviewed
See detailA Case Study On Computational Hermeneutics: E. J. Lowe's Modal Ontological Argument
Fuenmayor, David; Benzmüller, Christoph UL

in IfCoLog Journal of Logics and Their Applications (2018), 5(7), 1567-1603

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

Computers 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 argument 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 assistants. It aims at shedding light on the meanings of words and sentences by framing their inferential role in a given argument. By employing automated theorem reasoning technology within interactive proof assistants, we are able to drastically reduce (by several orders of magnitude) the time needed to test the logical validity of an argument’s formalization. As a result, a new approach to logical analysis, inspired by Donald Davidson’s account of radical interpretation, has been enabled. In computational hermeneutics, the utilization of automated reasoning tools effectively boosts our capacity to expose the assumptions we indirectly commit ourselves to every time we engage in rational argumentation and it fosters the explicitation and revision of our concepts and commitments. [less ▲]

Detailed reference viewed: 16 (0 UL)
Full Text
Peer Reviewed
See detailThe Higher-Order Prover Leo-III
Steen, Alexander UL; Benzmüller, Christoph UL

in Automated Reasoning 9th International Joint Conference, IJCAR 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings (2018)

Detailed reference viewed: 10 (1 UL)
Full Text
See detailCan Computers Help to Sharpen our Understanding of Ontological Arguments?
Benzmüller, Christoph UL; Fuenmayor, David

in Mathematics and Reality, Proceedings of the 11th All India Students' Conference on Science Spiritual Quest, 6-7 October, 2018, IIT Bhubaneswar, Bhubaneswar, India (2018)

Detailed reference viewed: 16 (0 UL)
Full Text
Peer Reviewed
See detailSystem Demonstration: The Higher-Order Prover Leo-III
Steen, Alexander; Benzmüller, Christoph UL

in CEUR Workshop Proceedings (2018), 2095

Detailed reference viewed: 9 (0 UL)
Full Text
Peer Reviewed
See detailComputational Hermeneutics: Using Computers to Interpret Philosophical Arguments (Abstract)
Fuenmayor, David; Benzmüller, Christoph UL

in Logical Correctness, Workshop at UNILOG'2018, UNILOG'2018 Book of Abstracts (2018)

Detailed reference viewed: 20 (0 UL)
See detailFirst Experiments with a Flexible Infrastructure for Normative Reasoning
Benzmüller, Christoph UL; Parent, Xavier UL

E-print/Working paper (2018)

A flexible infrastructure for normative reasoning is outlined. A small-scale demonstrator version of the envisioned system has been implemented in the proof assistant Isabelle/HOL by utilising the first ... [more ▼]

A flexible infrastructure for normative reasoning is outlined. A small-scale demonstrator version of the envisioned system has been implemented in the proof assistant Isabelle/HOL by utilising the first authors universal logical reasoning approach based on shallow semantical embeddings in meta-logic HOL. The need for such a flexible reasoning infrastructure is motivated and illustrated with a contrary-to-duty example scenario selected from the General Data Protection Regulation. [less ▲]

Detailed reference viewed: 17 (1 UL)
Full Text
Peer Reviewed
See detailARQNL 2018 Automated Reasoning in Quantified Non-Classical Logics
Benzmüller, Christoph UL; Otten, Jens

in CEUR Workshop Proceedings (2018), 2095

Detailed reference viewed: 14 (0 UL)