The proposed tutorial is intended to make people from the law community acquainted with formal tools for efficient and automated reasoning on legal texts.
How can computers aid legal practitioners in their work? The interpretation of legal texts and regulations depends on many factors such as experience and context. Nevertheless, once an interpretation is given, a computer can help in several ways:
The help of a computer is not only limited to the three points described above. For example, once an interpretation is given, a computer can be used in order to visualize all possible normative paths and can therefore help judges to avoid choosing a path which does not follow their interpretation. Or, it can be used in order to look for information, such as evidence, which can help making a correct normative decision. However, in this tutorial we are going to focus only on the three points described above since they are supported by the current version of the NAI tool.
What software do I need in order to use the NAI tool? The tool is a web application, which means that the only software required is a browser, such as Firefox or Chrome.
What knowledge and skills are required in order to be able to use the NAI tool? Clearly, the most important task is the interpretation of the text. We believe that any tool whose goal is to aid legal practitioners must make this task as easy as possible. At the same time, giving an interpretation which is unambiguous and formal enough, so that it can be used in order to answer relevant questions, requires one's understanding of a formal language. This is the main task of the tutorial's first two sessions. Once an interpretation is formalized within the tool, the computer can be used in order to support the three operations described above. The use of this part of the tool is handled in the third session of the tutorial.
Consider the Regulation (EC) No 593/2008 of the European Parliament and of the Council of 17 June 2008 on the law applicable to contractual obligations (Rome I). This regulation specifies different situations and cases which should affect the law used in contracts. In this example we focus on articles 3 and 4.
Article 3 - Freedom of choice
Article 4 - Applicable law in the absence of choice
Our main task is the formalization of the above norms. In order to make this task as simple and intuitive as possible, we have chosen to support it via annotations.
The tutorial consists of four lectures
This lecture will introduce the audience to propositional normal modal logic used to represent normative reasoning. It will focus on two specific logical systems: SDL (Standard Deontic Logic) and DL*.
We will show how the system DL* can be used to formalize certain aspects of legal documents. This lecture will present the audience with the NAI graphical tool and the basics of legal text formalization.
This lecture will present the field of automated reasoning. It will describe the capabilities of automated theorem proving and will introduce the audience to the automated features of NAI
In the last lecture the participants will use the NAI tool in order to first formalize a legal text and to get automatic answers to questions of various kind.
The tutorial and web application are based on the following works and tools.