论文标题：Modelling Value-Oriented Legal Reasoning in LogiKEy

论文链接：https://www.mdpi.com/2813-0405/2/1/3

期刊名：Logics

期刊主页：https://www.mdpi.com/journal/logics

一、引言

法律推理尤其在疑难案件中，并非机械套用规则，还涉及对先例、事实和自由、平等、安全、效用等价值的权衡。要让计算机辅助法律论证，模型既要表示规则与事实，也需明确表达具体情境中不同价值之间的偏好关系。本文结合逻辑多元主义的知识工程方法与法律理论，运用 LogiKEy 和 Isabelle/HOL，对价值导向的法律权衡理论进行形式化建模，并以经典财产法中的野生动物案例加以检验。研究关注：如何将复杂的法律价值推理转化为可表示、可检验、可由计算机辅助评估的逻辑模型？

二、材料与方法

本文采用方法框架构建与案例分析，而非统计性实证。研究团队包括计算机科学研究者 Christoph Benzmüller、David Fuenmayor，以及法律学者和法律哲学家 Bertram Lomfeld；Lomfeld 提供法律领域知识并评估形式化结果的适切性。研究以其“论辩式正当化语法”为基础，按 LogiKEy 的分层架构建模：L0 为经典高阶逻辑（HOL）；L1 采用偏好模态逻辑表示情境相关的价值偏好；L2 构建法律价值推理的领域专用语言（DSL）；L3 将法律与世界知识及案件事实编码进系统。随后，研究利用 Isabelle/HOL 进行形式化编码与验证，并结合 Sledgehammer 自动定理证明和 Nitpick 模型检验，考察推理结论与前提之间的关系。

三、分析与结果

框架分析：LogiKEy 的主要特点是采用可调整的多层架构，把逻辑基础、偏好表示、法律理论和具体应用连接起来。L0 层以经典高阶逻辑（HOL）作为统一的元逻辑；L1 层选择偏好模态逻辑，表示不同价值在特定条件下的优先关系；L2 层将法律价值理论编码为可操作的领域专用语言；L3 层则用该语言对法律案例及其背景知识进行形式化表示和评估。除底层元逻辑外，其余建模层可以根据所处理的问题进行调整。

案例分析：文章首先分析 Pierson v. Post 案：Post 追逐狐狸，而 Pierson 最终捕获狐狸，双方因野生动物的所有权发生争议。研究将案情与相关法律知识编码进模型，并明确表示“实际占有的稳定性”（STAB）相对于“捕获意图”（WILL）的价值偏好。在给定规则和前提下，自动证明工具可检验支持判决结果的推导是否成立。作者也构建支持 Post 的反向论证，展示当法律解释或价值偏好改变时，系统如何重新评估结论。随后，文章分析 Conti v. ASPCA 案：鹦鹉 Chester 逃离 ASPCA 后被 Conti 捕获，ASPCA 随后要求取回。模型将原所有者持续承担照料责任（RESP）及其对动物的依赖关系（RELI），与当前的实际占有（STAB）进行比较，并在给定假设下验证支持 ASPCA 的推理。

验证与适用边界：形式化模型不只用于推出结论，也可检查假设的一致性，并借助自动证明、模型与反模型检验发现推理结构中的问题。论文对相关案例进行了形式化推导，并检查前提的一致性及价值冲突。需要注意的是，系统无法脱离输入前提独立判断现实案件：法律规则、事实、背景知识及价值偏好仍需领域专家建模与评估。自动证明说明结论能否由给定前提推出，并不能单凭证明过程保证前提在法律解释中必然正确。

四、讨论

基于形式化建模与案例分析，本文展现了以下几个方面的意义：

1.LogiKEy 通过分层架构，将高阶逻辑、非经典逻辑、法律理论与实际应用连接起来，为复杂知识的形式化表示提供了统一框架；

2.法律规则可以被重构为特定情境下不同价值原则之间的条件性偏好关系，使法律权衡中的价值依据更加明确；

3.定理证明和模型检验工具能够帮助研究者检查推理的有效性、前提的一致性，并支持对相反论证的分析；

4.计算机科学与法律哲学的跨学科合作，是将抽象法律理论转化为可验证形式化模型的重要条件；

5.该方法可作为研究法律推理、知识表示以及可信人工智能伦理与法律治理的试验平台，但其结果仍取决于形式化前提和领域知识的质量。

五、展望与结论

作者指出，LogiKEy 的多层建模方式并不局限于本文采用的特定对象逻辑；在适当调整的基础上，其思路也可延伸至其他证明助手和高阶逻辑自动推理系统。论文公开了相关 Isabelle/HOL 形式化代码，为其他研究者检查、复现和扩展模型提供了基础。未来工作可以在这一基础上继续丰富法律与世界知识的编码，探索更多类型的法律论证情境，并进一步研究形式化推理如何为可解释、可信且具备法律与伦理约束的智能系统提供支持。需要强调的是，论文呈现的是方法论与案例层面的探索，而不是已经能够替代法官或法律专业人士作出实际裁决的通用系统。

总体而言，这项研究展示了如何将价值导向的法律权衡理论转化为计算机能够处理和检验的形式化结构。通过 LogiKEy 的分层框架，法律规则、语境条件与价值偏好可以被明确表达，再由 Isabelle/HOL 及相关工具辅助开展定理证明、模型检验和案例评估。其重要贡献在于为法律理论、逻辑学和人工智能之间建立可操作的连接：既让价值推理的部分结构变得更加透明，也为分析法律论证的前提、结论及其相互关系提供了可验证的研究路径。

Benzmüller, C.; Fuenmayor, D.; Lomfeld, B. Modelling Value-Oriented Legal Reasoning in LogiKEy. Logics 2024, 2, 31–78. https://doi.org/10.3390/logics2010003.

期刊介绍

主编：Prof. Dr. Valentin Goranko, Logic and Theoretical Philosophy, Stockholm University, Stockholm, Sweden

Logics（ISSN 2813-0405）是由曼迪匹艾（MDPI）出版的国际开放获取期刊，2023年发行创刊号，按季度出版。期刊关注逻辑系统、逻辑方法与逻辑理论，涵盖数理逻辑、计算逻辑、哲学逻辑、逻辑与数学的历史及哲学，并收录逻辑在计算机科学、认知科学和语言学等领域的应用研究。