References of "Benzmüller, Christoph 50026622"
     in
Bookmark and Share    
Full Text
Peer Reviewed
See detailComputer Science and Metaphysics: A Cross-Fertilization
Kirchner, Daniel; Benzmüller, Christoph UL; Zalta, Edward N.

in Open Philosophy (2019), 2(1), 230251

omputational philosophy is the use of mechanized computational techniques to unearth philosophical insights that are either difficult or impossible to find using traditional philosophical methods ... [more ▼]

omputational 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 (a) develop results in modal metaphysics whose discovery was computer assisted, and (b) 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 these results may be more broadly applicable within computer science. The paper includes a description of our background methodology and how it evolved, and a discussion of our new results. [less ▲]

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

in Review of Symbolic Logic (2019)

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

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 (inspired by ideas of Ernst Mally, formalized by Zalta) 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 simply adjoined to AOT’s specially formulated comprehension principle for relations. This result constitutes a new and important paradox, given how much expressive and analytic power is contributed by having the two kinds of complex terms in the system. Its discovery is the highlight of our joint project and provides strong evidence for a new kind of scientific practice in philosophy, namely, computational metaphysics. Our results were made technically possible by a suitable adaptation of Benzmüller’s metalogical approach to universal reasoning by semantically embedding theories in classical higher-order logic. This approach enables one to reuse state-of-the-art higher-order proof assistants, such as Isabelle/HOL, for mechanizing and experimentally exploring challenging logics and theories such as AOT. Our results also provide a fresh perspective on the question of whether relational type theory or functional type theory better serves as a foundation for logic and metaphysics. [less ▲]

Detailed reference viewed: 13 (0 UL)
Full Text
Peer Reviewed
See detailUniversal (Meta-)Logical Reasoning: The Wise Men Puzzle (Isabelle/HOL Dataset)
Benzmüller, Christoph UL

in Data in Brief (2019), 24(103823), 1--5

The authors universal (meta-)logical reasoning approach is demonstrated and assessed with a prominent riddle in epistemic reasoning: the Wise Men Puzzle. The presented solution puts a particular emphasis ... [more ▼]

The authors universal (meta-)logical reasoning approach is demonstrated and assessed with a prominent riddle in epistemic reasoning: the Wise Men Puzzle. The presented solution puts a particular emphasis on the adequate modeling of common knowledge and it illustrates the elegance and the practical relevance of the shallow semantical embedding approach when utilized within modern proof assistant systems such as Isabelle/HOL. The contributed dataset provides supporting evidence for claims made in the article “Universal (meta-)logical reasoning: Recent successes” (Benzmüller, 2019). [less ▲]

Detailed reference viewed: 14 (0 UL)
Full Text
Peer Reviewed
See detailChurch's Type Theory
Benzmüller, Christoph UL; Andrews, Peter

in Stanford Encyclopedia of Philosophy (2019)

Church’s type theory, aka simple type theory, is a formal logical language which includes classical first-order and propositional logic, but is more expressive in a practical sense. It is used, with some ... [more ▼]

Church’s type theory, aka simple type theory, is a formal logical language which includes classical first-order and propositional logic, but is more expressive in a practical sense. It is used, with some modifications and enhancements, in most modern applications of type theory. It is particularly well suited to the formalization of mathematics and other disciplines and to specifying and verifying hardware and software. It also plays an important role in the study of the formal semantics of natural language. When utilizing it as a meta-logic to semantically embed expressive (quantified) non-classical logics further topical applications are enabled in artificial intelligence and philosophy. A great wealth of technical knowledge can be expressed very naturally in it. With possible enhancements, Church’s type theory constitutes an excellent formal language for representing the knowledge in automated information systems, sophisticated automated reasoning systems, systems for verifying the correctness of mathematical proofs, and a range of projects involving logic and artificial intelligence. Some examples and further references are given in Sections 1.2.2 and 5 below. Type theories are also called higher-order logics, since they allow quantification not only over individual variables (as in first-order logic), but also over function, predicate, and even higher order variables. Type theories characteristically assign types to entities, distinguishing, for example, between numbers, sets of numbers, functions from numbers to sets of numbers, and sets of such functions. As illustrated in Section 1.2.2 below, these distinctions allow one to discuss the conceptually rich world of sets and functions without encountering the paradoxes of naive set theory. Church’s type theory is a formulation of type theory that was introduced by Alonzo Church in Church 1940. In certain respects, it is simpler and more general than the type theory introduced by Bertrand Russell in Russell 1908 and Whitehead & Russell 1927a. Since properties and relations can be regarded as functions from entities to truth values, the concept of a function is taken as primitive in Church’s type theory, and the λ-notation which Church introduced in Church 1932 and Church 1941 is incorporated into the formal language. Moreover, quantifiers and description operators are introduced in a way so that additional binding mechanisms can be avoided, λ-notation is reused instead. λ-notation is thus the only binding mechanism employed in Church’s type theory. [less ▲]

Detailed reference viewed: 16 (0 UL)
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: 85 (1 UL)
Full Text
See detailKI 2019: Advances in Artificial Intelligence -- 42nd German Conference on AI, Kassel, Germany, September 23-26, 2019, Proceedings
Benzmüller, Christoph UL; Stuckenschmidt, Heiner

Book published by Springer, Cham, Cham (2019)

This volume contains the papers presented at the 42nd German Conference on Artificial Intelligence (KI 2019), held during September 23–26, 2019, in Kassel, Germany. The German conference on Artificial ... [more ▼]

This volume contains the papers presented at the 42nd German Conference on Artificial Intelligence (KI 2019), held during September 23–26, 2019, in Kassel, Germany. The German conference on Artificial Intelligence (abbreviated KI for “Künstliche Intelligenz”) has developed from a series of inofficial meetings and workshops, organized by the German “Gesellschaft für Informatik” (association for computer science, GI), into an annual conference series dedicated to research on theory and applications of intelligent system technology. While KI is primarily attended by researchers from Germany and neighboring countries, it warmly welcomes international participation. The KI 2019 conference took place in Kassel, Germany, September 23–26, 2019, and it was held in conjunction with the 49th Annual Conference of the German Computer Science Association (INFORMATIK 2019). Information about the event can be found at www.ki2019.de and informatik2019.de, respectively. KI 2019 had a special focus theme on “AI methods for Argumentation” and we especially invited contributions that use methods from all areas of AI to understand, formalize, or generate argument structures in natural language. The special focus theme was organized in cooperation with the DFG funded priority program “RATIO: Robust Argumentation Machines”. Besides this special focus theme, the conference invited original research papers and shorter technical communications on all topics of AI. Further, we asked for the submission of extended abstracts summarizing papers that had recently been presented at major AI conferences. KI 2019 received 82 submissions, with authors from 25 countries. Submissions were – except for some special cases – reviewed by three Program Committee members. The Program Committee, comprised of 51 experts from 9 countries, decided to accept 29 papers. Out of these, 16 submissions were accepted as full papers, 10 as short papers and 3 as extended abstracts. The program also included three invited talks: – Jürgen Altmann (University of Dortmund): Autonomous Weapon Systems – Dangers and Need for an International Prohibition – Michael Beetz (University of Bremen): Digital Twin Knowledge Bases – Knowledge Representation and Reasoning for Robotic Agent – Antony Hunter (University College London): Towards Computational Persuasion for Behaviour Change Applications Two of these presentations are summarized in papers contained in this volume. Overall, it was a pleasure to organize KI 2019 and we are grateful to our co-organizers, Alexander Steen (Workshops and Tutorials Chair) and Kristina Yordanova (Doctoral Consortium Chair), who provided valuable additional support in organizing the event. We thank the Program Committee members and all additional reviewers for the effort and time they invested in the reviewing process. Further, we thank the Organizing Committee of INFORMATIK 2019 who took care of finances and local organization and allowed us to focus on the scientific aspects of the conference. Our appreciation also goes to the developers of EasyChair, which provides great functionalities that helped to organize the reviewing process and to create this volume. Last but not least, we would like to thank SAP SE for generously sponsoring travel grants for students to attend KI 2019. July 2019 Christoph Benzmüller Heiner Stuckenschmidt [less ▲]

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

in Benzmüller, Christoph; Stuckenschmidt, Heiner (Eds.) {KI} 2019: Advances in Artificial Intelligence - 42nd German Conference on AI, Kassel, Germany, September 23-26, 2019, Proceedings (2019)

Detailed reference viewed: 17 (1 UL)
Full Text
See detailExtensional Higher-Order Paramodulation in Leo-III
Steen, Alexander UL; Benzmüller, Christoph UL

E-print/Working paper (2019)

Detailed reference viewed: 19 (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: 68 (1 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: 132 (21 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: 148 (34 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: 38 (14 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: 45 (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: 55 (5 UL)
Full Text
Peer Reviewed
See detailSystem Demonstration: The Higher-Order Prover Leo-III
Steen, Alexander UL; Benzmüller, Christoph UL

in CEUR Workshop Proceedings (2018), 2095

Detailed reference viewed: 24 (14 UL)
See detailI/O Logic in HOL --- First Steps
Benzmüller, Christoph UL; Parent, Xavier UL

E-print/Working paper (2018)

A semantical embedding of input/output logic in classical higher-order logic is presented. This embedding enables the mechanisation and automation of reasoning tasks in input/output logic with off-the ... [more ▼]

A semantical embedding of input/output logic in classical higher-order logic is presented. This embedding enables the mechanisation and automation of reasoning tasks in input/output logic with off-the-shelf higher-order theorem provers and proof assistants. The key idea for the solution presented here results from the analysis of an inaccurate previous embedding attempt, which we will discuss as well. [less ▲]

Detailed reference viewed: 28 (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: 22 (1 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: 41 (3 UL)