Reference : Implementation of Dyadic Deontic Logic E in Isabelle/HOL
Scientific congresses, symposiums and conference proceedings : Unpublished conference
Engineering, computing & technology : Computer science
http://hdl.handle.net/10993/36396
Implementation of Dyadic Deontic Logic E in Isabelle/HOL
English
Benzmüller, Christoph mailto [University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC) >]
Farjami, Ali mailto [University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC) >]
Parent, Xavier mailto [University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC) >]
4-May-2018
Yes
International
10th edition of PhDs in Logic
from 01-05-2018 to 04-05-2018
Institute of Computer Science and the Institute of Philosophy of the Czech Academy of Sciences and by the Department of Logic of Charles University.
Prague
Czech Republic
[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.
http://hdl.handle.net/10993/36396

File(s) associated to this reference

Fulltext file(s):

FileCommentaryVersionSizeAccess
Open access
Phds in Logic.pdfPublisher postprint167.77 kBView/Open

Bookmark and Share SFX Query

All documents in ORBilu are protected by a user license.