I/O Logic in HOL
Christoph Benzmüller, Ali Farjami, Paul Joseph Yves Meder, Xavier Parent – 2018
A shallow semantical embedding of Input/Output logic in classical higher-order logic is presented, and shown to be faithful (sound an complete). This embedding has been implemented in the higher-order proof assistant Isabelle/HOL. We provide an empirical regulative framework for assessing General Data Protection Regulation.
Titel
I/O Logic in HOL
Verfasser
Christoph Benzmüller, Ali Farjami, Paul Joseph Yves Meder, Xavier Parent
Schlagwörter
Input/output logic ; Isabelle/HOL ; General Data Protection Regulation
Datum
2018-09-17
Quelle/n
Erschienen in
MIREL 2018 Workshop on MIning and REasoning with Legal texts, Sept. 2018