Dyadic Deontic Logic in HOL : Faithful Embedding and Meta-Theoretical Experiments
Faculty/Professorship: | AI Systems Engineering |
Author(s): | Benzmüller, Christoph ![]() |
Title of the compilation: | New developments in legal reasoning and logic : from ancient law to modern legal systems |
Editors: | Rahman, Shahid; Armgardt, Matthias; Nordtveit Kvernenes, Hans Christian |
Publisher Information: | Cham : Springer |
Year of publication: | 2022 |
Pages: | 353–377 |
Source/Other editions: | New developments in legal reasoning and logic : from ancient law to modern legal systems / Shahid Rahman, Matthias Armgardt, Hans Christian Nordtveit Kvernenes (editors). - Cham : Springer, 2022, S. 353-377. - ISBN 978-3-030-70084-3 |
is version of: | 10.1007/978-3-030-70084-3_14 |
Language(s): | English |
Licence: | German Act on Copyright |
URN: | urn:nbn:de:bvb:473-irb-545469 |
Abstract: | A shallow semantical embedding of a dyadic deontic logic by Carmo and Jones in classical higher-order logic is presented. The embedding is proven sound and complete, that is, faithful. This result provides the theoretical foundation for the implementation and automation of dyadic deontic logic within off-the-shelf higher-order theorem provers and proof assistants. To demonstrate the practical relevance of our contribution, the embedding has been encoded in the Isabelle/HOL proof assistant. As a result a sound and complete (interactive and automated) theorem prover for the dyadic deontic logic of Carmo and Jones has been obtained. Experiments have been conducted which illustrate how the exploration and assessment of meta-theoretical properties of the embedded logic can be supported with automated reasoning tools integrated with Isabelle/HOL. |
GND Keywords: | Deontische Logik; HOL; Semantik; Treue <Motiv> |
Keywords: | Dyadic deontic logic, Classical higher-order logic, Semantic embedding, Faithfulness |
DDC Classification: | 004 Computer science 510 Mathematics |
RVK Classification: | SK 130 |
Peer Reviewed: | Ja |
International Distribution: | Ja |
Type: | Contribution to an Articlecollection |
URI: | https://fis.uni-bamberg.de/handle/uniba/54546 |
Release Date: | 20. July 2022 |
File | Size | Format | |
---|---|---|---|
fisba54546.pdf | 1.52 MB | View/Open |

originated at the
University of Bamberg
University of Bamberg