Benzmüller, ChristophChristophBenzmüller0000-0002-3392-3093Fuenmayor, DavidDavidFuenmayor0000-0002-0042-4538Lomfeld, BertramBertramLomfeld2024-03-152024-03-1520242813-0405https://fis.uni-bamberg.de/handle/uniba/94348The logico-pluralist L OGI KE Y knowledge engineering methodology and framework is 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 illustrative property law cases (involving the appropriation of wild animals) within the Isabelle HOL proof assistant system, illustrating how L OGI KE Y 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. Modelling value-oriented legal reasoning in that framework, we establish novel bridges between the latest research in knowledge representation and reasoning in non-classical logics, automated theorem proving, and applications in legal reasoning.englegal balancing; value-oriented reasoningautomated theorem provinglogical pluralismproof assistantsIsabelle/HOL004article10.3390/logics2010003https://www.mdpi.com/2813-0405/2/1/3/pdf