Value-oriented Legal Reasoning in LogiKEy: Methodology and Case Study

The logico-pluralist LogiKEy knowledge engineering methodology and framework is exemplarily applied to the modelling of a theory of legal balancing in which legal knowledge (cases and laws) is encoded by utilising context-dependent value preferences. The theory obtained is then used to formalise, automatically evaluate, and reconstruct prominent property law cases (involving appropriation of wild animals) within the Isabelle/HOL proof assistant system. This illustrates how LogiKEy can harness interactive and automated theorem proving technology to provide a testbed for the development and formal verification of legal domain-specific languages and theories. With the work reported here we establish novel bridges between latest research in knowledge representation and reasoning in non-classical logics, automated theorem proving, and applications in legal reasoning.