Legal Debugging in Propositional Legal Representation

Abstract

Literal interpretation on laws may produce unexpected consequences. They are difficult to be recognized unless exceptional cases were taken to the court. The court may decide a literal interpretation as exceptional, and then they have to identify which rule is a source of exception.

To assist the court, we proposed an idea called legal debugging, to find out which rule condition, called a culprit, causes unexpected consequences in such exceptional cases. We adapt the algorithmic program debugging with consideration of characteristics in reasoning in judgement, such as non-recursive stratified structures and factual propositions in order to find a culprit at last.

This paper presents legal debugging in propositional Prolog as well as PROLEG (PROlog based LEGal reasoning support system) specialized for legal reasoning. An example of legal debugging that interacts with a user and finds a culprit is also shown under the PROLEG representation of the case adapted from the real Supreme Court case.

1 Introduction

Researchers have long been interested in representing legal knowledge in computers. Legal knowledge representation is usually divided into two types: rule-based and case-based. In rule-based legal representation, which is usually used for statutory laws, Legal rules are represented in logic programs such as Prolog [1, 2]. By formalizing the statute rules into computational logic, it provides benefits such as detecting conflicts in legal systems [3].

However, statute laws may be flawed. Even statute laws are cautiously drafted; some issues might be missing. These missing issues lead to unexpected consequences when we interpret the law literally. These issues are usually tacit, meaning that they are hard to know until such exceptional cases happen. When the cases are taken to the court, the court decided that the literal legal interpretation produces an unexpected consequence. The court has to identify which rule is a source of unexpected consequence and the court currently manually identifies such a rule so they might miss some sources of the unexpected result since exhaustive consideration might not be guaranteed.

Therefore, in this paper, we propose an idea of legal debugging, to find legal conditions that cause unexpected consequence, by imitating computer program debugging. In contrast with legal conflicts that deal with other legal rules written explicitly, legal debugging has to deal with tacit expectations from the courts or the legal experts. This paper tries to identify the existence of unexpected consequences from those tacit expectations and propose legal debugging as a potential way to realize and solve unexpected consequences from laws.

In this paper, we report legal debugging based on algorithmic debugging, which originally proposed for tracing the difference between computation result from the program and expectation result from the user. Our technique traces the difference between a literal interpretation from the legal representation and an expected interpretation from legal experts. At this preliminary step of legal debugging development, we only focus on representation of statute laws which express the laws in written forms. This paper considers legal representations under propositional logic which is the basis of more advanced legal representations. We also take into account of characteristics of reasoning in judgements. For example, the logic rules should be stratified and not recursive so there would be only one interpretation which satisfies the rules.

This paper provides the means to find a legal bug, called a culprit, in two propositional based legal representations. The first representation in this paper is Prolog, which is more familiar to logic programmers. Although Prolog is not designed specifically for laws, a number of law formalizations have been tested in Prolog such as British Nationality Act [1] and the Income Tax Act of Canada [2]. The second representation this paper is PROLEG which stands for PROlog based LEGal reasoning support system [4]. PROLEG uses the concept of exception instead of negation which is more suitable to laws which usually separate between conditions and exceptions in legal documents. PROLEG was implemented based on the Presupposed Ultimate Fact Theory of Japanese Civil code, a legal reasoning scheme in real legal practice [5].

This paper is structured as follows. Section 2 describes propositional legal representation in logic program with negation as failure and defines a legal debugging process under the semantics. Section 3 extends the legal debugging process under the PROLEG semantics. Section 4 demonstrates a legal debugging under PROLEG using the Supreme Court case. Section 5 compares legal debugging and other related works on debugging. The final section summarizes the idea of legal debugging and its application in future works.

2 Legal Debugging Under Prolog

Prolog is a well-known logic programming based on a logic program with negation as failure. Generally, a logic program with negation as failure consists of rules in the form described as follows.

2.1 Basic Definitions

Definition 1.

[Rule] A logic program with negation as failure is a finite set of rules Π which each element of Π is a rule R in the form h ← b₁,…,b_n, not c₁,…, not c_m where h, b_i (1 ≤ i ≤ n), and c_j (1 ≤ j ≤ m) are propositions.

We denote h as head(R), {b₁,…,b_n} as pos_body(R), {c₁,…,c_m} as neg_body(R), and body(R) as pos_body(R) $\cup$ neg_body(R). We call a rule without a body a fact.

Definition 2.

[Active rules] Let M be a set of propositions and Π be a logic program with negation as failure. A set of active rules of Π w.r.t. M denoted as Π^M is a set of {head(R) ← pos_body(R) | for all R ∈ Π such that neg_body(R) $\cap$ M = ∅}.

Definition 3.

[Satisfaction] Let M be a set of propositions and R be a rule. M satisfies R if the following condition is satisfied: if pos_body(R) ⊆ M then head(R) ∈ M.

Definition 4.

[Stable Model] Let Π be a logic program and M be a set of propositions. M is a stable model of Π if M is a minimum model of Π^M.

If M satisfies every rule in Π^M, M is a model of Π^M. The minimum model of Π^M is a model of Π^M which is the minimum in the sense of set inclusion.

Example 1.

The following example shows a logic program with negation as failure P.

• $\begin{array}{*{20}l} {p \leftarrow not\,q.} \hfill \\ {p \leftarrow not\,f.} \hfill \\ {q \leftarrow not\,r.} \hfill \\ {r \leftarrow f.} \hfill \\ {f \leftarrow .} \hfill \\ \end{array}$

Let M be {f, r, p}, a set of active rules of P w.r.t. M or P^M is

• $\begin{array}{*{20}l} {p \leftarrow .} \hfill \\ {r \leftarrow f.} \hfill \\ {f \leftarrow .} \hfill \\ \end{array}$

Which M satisfies every rules in P^M and M is the minimum set that can do such things according to P^M. Therefore, M is a stable model of P.

Two assumptions from legal reasoning are introduced to distinguish the propositional legal representation from general logic programs. First assumption is that, generally, legal rules are not recursive. Recursive rules are those rules whose dependency graph contains a loop (see details in [6]). For example {p ← p.}, {p ← not p.}, {p ← q. q ← p.} are recursive, but the program in Example 1 is not recursive. It is proved in [7] that a non-recursive program consists of only one stable model.

Definition 5.

[Non-recursive program] A logic program Π is non-recursive when there is a partition Π = Π₀ $\cup$ Π₁ $\cup$ … $\cup$ Π_n (Π_i and Π_j disjoint for all i ≠ j) such that, for a predicate p appears in a body of rule in Π_i then a rule with p in the head is only contained within Π₀ $\cup$ Π₁ $\cup$ … $\cup$ Π_j where j < i.

Second assumption is that some legal propositions are factual. Their truth values are usually evidence based so the court will finalize their truth values in a phase of fact finding and shall not reverse their truth values after that. Hence, such propositions are true only when given. From Example 1, f is factual because there is no rule that implies f (except a fact f ← .) so its truth value cannot be changed by altering other propositions. factual is defined as follows.

Definition 6.

[Factual] A proposition α is factual w.r.t. a program Π if there is no rule that implies α except a fact α ← ., in other words, α shall be true only when given.

However, some propositions could not be true concurrently. From Example 1, if r was true, q could not be true. We could say that {r} (or any sets that contain r) does not support q. To determine this relation between rules and a set of propositions, the idea of support is defined as follows.

Definition 7.

[Support] A set of propositions S supports a proposition α w.r.t. a logic program Π if there is a rule R ∈ Π such that α is the head of the rule (α = head(R)), pos_body(R) ⊆ S, and neg_body(R) $\cap$ S = ∅. R is called a supporting rule of α w.r.t. S.

Theorem 1.

[Relation between model and support] Given Π as a non-recursive logic and M is a stable model of Π, α ∈ M if and only if M supports α w.r.t. Π. (This relation is common. For further details, please see [8].

Proof

Suppose M supports α but α $\notin$ M, there is a supporting rule R of α in Π.

• Hence α = head(R), pos_body(R) ⊆ M and neg_body(R) $\cap$ M = ∅.

• But since α $\notin$ M, M does not satisfy head(R) ← pos_body(R) which exists in Π^M.

• It leads to contradiction with the definition of model.

Suppose M does not support α but α ∈ M, then no rules are supporting α.

• Thus, M - {α} must be a model because it satisfies every rule in Π^M.

• It leads to contradiction with the definition of the minimum model.

2.2 Formalizing Unexpected Consequences and Culprits

When the literal interpretation gives unexpected consequences, it means that we do not agree with the current stable model. However, the intended interpretation is not known explicitly in the first place but it rather reveals proposition by proposition when we consider the truth value of each proposition together with the debugger until we find a culprit defined to be a root cause of unexpected consequences.

However, because truth values of factual propositions are already finalized, the true factual proposition would not be possible to be excluded from the stable model and the false factual proposition would not be possible to be included in the stable model.

From Example 1, we could not intend {p, r} to be a stable model because f is already given and we could not change its truth value. In contrast, we could intend {p, f} to be the stable model because r is not factual so we allow changing the truth value of r. Therefore, we define an intended interpretation denoted as IM with following definitions.

Definition 8.

[Intended interpretation] An intended interpretation IM of a non-recursive logic program Π is a set of propositions such that a set of factual propositions in the stable model of Π and a set of factual propositions in IM are equal.

Consequently, if IM is different from the stable model, there must be a non-factual α that is not currently derived but intended to be derived or currently derived but intended not to be derived. We call such propositions as unexpected which is defined as follows.

Definition 9.

[Unexpected proposition] A proposition α is unexpected w.r.t. an intended interpretation IM and a non-recursive logic program Π with a stable model M if (1) α $\notin$ M but α ∈ IM or (2) α ∈ M but α $\notin$ IM. Factual propositions could not be unexpected due to constraints in Definition 8.

To modify the program so its stable model would become what we intend, we must work on a non-factual proposition called culprit defined as follows.

Definition 10.

[Culprit] a non-factual proposition α will be a culprit w.r.t. an intended interpretation IM and a logic program Π if

• α ∈ IM but IM does not support α w.r.t. Π or

• α $\notin$ IM but IM supports α w.r.t. Π.

Then, we get the following theorem.

Theorem 2.

[Finding a culprit] Given Π as a non-recursive logic program with a stable model M and IM as an intended interpretation that not equal to M. If α is unexpected w.r.t. IM and Π and α is not a culprit w.r.t. IM and Π, then there is another unexpected proposition β ≠ α in a body of a rule that implies α.

Proof

If α ∈ IM and α is not a culprit

• Then there is a rule R supporting α w.r.t. IM.

• Hence, pos_body(R) ⊆ IM and neg_body(R) $\cap$ IM = ∅.

• But α $\notin$ M so R is not a supporting rule of α w.r.t. M.

• Thus, pos_body(R) ⊄ min(Π) or neg_body(R) $\cap$ min(Π) ≠ ∅.

• Because Π is non-recursive, α $\notin$ body(R)

• Hence, there is another proposition β₁ ∈ pos_body(R) such that β₁ ∈ IM and β₁ $\notin$ M or another proposition β₂ ∈ neg_body(R) such that β₂ $\notin$ IM and β₂ ∈ M that could be found in a body of a rule R that implies α.

If α $\notin$ IM and α ∈ M, there is a rule R supporting α w.r.t. M.

• Hence, pos_body(R) ⊆ M and neg_body(R) $\cap$ M = ∅.

• And if α is not a culprit, R is not a supporting rule of α w.r.t. IM.

• Thus, pos_body(R) ⊄ IM or neg_body(R) $\cap$ IM ≠ ∅.

• Because Π is non-recursive, α $\notin$ body(R)

• Hence, there is another proposition β₁ ∈ pos_body(R) such that β₁ $\notin$ IM and β₁ ∈ M or another proposition β₂ ∈ neg_body(R) such that β₂ ∈ IM and β₂ $\notin$ M that could be found in a body of a rule R that implies α.

From Example 1, the stable model is {p, r, f}. Let the intended interpretation IM be {q, f}, p, q, and r will become unexpected, and r is a culprit according to Theorem 2 (Table 1).

Table 1. An illustrated example of Theorem 2

From Theorem 2, if we query from any unexpected proposition and find another unexpected proposition recursively, as long as the query sequence is finite and does not loop (e.g. a finite non-recursive logic program), the query finally succeeds by finding a culprit. Therefore, we could design the finding culprit algorithm as in Table 2.

Table 2. Finding culprit algorithm (a - They follow directly by the definition of a culprit, Definition 10. b - These conditions are actually determined when finding a supporting rule. They are mentioned to emphasize that they are unexpected.)

The algorithm is only for finding one culprit. In case there are two culprits or more, the user has to repeat the same procedure again. Actually, it is safe to check that the stable model from the revised program is equal to the intended interpretation. For example, from a program {p ← q, not r. q ← f₁. r ← f₂} with an empty set as the stable model, if an intended interpretation was {q}, we can see that only q would be unexpected hence it would be a culprit. If we resolved by just adding q as a fact, {p, q} would become a stable model, which is not same as what we intended. In another round, p would become unexpected w.r.t. {q} and hence p would be a culprit. If we resolved by removing the rule p ← q, not r from the program, {q} would finally become the stable model as we expected.

3 Legal Debugging Under PROLEG

PROLEG (PROlog based LEGal reasoning support system) [4] is a logic programming adapted from Prolog. It reflects the legal reasoning procedures called The Japanese Presupposed Ultimate Fact Theory practiced in Japanese law schools. PROLEG is different from Prolog in manipulation of negative conditions but the representation power of PROLEG is the same as Prolog [9]. In this section, we provide definitions for PROLEG and extend the legal debugging under PROLEG. First, these are basic definitions of PROLEG.

Definition 11.

[PROLEG] A PROLEG program P is a pair $\left\langle {H,E} \right\rangle$ where

• H is a set of rules R of the from h ← b₁,…,b_n. where h and b_i (1 ≤ i ≤ n) are propositions (note that there are no negations in the rule). We denote h as head(R) and {b₁,…,b_n} as body(R).

• E is a set of exceptions of the form exception(h, e) where h and e be propositions (note that e is a proposition, not a set of propositions).

Definition 12.

[Applicable rule] Let M be a set of propositions and $\left\langle {H,E} \right\rangle$ be a PROLEG program. We denote a set of applicable rules w.r.t. M by H^M = {R ∈ H | ¬∃exception(head(R), e) ∈ E such that e ∈ M}.

So if an exception of rule exists in M (e ∈ M) then the rule is inapplicable.

Definition 13.

[Extension] A set of propositions M is an extension of a PROLEG program $\left\langle {H,E} \right\rangle$ if M is the minimum model of H^M (M = min(H^M)).

Example 2.

P′ is a PROLEG program.

• $$ \begin{array}{*{20}l} {p \leftarrow q.} \hfill \\ {q \leftarrow f_{1} .} \hfill \\ {r \leftarrow f_{2} .} \hfill \\ {exception\left( {p,r} \right).} \hfill \\ \end{array} $$

Let M = {r}, H^M = {q ← f₁, r ← f₂ } (p ← q is inapplicable here because there is an exception (p, r) and r ∈ M). Since min(H^M) = ∅. M is not an extension of P′.

Let M = ∅, H^M = {p ← q, q ← f₁, r ← f₂ }. Since min(H^M) = ∅. M is an extension of P′.

PROLEG representation is actually aligned with the logic program with negation as failure but using exception instead of negation. However, one particular different point is that if we add an exception to a condition, it applies to all rules on that condition unlike a logic program with negation as failure whose negations must be added to the rule one by one as illustrated in Table 3.

Table 3. An equivalent representation between PROLEG (left) and Prolog (right)

Because the representation power of PROLEG is same as the logic program with negation as failure, we can extend the same idea of supports, culprits, and finding culprit theorem by using an extension of P instead of the stable model. For example, these are definition of support (Definition 7), definition of intended interpretation (Definition 8), and definition of unexpected proposition (Definition 9) in PROLEG.

Definition 14.

[Support in PROLEG] A set of proposition S supports a proposition p w.r.t. a PROLEG program P if there is a rule R such that p = head(R), body(R) ⊆ S, and there is no exception(p, e) ∈ E such that e ∈ S We call that R is a supporting rule of p w.r.t. S and P.

Definition 15.

[Intended interpretation in PROLEG] A set of propositions IM can be an intended interpretation of a PROLEG program P if and only if a set of factual propositions in an extension of P and a set of factual propositions in IM are equal.

Definition 16.

[Unexpected in PROLEG] A proposition p is unexpected w.r.t. an intended interpretation IM and a PROLEG program P if p is not in an extension of P but in IM or if p is in an extension of P but not in IM.

We design a finding culprit algorithm in PROLEG as shown in Table 4. It is still based on recursion from an unexpected proposition according to Theorem 2. Because the input PROLEG program P is not recursive, it can be deduced that there is only one extension of P.

Table 4. Finding culprit algorithm in PROLEG

4 Legal Debugging Example

In this section, we use an example of unexpected consequences adapted from this following case [10]:

• 1. A plaintiff made a lease contract for his house between him and the defendant.

• 2. When the defendant returned home for a while, he let his son use the room.

• 3. Then, the plaintiff claimed that the contract was ended by his cancellation for the reason that the defendant subleases without permission by literal interpretation of Japanese Civil Code Article 612 as follows.

  • Phrase 1: A lessee may not assign the lessee’s rights or sublease a leased thing without obtaining the approval of the lessor.

  • Phrase 2: If the lessee allows any third party to make use of or take profits from a leased thing in violation of the provisions of the preceding paragraph, the lessor may cancel the contract.

When the case was taken to the court, the court decided that the literal interpretation produces an unexpected consequence. Although the cancellation is valid if we interpret the related piece of law literally, the court decided that the literal interpretation is too strict because “the third party” who makes use of the room temporally was the defendant’s son and he did not harm the confidence between a lessee and a lessor, as the court mentioned the following:

• Phrase 2 is not applicable in exceptional situations where the sublease does not harm the confidence between a lessee and a lessor, and therefore the lessor cannot cancel the contract unless they prove the lessee’s destructing of confidence.

The Japanese Civil Code Article 612 and the facts from the case can be represented in propositional PROLEG as in Table 5.

Table 5. Propositional PROLEG representation of Japanese Civil Code Article 612

From this representation, cancellation_due_to_sublease , effective_lease _contract , and effective_sublease_contract are non-factual predicates in the extension of the program due to the given facts entailing these proposition and no exception is executed. This reflects when we interpret the law literally. However, since the court decided that the validity of cancellation_due_to_sublease is too harsh. It becomes an unexpected proposition. The legal debugger would help clarifying which legal conditions cause the unexpected consequence as well as finding the intended interpretation that supports the court reasoning. We could initiate debugging by using cancellation_due_to_sublease as an unexpected proposition as shown in Fig. 1.

Fig. 1.

Legal debugging steps from the rule base

The debugger firstly traced into the supporting rule of cancellation_due_to_sublease (the first rule) to determine two conditions in the body effective_lease_contract and effective_sublease_contract . The debugger asked user whether both conditions were intended to be fulfilled or not. If one of them was intended to be not fulfilled, it became a culprit because the intended interpretation would support it (situation 1 and 2). If both of them were intended to be fulfilled, the debugger retraced on approval_of_sublease which is an exception of cancellation_due_to_sublease . Then, the debugger asked user that approval_of_sublease was intended to be fulfilled or not. If it was intended to be fulfilled, it became a culprit because the intended interpretation would not support it (situation 3). If approval_of_sublease was intended to be not fulfilled, then there was no unexpected condition for cancellation_due_to_sublease , hence cancellation_due_to_sublease became a culprit itself (situation 4). The intended interpretations of each situation are illustrated in Table 6.

Table 6. Culprit and Intended Interpretation for Each Situation

A culprit is considered in top-down left-to-right manner. Although the user does not consider all non-factual propositions, the debugger would return a first encountered culprit as soon as the debugger could not find any unexpected propositions. A culprit would be useful for considered rather in its resolution. Generally, the court would give an exception from extra facts of the case, such as in this case exception (cancellation_due_to_sublease, nonabuse_of_confidence) may be introduced to correspond to the Supreme Court decision. However, there are other possibilities to resolve one culprit so the resolution of culprits should be investigated further.

5 Discussion and Related Works

5.1 Legal Debugging in Statute Legal Practice

Statute rules are usually constructed in a top-down approach, from abstract to concrete concept. Each condition must be proved and presented to the court in the order of the list written in the procedure. For example, the case in Sect. 4 of this paper involves an issue of cancellation of a lease contract due to sublease. To claim the issue, four conditions (effective lease contract, effective sublease contract must be effective, using the less thing, and manifesting cancellation) must be proved and presented to the court in order. However, when the court decided that the case produces an unexpected consequence. The court usually identifies the top concept to be unexpected. Therefore, the legal debugging helps the court to trace in a top-down manner from the abstract concept identified by the court to the culprit that causes unexpected consequences, as well as to trace in a left-to-right manner in order of the list written in the procedure.

5.2 Application of Debugging Besides Software

“Legal debugging” is proposed for tacit expectations unlike inconsistencies [11,12,13,14] that deals with conflicts between explicit written rules. Several paradigms have been proposed to find bugs such as online-offline justifications [15] and meta-programming [16] but most debugging technique are based on algorithmic debugging [17]. Besides software, algorithmic debugging has been proposed for navigating users in a few applications [18]. Zinn [19] has applied algorithmic debugging in tutoring systems. The papers view a program as a knowledge corpus and an intended interpretation as a student expectation. A student misconception can be viewed as a bug and a wrong answer can be viewed as an unexpected answer. Algorithmic debugging has also been applied in hardware design and verification. Kuchcinski et al. [20] has worked on using algorithmic debugging in hardware design by viewing circuits as auxiliary functions and logic programs respectively to detect faulty components.

Our paper is the first work proposing legal debugging. Legal debugging has to deal with tacit expectations from legal experts and different structures of representation, such as non-stratified structure and exception separation in PROLEG, and different resolution for preventing unexpected consequences, such as using exceptions instead of adding conditions. This paper views a representation of literal interpretation as a program and a culprit, a rule condition which causes unexpected consequences, as a bug.

5.3 Semantics of Legal Representation on Debugging

Program semantics may affect debugging schemes [18]. For example, in answer set programming, a debugger has to treat multiple situations due to the allowance of multiple answers [21,22,23,24]. In Datalog, a debugger has to deal with non-stratified programs differently because the semantics sometimes gives an empty set instead of non-termination for some types of non-stratified programs [25].

Since this paper is the first step on legal debugging, we have focused only a stratified and non-recursive representation. This representation often reflects the structure of statutory law that expects only one interpretation. Since a stratified and non-recursive program exists only one interpretation, we can eliminate the problems mentioned above. However, it is important to consider semantics used in legal representation because they still have some effects on legal debugging. For example, separation of conditions and exceptions in PROLEG affects resolution of legal culprits due to the border scope of exceptions.

6 Conclusion and Future Works

In this paper, we have proposed the idea of legal debugging in legal knowledge represented by logic programming. The idea has been presented in non-recursive program which we assume that some propositions’ truth values shall not be changed (called factual proposition). Then, we have proposed the idea of culprit, a rule condition that causes unexpected consequences. We begin the debugging process from an initial unexpected proposition. The debugger follows a sequence of unexpected propositions until it meets a culprit otherwise the initial unexpected proposition is a culprit itself. We prove the correctness of algorithm under non-recursive logic programing with negation as failure, and then we extend the algorithm to PROLEG system. In future, we will extend the algorithm for first-order logic programs with arguments and develop an interactive debugger in PROLEG system which asks user intention and steps into rule base to find culprits similarly to computer program debugging.