2018/02/23 by Christoph Benzmüller, Benzmüller, Christoph, Ali Farjami +3
Computer Science · Mathematics · #03B15 #03B60 #68T15 #68T27 #68T30 #Artificial Intelligence (cs.AI) #F.4 #FOS: Computer and information sciences #FOS: Mathematics #I.2.0 #I.2.3 #I.2.4 #Logic (math.LO) #Logic in Computer Science (cs.LO) #acm:03B15 #acm:03B60 #acm:68T15 #acm:68T27 #acm:68T30 #cs.AI #cs.LO #math.LO #msc:03B15 #msc:03B60 #msc:68T15 #msc:68T27 #msc:68T30
paper · pdf · doi:10.48550/arxiv.1802.08454
23 pages, 3 figures
arxiv created 2018/03/05 · arxiv updated 2018/03/06
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.