Logical Methods for Deontic Explanations

道义推理涉及到义务和相关概念，在从法律、伦理到人工智能的各个领域都有着重要的作用。道义逻辑和形式论证的结合为这类推理的建模提供了富有成效的理论基础。“道义解释的逻辑方法”（LoDEx）项目的三个合作伙伴代表了该领域的重要发展：Ciabattoni（维也纳理工大学）解决数学和逻辑的实际问题，Straßer（鲁尔大学波鸿）在哲学中使用形式方法，货车德尔托雷（卢森堡大学）提供计算机科学和人工智能中的法律的和伦理推理。现在，他们正在联合起来，发展一种正式的理论，他们称之为道义解释。道义解释提供了一些道义概念成立而另一些不成立的理由。它们为复杂的问题提供了答案，比如“在特定的背景下，为什么一个孩子应该托付给他的父亲，而不是母亲？或者“是否应该强迫一个跟随耶和华见证人信仰的人接受救命的输血？为什么（不）？''.通过对推理过程的理解和透明呈现，道义解释在许多领域都是一个重要的关注点。在（生物）伦理和法律案例研究的推动下，LoDEx开发了逻辑方法，并提供工具支持，以正式化和推理道义解释。通过整合基于偏好和基于规范的解释，LoDEx接受了Makinson（1998）和Horty（2014）提出的挑战，即结合道义逻辑领域的几种不相关的方法来制定统一的逻辑理论。通过正式的论证和对话，解释量身定制，以确保被解释者的理解与被解释者的先入之见和期望的微调解释的生成。LoDEx填补了规范性推理的正式理论中的一个核心空白，到目前为止，规范性推理一直关注的是合理性而不是个性化的解释。在法律和（生物）伦理学中迫切需要道义解释，这两个领域特别涉及道义推理，并且充满冲突。为了满足这一需求，LoDEx的正式方法将应用于这些领域的关键案例研究并进行评估。将开发计算机支持的工具，以便试验这些方法、正式的法律的和生物伦理学理论以及这些理论的应用。为此，我们将使用LogiKEy方法。新创建的LogiKEY数据集的传播将实现可重用性，并促进道义逻辑社区的实现。LoDEx方法、工具和应用将有助于及时应对跨学科挑战，为更加以人为本的逻辑和推理提供正式的基础。

Deontic reasoning, which involves obligation and related notions, is highly important in a variety of fields---from law and ethics to artificial intelligence. The combination of deontic logic and formal argumentation provides a fruitful theoretical basis for modelling this type of reasoning. The three partners of the "Logical methods for Deontic EXplanations" (LoDEx) project represent important developments in the area: Ciabattoni (Vienna University of Technology) addresses practical concerns in mathematics and logic, Straßer (Ruhr University Bochum) uses formal methods in philosophy, and van der Torre (University of Luxembourg) provides legal and ethical reasoners in computer science and artificial intelligence. Now they are joining forces to develop a formal theory of what they call deontic explanations. Deontic explanations provide reasons why some deontic notions hold and others do not. They provide answers to complex questions like "Why should a child be entrusted to its father, rather than its mother, given a specific context?'' or "Should someone who follows the faith of Jehovah's Witnesses be forced to undergo a life-saving blood transfusion? Why (not)?''. By targeting the understanding and transparent presentation of reasoning processes, deontic explanations are a major concern in many fields. Driven by case studies in (bio)ethics and law, LoDEx develops logical methods with tool support to formalise and reason about deontic explanations. By integrating both preference-based and norm-based explanations, LoDEx takes up the challenge raised by Makinson (1998) and Horty (2014) of formulating a unified logical theory combining several disconnected methods from the field of deontic logic. By means of formal argumentation and dialogues, explanations are tailored to ensure explainee comprehension with the generation of fine-tuned explanations relative to the explainee's preconceptions and expectations. LoDEx fills a central gap in formal theories of normative reasoning, which so far have been concerned with justifications rather than personalised explanations. There is an urgent demand for deontic explanations in law and (bio)ethics, two domains where deontic reasoning is particularly involved and which are rich in conflicts. To meet this demand, the formal methods of LoDEx will be applied to and evaluated on key case studies from these areas. Computer-supported tools will be developed in order to experiment with the methods, the formal legal and bioethical theories, and applications of those theories. We will use the LogiKEy methodology for this purpose. The dissemination of the newly created LogiKEY data sets will enable reusability and facilitate implementations for the deontic logic community. LoDEx methods, tools and applications will contribute to the timely interdisciplinary challenge of providing formal foundations to more human-centred logic and reasoning.