FMitF: Track 2: Formal Reasoning for Legal Conveyances

律师们起草了管理财产转移的被称为“转让书”的文件。这些转让书是以复杂的语法编写的，遵循严格的规则。在之前的工作中，调查人员开发了一个读取标准运输工具并计算其后果的系统。本项目扩展了这项初步工作，将其推广到更广泛的运输工具，并增加了一个无障碍的图形界面。该项目的创新之处在于将编程语言和形式方法领域的想法引入法律领域的问题。该项目的影响是创建一个系统，律师和法律教育工作者可以使用它来推理复杂的交易，并了解管理它们的法律是如何运作的。在技术层面，该系统将交易语言建模为特定于领域的编程语言，其具体语法是起草律师使用的法律英语的有限子集。它将传输解析为抽象语法树，然后根据正式的操作语义对其进行转换，以说明后续事件。图形界面提供了在事件中前进和后退等功能，使没有计算机科学背景的用户能够吸收基于语言的方法提供的见解。该项目开发了更丰富的事件模型，使该系统能够对事件与律师和法官用来解决纠纷的运输工具之间的相互作用进行自动推理。最后，调查人员将在课堂上部署该系统，开发一系列探索物权法主要要素的练习。这一奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

Lawyers draft documents called "conveyances" that govern the transfer of property. These conveyances are written in an intricate syntax that follows precise rules. In previous work, the investigators developed a system for reading standard conveyances and computing their consequences. The present project extends that preliminary work by generalizing it to cover a wider range of conveyances and adding an accessible graphical interface. The project's novelties are in bringing ideas from the fields of programming languages and formal methods to bear on problems in the legal domain. The project's impacts are to create a system that can be used by lawyers and legal educators to reason about complex conveyances and to understand how the laws governing them work.At a technical level, the system models the language of conveyances as a domain-specific programming language whose concrete syntax is a restricted subset of the legal English used by the lawyers who draft them. It parses a conveyance into an abstract syntax tree, which it then transforms according to a formal operational semantics to account for subsequent events. A graphical interface provides features such as stepping forward and backward through events, enabling users without a background in computer science to absorb the insights offered by the language-based approach. The project develops a richer model of events, enabling the system to engage in automated reasoning about interactions between events and conveyances that are used by lawyers and judges to settle disputes. Finally, the investigators will deploy the system in the classroom, developing a series of exercises that explore the main elements of property law.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.