Faithful Semantical Embedding of a Dyadic Deontic Logic in HOL

Reference : Faithful Semantical Embedding of a Dyadic Deontic Logic in HOL


	Document type :	Reports : Expert report
	Discipline(s) :	Engineering, computing & technology : Computer science
	To cite this reference:	http://hdl.handle.net/10993/36397

Title :	Faithful Semantical Embedding of a Dyadic Deontic Logic in HOL
Language :	English
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) >]
Publication date :	23-Feb-2018
Keywords :	[en] Dyadic deontic logic ; Classical higher-order logic ; Semantic embedding ; Faithfulness
Abstract :	[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.
Permalink :	http://hdl.handle.net/10993/36397

File(s) associated to this reference

Fulltext file(s):

	File	Commentary	Version	Size	Access
Open access	Faithful Semantical Embedding of a.pdf		Author preprint	1.04 MB	View/Open

All documents in ORBi^lu are protected by a user license.