![]() Benzmüller, Christoph ![]() ![]() 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 ▲] Detailed reference viewed: 170 (6 UL)![]() Benzmüller, Christoph ![]() ![]() ![]() in IfCoLog Journal of Logics and Their Applications (2019), 6(5), 715--732 Detailed reference viewed: 73 (13 UL)![]() Farjami, Ali ![]() ![]() ![]() 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: 281 (40 UL)![]() Meder, Paul Joseph Yves ![]() Bachelor/master dissertation (2018) This work presents temporal STIT I/O logic, an I/O logic based on temporal STIT logic, and documents its investigation with the proof assistant tool Isabelle/ HOL. We show how to semantically embedding ... [more ▼] This work presents temporal STIT I/O logic, an I/O logic based on temporal STIT logic, and documents its investigation with the proof assistant tool Isabelle/ HOL. We show how to semantically embedding temporal STIT logic as well as the out2 operator in HOL. Implementing those embeddings and also the already existing embedding of the out1 operator into Isabelle/HOL framework, enables the application of higher-order automatic theorem provers for automated reasoning tasks in temporal STIT I/O logic. Finally, we relate our logic to a more philosophical topic called moral luck, identify which aspects of moral luck can be studied by it, and use examples from this subject as test cases for the logic. [less ▲] Detailed reference viewed: 187 (31 UL) |
||