The proposed tutorial is intended to make people from the law community acquainted with formal tools for efficient and automated reasoning. Particular emphasis will be put on the use of theorem provers for reasoning on legal texts. The tutorial will cover all steps required: the translation of natural language sentences taken from the texts into formulas of a logical language, the conceptual analysis of the deontic notions defined in the logical language and the actual use of theorem provers. The main goal is to add automated theorem provers to the inventory of tools that can be used by people dealing with the law.
The tutorial consists of four lectures
This lecture will introduce the audience to propositional normal modal logic and to two specific logics, the Standard Deontic Logic (SDL) and the DL* logic.
The DL* logic is suitable for the formalization 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 then answer, fully automatically, several different questions.
To appear soon...