[en] A shallow semantical embedding of a dyadic deontic logic by Carmo
and Jones in classical higher-order logic is presented. This
embedding is proven sound and complete, that is, faithful.
The work presented here provides the theoretical foundation for the
implementation and automation of dyadic deontic logic within
off-the-shelf higher-order theorem provers and proof assistants.
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)
Langue du document :
Anglais
Titre :
Faithful Semantical Embedding of a Dyadic Deontic Logic in HOL
