Reference : Faithful Semantical Embedding of a Dyadic Deontic Logic in HOL
Reports : Expert report
Engineering, computing & technology : Computer science
http://hdl.handle.net/10993/36397
Faithful Semantical Embedding of a Dyadic Deontic Logic in 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) >]
23-Feb-2018
[en] Dyadic deontic logic ; Classical higher-order logic ; Semantic embedding ; Faithfulness
[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.
http://hdl.handle.net/10993/36397

File(s) associated to this reference

Fulltext file(s):

FileCommentaryVersionSizeAccess
Open access
Faithful Semantical Embedding of a.pdfAuthor preprint1.04 MBView/Open

Bookmark and Share SFX Query

All documents in ORBilu are protected by a user license.