[en] We have devised a shallow semantical embedding of a dyadic deontic logic (by B.Hansson and \AA{}qvist) in classical higher-order logic. This embedding has been 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 :
no
Langue du document :
Anglais
Titre :
Implementation of Dyadic Deontic Logic E in Isabelle/HOL
Date de publication/diffusion :
04 mai 2018
Nom de la manifestation :
10th edition of PhDs in Logic
Organisateur de la manifestation :
Institute of Computer Science and the Institute of Philosophy of the Czech Academy of Sciences and by the Department of Logic of Charles University.
