Browse ORBi

- What it is and what it isn't
- Green Road / Gold Road?
- Ready to Publish. Now What?
- How can I support the OA movement?
- Where can I learn more?

ORBi

Results 1-20 of 39.
((uid:50026622))
Automating Free Logic in HOL, with an Experimental Application in Category Theory Benzmüller, Christoph ; 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: 75 (1 UL)Universal (Meta-)Logical Reasoning: Recent Successes Benzmüller, Christoph 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: 62 (1 UL)I/O Logic in HOL Farjami, Ali ; Meder, Paul Joseph Yves ; Parent, Xavier 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: 137 (31 UL)Aqvist's Dyadic Deontic Logic E in HOL Benzmüller, Christoph ; Farjami, Ali ; Parent, Xavier 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: 121 (20 UL)A Faithful Semantic Embedding of the Dyadic Deontic Logic E in HOL Benzmüller, Christoph ; Farjami, Ali ; Parent, Xavier Poster (2018, June 16) Detailed reference viewed: 21 (5 UL)A Dyadic Deontic Logic in HOL Benzmüller, Christoph ; Farjami, Ali ; Parent, Xavier 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: 33 (13 UL)Implementation of Dyadic Deontic Logic E in Isabelle/HOL Benzmüller, Christoph ; Farjami, Ali ; Parent, Xavier 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: 43 (4 UL)Faithful Semantical Embedding of a Dyadic Deontic Logic in HOL Benzmüller, Christoph ; Farjami, Ali ; Parent, Xavier 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: 53 (5 UL)First Experiments with a Flexible Infrastructure for Normative Reasoning Benzmüller, Christoph ; Parent, Xavier 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)I/O Logic in HOL --- First Steps Benzmüller, Christoph ; Parent, Xavier 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: 27 (0 UL)The Higher-Order Prover Leo-III Steen, Alexander ; Benzmüller, Christoph 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: 34 (2 UL)A Case Study On Computational Hermeneutics: E. J. Lowe's Modal Ontological Argument ; Benzmüller, Christoph 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: 52 (0 UL)Formalisation and Evaluation of Alan Gewirth's Proof for the Principle of Generic Consistency in Isabelle/HOL ; Benzmüller, Christoph 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: 45 (0 UL)Some Reflections on a Computer-aided Theory Exploration Study in Category Theory (Extended Abstract) Benzmüller, Christoph ; in 3rd Conference on Artificial Intelligence and Theorem Proving (AITP 2018), Book of Abstracts (2018) Detailed reference viewed: 14 (0 UL)System Demonstration: The Higher-Order Prover Leo-III ; Benzmüller, Christoph in CEUR Workshop Proceedings (2018), 2095 Detailed reference viewed: 16 (6 UL)Axiom Systems for Category Theory in Free Logic Benzmüller, Christoph ; in Archive of Formal Proofs (2018) Detailed reference viewed: 24 (0 UL)Can Computers Help to Sharpen our Understanding of Ontological Arguments? Benzmüller, Christoph ; 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: 27 (0 UL)A Deontic Logic Reasoning Infrastructure Benzmüller, Christoph ; Parent, Xavier ; van der Torre, Leon in Sailing Routes in the World of Computation, 14th Conference on Computability in Europe, CiE 2018, Kiel, Germany, July 30 – August 3, 2018, Proceedings (2018) A flexible infrastructure for the automation of deontic and normative reasoning is presented. Our motivation is the development, study and provision of legal and moral reasoning competencies in future ... [more ▼] A flexible infrastructure for the automation of deontic and normative reasoning is presented. Our motivation is the development, study and provision of legal and moral reasoning competencies in future intelligent machines. Since there is no consensus on the “best” deontic logic formalisms and since the answer may be application specific, a flexible infrastructure is proposed in which candidate logic formalisms can be varied, assessed and compared in experimental ethics application studies. Our work thus links the historically rich research areas of classical higher-order logic, deontic logics, normative reasoning and formal ethics. [less ▲] Detailed reference viewed: 80 (1 UL)Computational Hermeneutics: Using Computers to Interpret Philosophical Arguments (Abstract) ; Benzmüller, Christoph in Logical Correctness, Workshop at UNILOG'2018, UNILOG'2018 Book of Abstracts (2018) Detailed reference viewed: 33 (0 UL)ARQNL 2018 Automated Reasoning in Quantified Non-Classical Logics Benzmüller, Christoph ; in CEUR Workshop Proceedings (2018), 2095 Detailed reference viewed: 16 (0 UL) |
||