Document Open Access Logo

Value-Oriented Legal Argumentation in Isabelle/HOL

Authors Christoph Benzmüller , David Fuenmayor

PDF
Thumbnail PDF

File

LIPIcs.ITP.2021.7.pdf
  • Filesize: 2.39 MB
  • 20 pages

Document Identifiers

Author Details

Christoph Benzmüller
  • Freie Universität Berlin, Germany
David Fuenmayor
  • University of Luxembourg, Luxembourg
  • Freie Universität Berlin, Germany

Acknowledgements

We thank Bertram Lomfeld for encouraging us to take on this challenge; we also thank the anonymous reviewers for their valuable feedback.

Cite AsGet BibTex

Christoph Benzmüller and David Fuenmayor. Value-Oriented Legal Argumentation in Isabelle/HOL. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 7:1-7:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.ITP.2021.7

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.

Subject Classification

ACM Subject Classification
  • Computing methodologies → Knowledge representation and reasoning
Keywords
  • Higher order logic
  • preference logic
  • shallow embedding
  • legal reasoning

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Isabelle/HOL sources for this formalisation work. http://logikey.org, 2021. Subfolder: URL: https://github.com/cbenzmueller/LogiKEy/tree/master/Preference-Logics/EncodingLegalBalancing.
  2. Trevor J. M. Bench-Capon. The missing link revisited: The role of teleology in representing legal argument. Artificial Intelligence and Law, 10(1-3):79-94, 2002. Google Scholar
  3. Trevor J. M. Bench-Capon. HYPO’s legacy: introduction to the virtual special issue. Artificial Intelligence and Law, 25(2):205-250, 2017. Google Scholar
  4. Trevor J. M. Bench-Capon. The need for good old-fashioned AI and Law. In W. Hötzendorfer, C. Tschol, and F. Kummer, editors, In International Trends in Legal Informatics: A Festschrift for Erich Schweighofer. Weblaw AG, 2020. Google Scholar
  5. Trevor J. M. Bench-Capon and Giovanni Sartor. A model of legal reasoning with cases incorporating theories and value. Artificial Intelligence, 150:97-143, 2003. Google Scholar
  6. Christoph Benzmüller. Cut-elimination for quantified conditional logic. Journal of Philosophical Logic, 46(3):333-353, 2017. URL: https://doi.org/10.1007/s10992-016-9403-0.
  7. Christoph Benzmüller. Universal (meta-)logical reasoning: Recent successes. Science of Computer Programming, 172:48-62, 2019. URL: https://doi.org/10.1016/j.scico.2018.10.008.
  8. Christoph Benzmüller, Ali Farjami, Paul Meder, and Xavier Parent. I/O logic in HOL. Journal of Applied Logics - IfCoLoG Journal of Logics and their Applications (Special Issue: Reasoning for Legal AI), 6(5):715-732, 2019. Google Scholar
  9. Christoph Benzmüller, Ali Farjami, and Xavier Parent. Åqvist’s dyadic deontic logic E in HOL. Journal of Applied Logics - IfCoLoG Journal of Logics and their Applications (Special Issue: Reasoning for Legal AI), 6(5):733-755, 2019. Google Scholar
  10. Christoph Benzmüller, Ali Farjami, and Xavier Parent. Dyadic deontic logic in hol: Faithful embedding and meta-theoretical experiments. In Matthias Armgardt, Hans Christian Nordtveit Kvernenes, and Shahid Rahman, editors, New Developments in Legal Reasoning and Logic: From Ancient Law to Modern Legal Systems, volume 23 of Logic, Argumentation & Reasoning. Springer Nature Switzerland AG, 2021. URL: https://doi.org/10.1007/978-3-030-70084-3.
  11. Christoph Benzmüller, David Fuenmayor, and Bertram Lomfeld. Encoding legal balancing: Automating an abstract ethico-legal value ontology in preference logic, 2020. Workshop on Models of Legal Reasoning (MLR 2020), hosted by 17th Conference on Principles of Knowledge Representation and Reasoning (KR 2020). Unpublished paper available at: URL: https://www.researchgate.net/publication/342380027.
  12. Christoph Benzmüller and Bertram Lomfeld. Reasonable machines: A research manifesto. In Ute Schmid, Franziska Klügl, and Diedrich Wolter, editors, KI 2020: Advances in Artificial Intelligence - 43rd German Conference on Artificial Intelligence, Bamberg, Germany, September 21–25, 2020, Proceedings, volume 12352 of Lecture Notes in Artificial Intelligence, pages 251-258. Springer, Cham, 2020. URL: https://doi.org/10.1007/978-3-030-58285-2_20.
  13. Christoph Benzmüller, Xavier Parent, and Leendert van der Torre. Designing normative theories for ethical and legal reasoning: LogiKEy framework, methodology, and tool support. Artificial Intelligence, 287:103348, 2020. URL: https://doi.org/10.1016/j.artint.2020.103348.
  14. Christoph Benzmüller and Lawrence C. Paulson. Multimodal and intuitionistic logics in simple type theory. The Logic Journal of the IGPL, 18(6):881-892, 2010. URL: https://doi.org/10.1093/jigpal/jzp080.
  15. Christoph Benzmüller and Lawrence C. Paulson. Quantified multimodal logics in simple type theory. Logica Universalis (Special Issue on Multimodal Logics), 7(1):7-20, 2013. URL: https://doi.org/10.1007/s11787-012-0052-y.
  16. Donald Berman and Carole Hafner. Representing teleological structure in case-based legal reasoning: the missing link. In Proceedings 4th ICAIL, pages 50-59. New York: ACM Press, 1993. Google Scholar
  17. Jasmin C. Blanchette, Sascha Böhme, and Lawrence C. Paulson. Extending Sledgehammer with SMT solvers. Journal of Automated Reasoning, 51(1):109-128, 2013. Google Scholar
  18. Jasmin C. Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, and Josef Urban. Hammering towards QED. Journal of Formalized Reasoning, 9(1):101-148, 2016. Google Scholar
  19. Jasmin C. Blanchette and Tobias Nipkow. Nitpick: A counterexample generator for higher-order logic based on a relational model finder. In Matt Kaufmann and Lawrence C. Paulson, editors, ITP 2010, volume 6172 of LNCS, pages 131-146. Springer, 2010. Google Scholar
  20. Craig Boutilier. Toward a logic for qualitative decision theory. In Principles of knowledge representation and reasoning, pages 75-86. Elsevier, 1994. URL: https://doi.org/10.1016/B978-1-4832-1452-8.50104-4.
  21. David Fuenmayor. Topological semantics for paraconsistent and paracomplete logics. Archive of Formal Proofs, 2020. , Formal proof development. URL: https://isa-afp.org/entries/Topological_Semantics.html.
  22. Bernhard Ganter and Rudolf Wille. Formal concept analysis: mathematical foundations. Springer Berlin, 2012. Google Scholar
  23. Thomas F. Gordon and Douglas Walton. Pierson vs. Post revisited. Frontiers in Artificial Intelligence and Applications, 144:208, 2006. Google Scholar
  24. Joseph Y. Halpern. Defining relative likelihood in partially-ordered preferential structures. Journal of Artificial Intelligence Research, 7:1-24, 1997. Google Scholar
  25. Robert Koons. Defeasible Reasoning. In Edward N. Zalta, editor, The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, winter 2017 edition, 2017. Google Scholar
  26. P. Krause, S. Ambler, Elvang-Goransson, M., and J. Fox. A logic of argumentation for reasoning under uncertainty. Computational Intelligence, 1995. URL: https://doi.org/10.1111/j.1467-8640.1995.tb00025.x.
  27. Fenrong Liu. Changing for the better: Preference dynamics and agent diversity. PhD thesis, Institute for Logic, Language and Computation, Universiteit van Amsterdam, 2008. Google Scholar
  28. Fenrong Liu. Reasoning about Preference Dynamics. Springer Netherlands, 2011. URL: https://doi.org/10.1007/978-94-007-1344-4.
  29. Bertram Lomfeld. Die Gründe des Vertrages: Eine Diskurstheorie der Vertragsrechte. Mohr Siebeck, Tübingen, 2015. Google Scholar
  30. Bertram Lomfeld. Grammatik der Rechtfertigung: Eine kritische Rekonstruktion der Rechts(fort)bildung. Kritische Justiz, 52(4), 2019. Google Scholar
  31. Juliano Maranhão and Giovanni Sartor. Value assessment and revision in legal interpretation. In Proceedings of the Seventeenth International Conference on Artificial Intelligence and Law, ICAIL 2019, Montreal, QC, Canada, June 17-21, 2019, pages 219-223, 2019. URL: https://doi.org/10.1145/3322640.3326709.
  32. L. Thorne McCarty. An implementation of Eisner v. Macomber. In Proceedings of the 5th International Conference on Artificial Intelligence and Law, pages 276-286, 1995. Google Scholar
  33. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL: A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002. Google Scholar
  34. Henry Prakken. An exercise in formalising teleological case-based reasoning. Artificial Intelligence and Law, 10(1-3):113-133, 2002. Google Scholar
  35. Henry Prakken and Giovanni Sartor. Law and logic: A review from an argumentation perspective. Artificial Intelligence, 227:214-225, 2015. Google Scholar
  36. Edwina L. Rissland and Kevin D. Ashley. A case-based system for trade secrets law. In Proceedings of the 1st international conference on Artificial Intelligence and Law, pages 60-66, 1987. Google Scholar
  37. Johan van Benthem, Patrick Girard, and Olivier Roy. Everything else being equal: A modal logic for ceteris paribus preferences. J. Philos. Log., 38(1):83-125, 2009. URL: https://doi.org/10.1007/s10992-008-9085-3.
  38. Georg Henrik von Wright. The logic of preference. Edinburgh University Press, 1963. Google Scholar
  39. Makarius Wenzel. Isabelle/Isar—a generic framework for human-readable proof documents. From Insight to Proof-Festschrift in Honour of Andrzej Trybulec, 10(23):277-298, 2007. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact