Åqvist's Dyadic Deontic Logic E in HOL

EasyChair Preprint 554

Abstract

We devise a shallow semantical embedding of Åqvist's dyadic deontic logic E in classical higher-order logic. This embedding is 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 \textit{implementation} fruitfully enables interactive and automated reasoning at the meta-level and the object-level.

Keyphrases: Dyadic deontic logic E, Preference Models, automated reasoning, classical higher-order logic, semantic embedding

@booklet{EasyChair:554,
  author    = {Christoph Benzmüller and Ali Farjami and Xavier Parent},
  title     = {Åqvist's Dyadic Deontic Logic E in HOL},
  doi       = {10.29007/t29j},
  howpublished = {EasyChair Preprint 554},
  year      = {EasyChair, 2018}}