License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2021.7
URN: urn:nbn:de:0030-drops-139028
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/13902/
Benzmüller, Christoph ;
Fuenmayor, David
Value-Oriented Legal Argumentation in Isabelle/HOL
Abstract
Literature in AI & Law contemplates argumentation in legal cases as an instance of theory construction. The task of a lawyer in a legal case is to construct a theory containing: (a) relevant generic facts about the world, (b) relevant legal rules such as precedents and statutes, and (c) contingent facts describing or interpreting the situation at hand. Lawyers then elaborate convincing arguments starting from these facts and rules, deriving into a positive decision in favour of their client, often employing sophisticated argumentation techniques involving such notions as burden of proof, stare decisis, legal balancing, etc. In this paper we exemplarily show how to harness Isabelle/HOL to model lawyer’s argumentation using value-oriented legal balancing, while drawing upon shallow embeddings of combinations of expressive modal logics in HOL. We highlight the essential role of model finders (Nitpick) and "hammers" (Sledgehammer) in assisting the task of legal theory construction and share some thoughts on the practicability of extending the catalogue of ITP applications towards legal informatics.
BibTeX - Entry
@InProceedings{benzmuller_et_al:LIPIcs.ITP.2021.7,
author = {Benzm\"{u}ller, Christoph and Fuenmayor, David},
title = {{Value-Oriented Legal Argumentation in Isabelle/HOL}},
booktitle = {12th International Conference on Interactive Theorem Proving (ITP 2021)},
pages = {7:1--7:20},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-188-7},
ISSN = {1868-8969},
year = {2021},
volume = {193},
editor = {Cohen, Liron and Kaliszyk, Cezary},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2021/13902},
URN = {urn:nbn:de:0030-drops-139028},
doi = {10.4230/LIPIcs.ITP.2021.7},
annote = {Keywords: Higher order logic, preference logic, shallow embedding, legal reasoning}
}
