| Departments |
Computer Science, Zienkiewicz Institute for Modelling, Data and AI
|
|---|
| Description | Since the 1980s, encoding natural language expressions of legal rules (norms) into precise logical, codable representations has been a key ambition of AI and Law, wherein AI concepts and techniques are applied to legal information and processes.
Progress has been made in encoding laws in Prolog (Logic Programming), and there are several available samples (see preparation)
Such encodings facilitate: access to legal information, drawing determinations, and compliance checking. For instance, a citizen might input their details and find out what benefits they are eligible for; companies could determine if they are compliant with the law.
One challenge has been to facilitate the encoding pipeline, that is, the process of encoding natural language formally and checking that it is correct. LLMs can be useful here and are the subject of active research.
This project would be done in conjunction with several colleagues in the Theory Group at Swansea University Department of Computer Science.
Another challenge has been to apply formal methods to the encodings so as to be able to flexibly prove theorems about the domain. We propose using Rocq-elpi: Rocq is a powerful interactive theorem prover, and ELPI is a higher-order logic programming language. These can be the formal language in which to encode and reason with rich representations of the law.
Recent research reports progress in encoding the law using other theorem provers and encodings (Isabelle/Higher-order Logic), using the LogiKey method, which provides us with something of a roadmap for this project
ROCQ-elpi.
The student will have the opportunity to get involved a rapidly growing AI area of electronic processing of legal documents. We will start small and build up.
The project will be done in collaboration with colleagues in the Theory group - Mukesh Tiwari and Anton Setzer |
|---|
| Preparation | Indicative Background
Logic Programming for Large Scale Applications in Law (1987)
https://www.google.com/url?sa=t&source=web&rct=j&opi=89978449&url=https://cgi.csc.liv.ac.uk/~tbc/publications/ICAIL87supp.pdf
Prolog encodings of law (on SWISH and using Logical English, which translates into Prolog)
https://logicalenglish.logicalcontracts.com/example/LogicalEnglish.swinb
Logical English repo
https://github.com/LogicalContracts
Rocq-elpi
* Rocq is an interactive theorem prover for automated reasoning
* ELPI is an embeddable λProlog interpreter
https://rocq-prover.org/
https://rocq-prover.org/p/rocq-elpi/latest
Modelling Value-Oriented Legal Reasoning in LOGIKEY. Benzmüller, Fuenmayor, Lomfeld. 2024
https://www.mdpi.com/2813-0405/2/1/3 |
|---|
| Project Categories |
Artificial Intelligence (AI), Law, Modelling, Theorical Computer Science |
|---|
| Project Keywords |
Logic, Programming Languages, Proofs |
|---|
Level of Studies
|
| Level 6 (Undergraduate Year 3) |
yes
|
|---|
| Level 7 (Masters) |
yes
|
|---|
| Level 8 (PhD) |
yes
|
|---|