LogiKEy Workbench: Deontic Logics, Logic Combinations and Expressive Ethical and Legal Reasoning (Isabelle/HOL Dataset)

in Data in Brief (2020), 33

The LogiKEy workbench and dataset for ethical and legal reasoning is presented. This workbench simultaneously supports development, experimentation, assessment and deployment of formal logics and ethical ... [more ▼]

The LogiKEy workbench and dataset for ethical and legal reasoning is presented. This workbench simultaneously supports development, experimentation, assessment and deployment of formal logics and ethical and legal theories at different conceptual layers. More concretely, it comprises, in form of a dataset (Isabelle/HOL theory files), formal encodings of multiple deontic logics, logic combinations, deontic paradoxes and normative theories in the higher-order proof assistant system Isabelle/HOL. The data were acquired through application of the LogiKEy methodology, which supports experimentation with different normative theories, in different application scenarios, and which is not tied to specific logics or logic combinations. Our workbench consolidates related research contributions of the authors and it may serve as a starting point for further studies and experiments in flexible and expressive ethical and legal reasoning. It may also support hands-on teaching of non-trivial logic formalisms in lecture courses and tutorials. [less ▲]

I/O Logic in HOL

in IfCoLog Journal of Logics and Their Applications (2019), 6(5), 715--732

Machine Argumentation. Can We Replace Taxi Drivers by Robots?

in Natural Argument, A tribute to John Woods (2019)

We need ethical non-monotonic action logics to control machines which interact heavily with humans. Such logics face special problems and require features which we need to recognise and to address. We ... [more ▼]

We need ethical non-monotonic action logics to control machines which interact heavily with humans. Such logics face special problems and require features which we need to recognise and to address. We believe that injecting argumentation methods into action pre-conditions is possibly the way to proceed to model what is needed. To get an idea of what is needed we must investigate a typical problem of replacing a human with a robot operating in a highly interactive environment. This paper focuses on replacing a human taxi driver by a robot. Robot driven cars are already under production and so there is an urgent need for modelling the kind of Artificial Intelligence/Logic/Norms/Ethics which is to be involved and installed in the mind of the Robot. This is research in progress. [less ▲]

I/O Logic in HOL

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 ▲]

A Dyadic Deontic Logic in HOL

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 ▲]

Faithful Semantical Embedding of a Dyadic Deontic Logic in HOL

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 ▲]