First Experiments with a Flexible Infrastructure for Normative Reasoning
This work addresses the need for flexible reasoning infrastructure in normative domains, but it is incremental as it builds on existing universal logical reasoning approaches.
The authors tackled the problem of normative reasoning by implementing a small-scale demonstrator in Isabelle/HOL using shallow semantical embeddings, motivated by a contrary-to-duty example from the General Data Protection Regulation.
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.