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

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: 50 (15 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: 45 (13 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: 12 (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: 22 (11 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: 29 (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: 47 (5 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: 18 (0 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: 17 (1 UL)Rules and Reasoning, Second International Joint Conference, RuleML+RR 2018, Luxembourg, Luxembourg, September 18-21, 2018, Proceedings Benzmüller, Christoph ; ; Parent, Xavier et al Book published by Springer (2018) Detailed reference viewed: 14 (2 UL)A Model for Regulating of Ethical Preferences in Machine Ethics Baniasadi, Zohreh ; Parent, Xavier ; Max, Charles et al in Proceedings of International Conference on Human-Computer Interaction (2018) Detailed reference viewed: 38 (9 UL)Detachment in Normative Systems: Examples, inference Patterns, Properties Parent, Xavier ; van der Torre, Leon in The IfCoLog Journal of Logics and their Applications (2017), 4(9), 2295-3039 There is a variety of ways to reason with normative systems. This partly reflects a variety of semantics developed for deontic logic, such as traditional semantics based on possible worlds, or alternative ... [more ▼] There is a variety of ways to reason with normative systems. This partly reflects a variety of semantics developed for deontic logic, such as traditional semantics based on possible worlds, or alternative semantics based on algebraic methods, explicit norms or techniques from non-monotonic logic. This diversity raises the question how these reasoning methods are related, and which reasoning method should be chosen for a particular application. In this paper we discuss the use of examples, inference patterns, and more abstract properties. First, benchmark examples can be used to compare ways to reason with normative systems. We give an overview of several benchmark examples of normative reasoning and deontic logic: van Fraassen’s paradox, Forrester’s paradox, Prakken and Sergot’s cottage regulations, Jeffrey’s disarmament example, Chisholm’s paradox, Makinson’s Möbius strip, and Horty’s priority examples. Moreover, we distinguish various interpretations that can be given to these benchmark examples, such as consistent interpretations, dilemma interpretations, and violability interpretations. Second, inference patterns can be used to compare different ways to reason with normative systems. Instead of analysing the benchmark examples semantically, as it is usually done, in this paper we use inference patterns to analyse them at a higher level of abstraction. We discuss inference patterns reflecting typical logical properties such as strengthening of the antecedent or weakening of the consequent. Third, more abstract properties can be defined to compare different ways to reason with normative systems. To define these more abstract properties, we first present a formal framework around the notion of detachment. Some of the ten properties we introduce are derived from the inference patterns, but others are more abstract: factual detachment, violation detection, substitution, replacements of equivalents, implication, para-consistency, conjunction, factual monotony, norm monotony, and norm induction. We consider these ten properties as desirable for a reasoning method for normative systems. [less ▲] Detailed reference viewed: 169 (26 UL)Implementation of Carmo and Jones Dyadic Deontic Logic in Isabelle/HOL Benzmüller, Christoph ; Farjami, Ali ; Parent, Xavier 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: 98 (16 UL)The pragmatic oddity in a norm-based semantics Parent, Xavier ; van der Torre, Leon in Governatori, Guido (Ed.) 16th International Conference on Artificial Intelligence & Law (ICAIL-17) (2017, June) The ideal worlds of a possible worlds semantics may satisfy both a primary obligation and an associated secondary obligation, for example the obligation to keep a promise and the obligation to apologise ... [more ▼] The ideal worlds of a possible worlds semantics may satisfy both a primary obligation and an associated secondary obligation, for example the obligation to keep a promise and the obligation to apologise for not keeping it. This is known as the pragmatic oddity introduced by Prakken and Sergot. We argue that an adequate treatment of the pragmatic oddity within a norm-based semantics can be obtained, by not allowing primary and secondary obligations to aggregate, because they are obligations of a di erent kind. On the basis of this conceptual analysis, we introduce two logics, depending on the stance taken on the representation of normative con icts, and we present sound and complete proof systems for these logics. We then give a formal analysis, discuss extensions, and highlight various topics for further research. [less ▲] Detailed reference viewed: 176 (21 UL)A Representation Theorem for Abstract Cumulative Aggregation Ambrossio, Diego Agustin ; Parent, Xavier ; van der Torre, Leon Report (2016) From any two conditional obligations “X if A” and “Y if B”, cumulative aggregation derives the combined obligation “X ∪ Y if A ∪ (B \ X)”, whereas simple aggregation derives the obligation “X ∪ Y if A ∪ ... [more ▼] From any two conditional obligations “X if A” and “Y if B”, cumulative aggregation derives the combined obligation “X ∪ Y if A ∪ (B \ X)”, whereas simple aggregation derives the obligation “X ∪ Y if A ∪ B”. We propose FC systems consisting of cumulative aggregation together with factual detachment, and we give a representation result for FC systems, as well as for FA systems consisting of simple aggregation together with factual detachment. We relate FC and FA systems to each other and to input/output logics recently introduced by Parent and van der Torre. [less ▲] Detailed reference viewed: 138 (37 UL)Cumulative Aggregation Ambrossio, Diego Agustin ; Parent, Xavier ; van der Torre, Leon in Deontic Logic and Normative Systems (2016) From any two conditional obligations “X if A” and “Y if B”, cumulative aggregation derives the combined obligation “X ∪ Y if A ∪ (B\X)”, whereas simple aggregation derives the obligation “X ∪ Y if A ∪ B” ... [more ▼] From any two conditional obligations “X if A” and “Y if B”, cumulative aggregation derives the combined obligation “X ∪ Y if A ∪ (B\X)”, whereas simple aggregation derives the obligation “X ∪ Y if A ∪ B”. We propose FC systems consisting of cumulative aggregation together with factual detachment, and we give a representation result for FC systems, as well as for FA systems consisting of simple aggregation together with factual detachment. We relate FC and FA systems to each other and to input/output logics recently introduced by Parent and van der Torre. [less ▲] Detailed reference viewed: 72 (10 UL)Completeness of Aqvist's systems E and F Parent, Xavier in Review of Symbolic Logic (2015), 8(1), 164-177 This paper tackles an open problem posed by Åqvist. It is the problem of whether his dyadic deontic systems E and F are complete with respect to their intended Hanssonian preference- based semantics. It ... [more ▼] This paper tackles an open problem posed by Åqvist. It is the problem of whether his dyadic deontic systems E and F are complete with respect to their intended Hanssonian preference- based semantics. It is known that there are two different ways of interpreting what it means for a world to be best or top-ranked among alternatives. This can be understood as saying that it is optimal among them, or maximal among them. First, it is established that, under either the maximality rule or the optimality rule, E is sound and complete with respect to the class of all preference models, the class of those in which the betterness relation is reflexive, and the class of those in which it is total. Next, an analogous result is shown to hold for F. That is, it is established that, under either rule, F is sound and complete with respect to the class of preference models in which the betterness relation is limited, the class of those in which it is limited and reflexive, and the class of those in which it is limited and total. [less ▲] Detailed reference viewed: 44 (7 UL)Maximality vs. Optimality in Dyadic Deontic Logic Parent, Xavier in J. Philosophical Logic (2014), 43(6), 1101--1128 This paper reports completeness results for dyadic deontic logics in the tradition of Hansson’s systems. There are two ways to understand the core notion of best antecedent- worlds, which underpins such ... [more ▼] This paper reports completeness results for dyadic deontic logics in the tradition of Hansson’s systems. There are two ways to understand the core notion of best antecedent- worlds, which underpins such systems. One is in terms of maximality, and the other in terms of optimality. Depending on the choice being made, one gets different evaluation rules for the deontic modalities, but also different versions of the so-called limit assumption. Four of them are disentangled, and compared. The main observation of this paper is that, even in the partial order case, the contrast between maximality and optimality is not as significant as one could expect, because the logic remains the same whatever notion of best is used. This is established by showing that, given analogous properties for the betterness relation, the same system is sound and complete with respect to its intended modelling. The chief resultofthispaperconcernsA ̊qvist’ssystemFsupplementedwiththeprinciple(CM)of cautious monotony. It is established that, under the maximality rule, F+(CM) is sound and complete with respect to the class of models in which the betterness relation is required be reflexive and smooth (for maximality). From this, a number of spin-off results are obtained. First and foremost, it is shown that a similar determination result holds for optimality; that is, under the optimality rule, F+(CM) is also sound and complete with respect to the class of models in which the betterness relation is reflexive and smooth (for optimality). Other spin-off results concern classes of models in which further constraints are placed on the betterness relation, like totalness and transitivity. [less ▲] Detailed reference viewed: 45 (2 UL)Sing and Dance! van der Torre, Leon ; Parent, Xavier in Sing and Dance! (2014) Makinson and van der Torre [13] introduce a number of input/output (I/O) logics to reason about conditional norms. The key idea is to make obligations relative to a given set of conditional norms. The ... [more ▼] Makinson and van der Torre [13] introduce a number of input/output (I/O) logics to reason about conditional norms. The key idea is to make obligations relative to a given set of conditional norms. The meaning of the normative concepts is, then, given in terms of a set of procedures yielding outputs for inputs. Using the same methodology, Stolpe[19,20] has developed some more I/O logics to include systems without the rule of weakening of the output (or principle of inheritance). We extend Stolpe’s account in two directions. First, we show how to make it support reasoning by cases−a common form of reasoning. Second, we show how to inject a new (as we call it, “aggregative”) form of cumulative transitivity, which we think is more suitable for normative reasoning. The main outcomes of the paper are soundness and completeness theorems for the proposed systems with respect to their intended semantics. [less ▲] Detailed reference viewed: 55 (5 UL)Aggregative Deontic Detachment for Normative Reasoning Parent, Xavier ; van der Torre, Leon in KR&R (2014) Detailed reference viewed: 26 (1 UL)Intuitionistic basis for IOL Parent, Xavier ; van der Torre, Leon ; Gabbay, Dov M. in Hansson, Sven Ove (Ed.) David Makinson's outsanding contribution to non-classical logic (2014) Detailed reference viewed: 88 (20 UL) |
||