[en] We devise a shallow semantical embedding of \AA{}qvist's dyadic deontic logic {\bf 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.
Disciplines :
Sciences informatiques
Auteur, co-auteur :
BENZMÜLLER, Christoph ; University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)
FARJAMI, Ali ; University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)
PARENT, Xavier ; University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)
Co-auteurs externes :
yes
Langue du document :
Anglais
Titre :
Aqvist's Dyadic Deontic Logic E in HOL
Date de publication/diffusion :
17 septembre 2018
Nom de la manifestation :
MIREL 2018 workshop on MIning and REasoning with Legal texts
Organisateur de la manifestation :
University of Luxembourg
Lieu de la manifestation :
Luxembourg
Date de la manifestation :
17-09-2018
Manifestation à portée :
International
Projet européen :
H2020 - 690974 - MIREL - MIREL - MIning and REasoning with Legal texts
