[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 :
Computer science
Author, co-author :
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)
External co-authors :
no
Language :
English
Title :
Implementation of Dyadic Deontic Logic E in Isabelle/HOL
Publication date :
04 May 2018
Event name :
10th edition of PhDs in Logic
Event organizer :
Institute of Computer Science and the Institute of Philosophy of the Czech Academy of Sciences and by the Department of Logic of Charles University.
