Normative Reasoning with Expressive Logic Combinations

摘要

We discuss ongoing work on reusing existing (higher-order) automated reasoning infrastructure for seamlessly combining and reasoning with different non-classical logics (modal, deontic, epistemic, paraconsistent, etc.), particularly suited for normative reasoning. Our work illustrates, in particular, the utilisation of the Isabelle/HOL proof assistant for the representation and formal assessment of linguistically complex ethical arguments. Our work pushes existing boundaries in knowledge representation and reasoning. We demonstrate that intuitive, formal encodings of complex ethical theories and their automation on the computer are no longer antipodes.