Laws must be understood and their application must be explained and justified. As such, they seem to be the perfect use case for (non-classical) automated reasoning. Indeed, there is much academic research in legal knowledge representation and reasoning. Nevertheless, there are no commercial reasoning-based applications, apart from legal expert systems. In this paper, we review some of the problems towards this goal and describe a possible solution.
Information systems are playing an important role in helping people in a wide range of tasks, ranging from searching to decision-making.
One area in which such tools can contribute is the legal domain: New court cases
and legislations are accumulated every day. In addition, international organizations like
the European Union are constantly aiming at combining and integrating separate legal
systems [
Approaches for searching over legal texts have long seen commercial success [
The most important application for these tools, though, is for capturing expertise.
Expert systems [
Nevertheless and despite their proven usefulness, expert systems are not widely used
in the legal domain. The main reason for that is the difficulty to capture the expert
knowledge within a computer program [
The second challenge is especially important as it affects the trust that can be placed
in the expert system. The more processing which is required, the less trust that can be
placed in the knowledge. Even systems which are created with a relatively flexible tool,
such a programming language, suffer from knowledge transformation. In their seminal
paper, Sergot et al. [
Both these challenges have been been the focus of research. The need of several domain
experts is dealt with mainly via no-code platforms, such as Neota Logic [
The second challenge is addressed by providing a richer language in which to capture
knowledge. Such systems are based on a reasoning engine, which tries to emulate actual
legal reasoning, and normally depend on non-classical logics such as Defeasible Deontic
[
These systems have the potential to overcome the main disadvantages of expert systems. By utilizing a more sophisticated reasoning engine, they allow for a more compact and faithful representation of the original legislation, while preserving the main advantages of expert systems.
Nevertheless, such systems have enjoyed little commercial success in the legal domain. The main goal of this paper is to investigate the reasons for that and to suggest remedies.
The most obvious shortcoming of such systems is their inability to address the first challenge. In fact, often, the richer the language is, the higher the need is for several domain experts.
This usability issue was identified to be one of the main requirement of expert systems
building tools (e.g. [
Various attempts have been done in order to make such tools more accessible to legal
practitioners via a more user-friendly interface. Logical English for example [
Another approach, demonstrated in [
A main additional disadvantage of all the approaches above is the lack of tools and
methodologies for asserting the correctness of the logical representations of the legal
texts. A discussion about the need can be found in [
Among existing validation results, one can find a methodology for building legal
ontologies [
To summarize, the above approaches underline a key issue in legal reasoning and
knowledge representation, which is the tension between the expressiveness of the knowledge and
the efficiency of reasoning over it [
Those approaches which use a programming language as the format for knowledge representation enjoy efficient reasoning but require a non-trivial translation in order to capture the nuances of the law. Moreover, while they are often capable of producing a proof, these proofs are not easily translated into legal arguments. On the other hand, approaches targeting the legal text directly, do not offer a direct reasoning engine.
In the next section, we focus on this tension and offer a possible solution - the use of
two different languages, one expressive and one efficient - and an automatic bidirectional
translation mechanism between them. This section builds on the works in [
This section is based on the meta-level annotations introduced in [
As discussed in the previous section, legal formalisms suffer from the tension between
expressiveness and efficient reasoning. This tension is captured by the following three
requirements [
General and extensible formats such as DAPRECO [
Both approaches would struggle with point (3). On the one hand, we expect the
formalization to be certified by a legal expert. On the other, both programming languages
and other formal formats require a programmer or a logician for the encoding. This gives
raise to methodologies for validation such as [
Maintaining the knowledge base requires the ability to track changes in the law and apply them to the formalization. Any encoding of the law which cannot be easily traced back to the original text would not be easily maintainable. The maintaining property can be directly linked to the need of an isomorphic translation, which maps a one-to-one relation between the original text and its formal version. Such isomorphism allows mapping back from the formal version to the original version and therefore to identify the elements in the formalism which would require a change. If the encoding requires a translation which is not isomorphic to the original text, tracing the result back would not be trivial.
It seems then than none of the current systems can support more than one of the requirements.
We propose a new approach for defining new systems, which follows the above reasoning. We identify point (3) above as the one currently not adequately supported by existing systems. We then propose a solution which meets the requirements of this point and develop the idea further in order to support the other two points.
An important point which is not directly covered by the above three points, but which is often mentioned in discussions with lawyers, is accountability. We consider this point as closely related to validation, as it qualifies what is a good validation process.
We will next introduce the basic idea of such an expressive language and claim that it can both represent faithfully the original text, as well as be easily maintainable.
We then go on to argue that it satisfies the different required properties.
If we consider the formalization processes as a function from legal texts to logical formulae, the maintainability requirement states that this function must be isomorphic. Given a formula, we should be able to generate the original text.
It seems that the only possible solution to that is to use a logic which is as expressive as the original text. This also implies point (1). If the logic is as expressive as the original, then regenerating the original text amounts to just pretty printing formulae. Using a logic of lower expressivity would cause any translation into original text to result in some level of information loss.
In order to define such a logic, we first need to understand what we try to formalize. Definition 1 (Legal interpretation). A legal interpretation of a legal text is defined as the interpretation of a legal expert with regard to a specific context problem. It should be noted that interpretations are usually subjective and context dependant.
In order to formalize legal interpretations in a formal language, we propose using the Legal Linguistic Templates (LLTs) language. This language is a general logical language and contains an interpreted logical connective for each foundational legal construct. Examples of such constructs are prohibitions and exceptions. The basic elements of the language are first-order atoms.
Using the above language, we can define formal interpretations of legal ones. Definition 2 (Formal interpretations). Given a legal interpretation L containing n statements, a formal interpretation for L is a set of n statements over an LLT language.
Before we move forward to the computational adequacy of the LLTs language, we
would like to mention that within the terminology of programming languages [
By choosing an LLTs language which is expressive enough to describe a “good” formal interpretation of a legal text, we seem to go further away from computational adequacy. We now show that this is not necessarily the case.
We achieve that by following the "shallow semantical embeddings" defined by Benzmüller
[
If the logic M that we choose is computationally adequate, then we effectively obtain the computational adequacy of L. This is achieved in practice by applying the shallow semantical embedding, and then applying software for the computationally adequate result.
The logic chosen by Benzmüller is Higher-order Logic [29] and the various software
which can be used to reason over the embeddings include Isabelle/HOL [
The LLTs languages we have used so far seems to be too general for the use of shallow semantical embeddings. We will next generalize the notion of a "shallow semantical embedding".
Definition 3 (Embedding functions). An embedding function φ of a logic L into a logic M, is a total function from L to M.
Definition 4 (Adequate meta-logics). An adequate meta-logic is a computationally adequate logic, into which an embedding function from another logic exists.
For example, first-order logic with negation interpreted as negation-as-failure (NAF) [31] is computationally adequate as embeddings in this language can be executed in Prolog [32].
Assuming that our LLTs language contains a connective for prohibition and another for exceptions, we can describe the following embedding function into a first-order logic with NAF.
• φ(∅) =⇒ ∅ • φ(S ∪ {GeneralProhibition(B)}) =⇒ prohibited(φ({B})) ∪ φ(S) • φ(S ∪ {Exception(A,B), LabeledStatement(A,C)}) =⇒ {not φ({B}) φ({C})} ∪ φ(S) ⇒ Note that the resulted set denotes a set of first-order formulae. A standard normalization can be used in order to obtain a logic program where arguments of atoms are universally quantified on the level of the whole program. The function symbol prohibited is uninterpreted.
Having the embedding, we can now use Prolog in order to compute various properties. To check for violations of the prohibition, for example, one would need to add Prolog facts and then check if prohibited(_) can be derived.
The last requirement of a legal formalization language is to have a good validation process, which can ensure that legal experts be held accountable.
The approach taken in order to meet this requirement follows a very basic idea in programming languages, that of a pretty printer [33]. Pretty printing takes a formal structure, such as an LLT formula, and presents it in a user friendly form.
While the concept is basic, it turns out to be very powerful in the legal domain. By printing an LLT formula as a legal statement in English, we effectively translate it back into the original legislation language. This feature allows a legal expert to compare the two versions of the legislation - the original and the pretty printed one - and to make a decision regarding its validity. This decision can be made even when the legal expert does not have any knowledge in logic and has not participated in the generation of the LLT formulae.
In this section we describe an implementation of the LLTs language. The goal of the implemented LegAi annotation editor is to support annotating legal texts with LLTs. At the same time, the editor supports the validation mechanism described earlier in the paper by providing legal experts with a comparison of the original and generated text.
The editor can be found online2 and requires a registration. After registration, the editor displays a message that an email to activate the account must be sent to the code maintainer, who associates the new user to a specific account with specific rights.
Once logged in, the user has the ability to paste legal texts into an annotation editor. The user starts with selecting a sentence they wish to annotate and then a (top-level) LLT wizard opens. The wizard guides the user in the annotation process, shows the possible/required LLTs that can/must be nested.
The LLT language contains one “leaf” LLT, called Atom, which can be instantiated with all possible vocabulary. The wizard ensures that annotations are always syntactically correct.
When selecting a specific vocabulary, the wizard allows selection of all parameters, according to their type. The user has control over how to generate or choose variables for the vocabulary and its parameters.
Once a top-level LLT was created, the user can click on the annotation and see a tree structure corresponding to the formal version of the text.
A list of all vocabulary and their associated legal texts appear on a separate tab.
An example of annotating two simplified articles of the GDPR is shown on the top of Fig. 1.
In order to check if an annotation captures correctly the meaning of a legal sentence, the user can view the formal tree structure, as defined in the previous section and shown on the middle of the figure.
Nevertheless, such a formal structure is not easily readable by non-logicians. In order to rectify that, a feature called reverse translation, which implemented the pretty printer approach, was added to the editor.
The reverse translation, which is accessible on a separate tab, generates a legal text from the formal tree structure. It then places the reversely generated text next to the original text. The user can then compare the two versions and decide if the formal version correctly captures the meaning of the original one, as shown on the bottom of the figure. Since our vocabulary is denoted via first-order terms, each contains both a name and a set of parameters. In the reverse translation, we display the name only, while hovering over the text shows all the used parameters.
In this paper we have considered the creation of formal interpretations of legal texts. This problem is one of the main ones preventing automated reasoning from being more utilized and commercialized.
We have discussed the main current approaches and identified several requirements which need to be addressed. We then defined a language, called LLTs, which we argue satisfies all the requirements.
This language is implemented in an online tool called the LegAi editor, which is briefly introduced.
The work done in this paper aims at getting legal experts involved in the creation of legal knowledge. Towards this goal, we currently collaborate with a German GDPR consultancy firm. First impressions show that the creation of legal knowledge by a non-technical legal expert is possible via the annotations editor and wizard. They also confirm that a comparison tool can help the validation of the formal interpretations and therefore raise the possibility of accountability.
Our direct future work is to implement a set of computational tools which can take advantage of the created formal interpretations. We are currently developing a tool which can help the different consultants of the firm attain uniformity of legal advice by using the tool to guide them in the consultancy process. [29] A. Church, A formulation of the simple theory of types, The journal of symbolic logic 5 (1940) 56–68. [30] A. Steen, C. Benzmüller, The higher-order prover leo-iii, in: International Joint
Conference on Automated Reasoning, Springer, 2018, pp. 108–116. [31] K. L. Clark, Negation as failure, in: Logic and data bases, Springer, 1978, pp.
293–322. [32] A. Colmerauer, An introduction to prolog iii, in: Computational Logic, Springer, 1990, pp. 37–79. [33] J. Hughes, The design of a pretty-printing library, in: International School on Advanced Functional Programming, Springer, 1995, pp. 53–96.