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.