Download PDFOpen PDF in browser

Åqvist's Dyadic Deontic Logic E in HOL

EasyChair Preprint no. 554

15 pagesDate: October 3, 2018


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: automated reasoning, classical higher-order logic, Dyadic deontic logic E, Preference Models, semantic embedding

BibTeX entry
BibTeX does not have the right entry for preprints. This is a hack for producing the correct reference:
  author = {Christoph Benzmüller and Ali Farjami and Xavier Parent},
  title = {Åqvist's Dyadic Deontic Logic E in HOL},
  howpublished = {EasyChair Preprint no. 554},
  doi = {10.29007/t29j},
  year = {EasyChair, 2018}}
Download PDFOpen PDF in browser