Faithful Semantical Embedding of a Dyadic Deontic Logic in HOL
This work provides a theoretical foundation for automating dyadic deontic logic in off-the-shelf tools, addressing a specific need in formal verification and logic communities.
The authors tackled the problem of embedding a dyadic deontic logic into classical higher-order logic, proving the embedding is sound and complete, which enables its automation in existing theorem provers.
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.