Implementation of Carmo and Jones Dyadic Deontic Logic in Isabelle/HOL
Christoph Benzmüller, Ali Farjami, Xavier Parent, Leendert van der Torre · Open Repository and Bibliography (University of Luxembourg) · 2017
A shallow semantical embedding of a dyadic deontic logic (by Carmo and Jones) in Isabelle/HOL is presented. First experiments provide evidence that this logic implementation fruitfully enables interactive and automated reasoning at the meta-level the object-level.