FMitF: Track 2: Formal Reasoning for Legal Conveyances

点击翻译按钮获取中文摘要

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.