AQVIST'S DYADIC DEONTIC LOGIC E IN HOL

We devise a shallow semantical embedding of Aqvist's dyadic deontic logic E in classical higher-order logic. This embedding is shown to be faithful, viz. sound and complete. This embedding is also encoded in Isabelle/HOL, which turns this system into a proof assistant for deontic logic reasoning. The experiments with this environment provide evidence that this logic implementation fruitfully enables interactive and automated reasoning at the meta-level and the object-level.