Aqvist's Dyadic Deontic Logic E in HOL

Christoph Benzmüller , Ali Farjami, Xavier Parent – 2018

We devise a shallow semantical embedding of \AA{}qvist's dyadic deontic logic {\bf E} in classical higher-order logic. This embedding is encoded in Isabelle/HOL, which turns this system into a proof assistant for deontic logic reasoning. The experiments with this environment provide evidence that this logic \textit{implementation} fruitfully enables interactive and automated reasoning at the meta-level and the object-level.

Titel
Aqvist's Dyadic Deontic Logic E in HOL
Verfasser
Christoph Benzmüller , Ali Farjami, Xavier Parent
Datum
2018-09-17
Quelle/n
Erschienen in
MIREL 2018 workshop on MIning and REasoning with Legal Texts. University Luxembourg, Sept. 2018.
Größe oder Länge
15 pages