Faithful Semantical Embedding of a Dyadic Deontic Logic in HOL
Artificial Intelligence
2018-03-06 v2 Logic in Computer Science
Logic
Abstract
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.
Keywords
Cite
@article{arxiv.1802.08454,
title = {Faithful Semantical Embedding of a Dyadic Deontic Logic in HOL},
author = {Christoph Benzmüller and Ali Farjami and Xavier Parent},
journal= {arXiv preprint arXiv:1802.08454},
year = {2018}
}
Comments
23 pages, 3 figures