On the Legal Debugging in PROLEG program
Wachara Fungwacharakorn1 and Ken Satoh2
1

National Institute of Informatics, Sokendai University, Tokyo, Japanwacharaf@nii.ac.jp
2
National Institute of Informatics, Sokendai University, Tokyo, Japanksatoh@nii.ac.jp

Abstract. PROLEG is a legal reasoning system adapted from Prolog. It gives
legal reasoning based on rule base extracted from legislation. However,legislation itself contains unexpected exceptions which can be detected only
when an exceptional situation happens. In this paper, we proposed a techniquecalled “legal debugging” to find out which rule conditions should be revised insuch exceptional cases. We firstly present the legal debugging in the context of
non-recursive logic program. Then, we extend into the context of PROLEG
program and illustrate legal debugging in PROLEG with a Supreme Court case.
Keywords: Legal Reasoning, Legal Representation, Algorithmic Debugging.

1

Introduction

PROLEG (PROlog based LEGal reasoning support system) [1] is a logic
programming adapted from Prolog. It reflects the legal reasoning procedures called
ultimate fact theory practiced in Japanese law schools. In brief, PROLEG is similar to
Prolog but using exception instead of negation. To simulate legal reasoning, PROLEG
retrieves facts from the case and gives reasoning based on legal rules.
However, legal rules itself have unexpected exceptions. They are hard to be
detected unless such particular exceptional case happens. For example, let’s considera case that a plaintiff made a lease contract for his house between him and the defendant. The defendant let his son use a room when he comes back home for a while. Thenthe plaintiff claimed that the contract was ended by his cancellation of the contract for
the reason that the defendant subleases without permission.
According to the related piece of legislation, Japanese Civil Code Article 612, theleaser may cancel the contract if the lessee lets any third party use the property
without lessor’s permission.
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 aleased thing in violation of the provisions of the preceding paragraph, the lessor
may cancel the contract.

If we interpret the legislation literally, the cancellation is valid. However, when we
take into account that the person who temporally uses the room was the defendant’s
son and he did not harm the confidence between a lessee and a lessor, the regulation
might look too strict. The Supreme Court agreed to this and decided following [2]:Phrase 2 is not applicable in exceptional situations where the sublease does notharm 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.
Hence, when giving a legal reasoning in this case, some rule conditions would be
affected. Finding those rule conditions can be regarded as legal debugging.
A debugger identifies a culprit, a condition that causes unexpected consequences, andallows the users to resolve it.
Therefore, in this paper, we try to formalize the process of legal debugging in
PROLEG program. This paper is structured as follows. Section 2 describes
legal reasoning characteristics in the context of logic program with negation as failureand defines a legal debugging process in that context. Section 3 extends the legal
debugging process into the context of PROLEG. Section 4 demonstrates a legal
debugging process in PROLEG using the above Supreme Court case. Section 5compares legal debugging and other related works on debugging process. The final
section summarizes the idea of legal debugging and its application as the future work.

2

Legal Reasoning and Debugging in Logic Program Context

2.1

Legal Reasoning in Logic Program Context

Before defining the legal debugging process, this section introduces basic
assumptions of legal reasoning in the context of logic program with negation as
failure because it is familiar to many logic programmers. Generally, the logic programwith negation as failure is defined by following definitions.
Definition 1. [Rules] Let h, bi (1 i  n), and cj (1 j  m) be propositions and R be arule of the form h b1,…,bn, not c1,…, not cm.
We denote h as head(R), {b1,…,bn} as pos_body(R), {c1,…,cm} as neg_body(R),and body(R) as pos_body(R)  neg_body(R). We allow a rule without a body denoted
as fact.
Definition 2. [Satisfaction] Let I be a set of propositions and R be a rule. I satisfies R
if the following condition is satisfied:
if pos_body(R)  I and neg_body(R)  I =  then h  I.

Definition 3. [Model] Let P be a finite set of rules and I be a set of propositions. If I
satisfies every rule in P, we call that I is a model of P. The minimum model of P
(denoted as min(P)) is a model of P which is the minimum in the sense of set inclusion.
Example 1. An example of a logic program Pp q, not r.
q f1.
r f2.
From Example 1, {q} does not satisfy the rule R: p  q, not r because
pos_body(R)  {q} and neg_body(R)  {q} =  but p  {q}. The example sets ofpropositions that satisfy every rule in P are , {r}, {q, r}, {p, q} hence they aremodels of P and the minimum model of P is  (min(P) = ). Sometimes theminimum model is referred as an answer set.
Note that propositions in this paper do not contain arguments (Zeroth-order logic).
Propositions that contain arguments are such as p(a), or p(a,b) which can be seen inlegal representation such as contract(plaintiff, defendant) but we omit them in thispaper to simplify the idea. We will continue to work on them in the future works.
There are also two assumptions from legal reasoning that we use for simplifying
and distinguishing the logic program that represents legal knowledge from generallogic programs. First assumption from legal reasoning is that, generally, the rules
from legislation are not recursive. Recursive rules are those rules whose dependency
graph contains a loop (see details in [3]). For example {p  p.},{p  not p.},{p  q. q  p.} are recursive, but the program in Example 1 is not recursive .
Second assumption is that, some propositions in legislation are contingent. Their
truth values shall not be determined analytically but by directly derive from theevidences e.g. the signature is valid or not. Hence, such propositions never appear as ahead of a rule with a body so their truth values could be changed when modifying
other propositions so we could define contingent as follows.
Definition 4. [Contingency] A proposition is contingent if it does not appear as a headof a rule with a body.
From Example 1, f1 and f2 are contingent. Their truth value could not be changed
by modifying other propositions but only by adding them as facts (a rule without abody). In contrast, p, q, or r could be changed their truth value by modifying otherpropositions, for example, p could become true if we made q true (such as just adding
q as a fact) and kept r false.
However, some propositions could not be true concurrently. From Example 1, if r
was true, p could not be true. We could say that {r} (or any sets that contain r) does
not support p. To determine this relation between rules and a set of propositions, theidea of support is defined as follows.

Definition 5. [Support] A set of propositions S supports a non-contingent proposition
p w.r.t. a logic program P if there is a rule R  P such that p is the head of the rule(p=head(R)), pos_body(R)  S, and neg_body(R)  S = . R is called a supporting
rule of p w.r.t. S.
Theorem 1. [Relation between model and support] Given P as a non-recursive logic
program and p is non-contingent and, p  min(P) if and only if min(P) supports p.
Proof.
Suppose min(P) supports p but p  min(P), then there is a rule R  P supporting of p.
Hence p=head(R), pos_body(R)  min(P) and neg_body(R)  min(P) = .
But since p  min(P), min(P) does not satisfy R.
It leads to contradiction with the definition of model.
Suppose min(P) does not support p but p  min(P), then no rules are supporting p.
Thus, min(P) - {p} must be a model because it satisfies every rule in P.
It leads to contradiction with the definition of the minimum model.
2.2

Legal Debugging in Logic Program Context

When the direct interpret of legislation gives unexpected results, it means that we
intend a different minimum model from the existed minimum model. However,
because truth values of contingent propositions are already finalized, one that iscontingently true would not be possible to be excluded from a minimum model andthat is contingently false would not be possible to be included in a minimum model.
From Example 1, we could not intend {f1} to be a minimum model because f1 iscontingently false and we could not change its truth value. In contrast, we could intend {q} to be a minimum model because q is not contingent so we allow changing
the truth value of q (such as just adding q as a fact). Therefore, we define an intended
model denoted as IM with following definitions.
Definition 6. [Intended model constraint] A set of propositions IM can be an intended
model of a logic program P if and only if a set of contingent facts in min(P) and a setof contingent facts in IM are equal.
Consequently, if IM is different from min(P), there must be a non-contingent p thatis not currently derived but intended to be derived (p  min(P) but p  IM) or
currently derived but intended not to be derived (p  min(P) but p  IM). Such proposition is called unexpected which is defined as follows.
Definition 7. [Unexpectation] A proposition p is unexpected w.r.t. an intended model
IM and a logic program P if p  min(P) but p  IM or if p  min(P) but p  IM .
Contingent propositions could not be unexpected due to constraints in Definition 6.

To modify the program so its minimum model was changed to what we intended,
we must work on some non-contingent propositions called culprit defined as follows.
Definition 8. [Culprit] a non-contingent proposition p will be a culprit of a logic program P w.r.t. an intended model IM if p  IM but IM does not support p or
 p  IM but IM supports p
From Example 1, if IM = {q}.
 p  IM but IM supports p by p  q, not r, hence p is a culprit of P
 q  IM but IM does not support q, hence q is a culprit of P
 r  IM and IM does not support r, hence r is not a culprit of P
Then, we get the following property.
Theorem 2. [Unexpectation Propagation] Given P as a non-recursive logic programand IM as an intended model that not equal to min(P). If p is unexpected w.r.t. IM andP, then there is existed another proposition q in a body of a rule whose head is p such thatq is unexpected w.r.t. IM and P otherwise
 p is a culprit w.r.t. IM and P itself
Proof.
If p  IM and p is also not a culprit
Then there is a rule R supporting of p w.r.t. IM.
Hence, pos_body(R)  IM and neg_body(R)  IM = .
But p  min(P), R is not a supporting rule of p w.r.t. min(P).
Thus, pos_body(R)  min(P) or neg_body(R)  min(P)  .
Because P is non-recursive, p body(R)Hence, there is another proposition q  pos_body(R) such that q  IM andq  min(P) or another proposition r  neg_body(R) such that r  IM andr  min(P) that could be found in a body of a rule R whose head is p .
If p  IM and p  min(P), there is a rule R supporting of p w.r.t. min(P).
Hence, pos_body(R)  min(P) and neg_body(R)  min(P) = .
And if p is not a culprit, R is not a supporting rule of p w.r.t. IM.
Thus, pos_body(R)  IM or neg_body(R)  IM  .
Because P is non-recursive, p body(R)Hence, there is another proposition q  pos_body(R) such that q  IM andq  min(P) or another proposition r  neg_body(R) such that r  IM andr  min(P) that could be found in a body of a rule R whose head is p.

Example 2. Given P a logic program as in Table 1, then f is contingent andmin(P) = {p, r, f}. Let the intended model IM be {q, f}, p, q, and r are unexpected,
and r is a culprit according to Theorem 2.
Table 1. An illustrated example of Theorem 2
Rulesp not q.
p not f.
q not r.
r f.
f.

Unexpectedfound in a head
p
p
q
r
-

Supporting Rulew.r.t. min(P)Supporting
Supporting-

Supporting Rulew.r.t. IM
Supporting
Supporting-

Unexpected found in a bodyqr
- (thus r is a culprit w.r.t. IM)-

From Theorem 2, if we query from any unexpected proposition and find anotherunexpected proposition recursively, as long as the query sequence is finite and does
not loop (e.g. P is a finite non-recursive logic program), the query finally succeeds byfinding a culprit. Therefore, we could design the finding culprit algorithm as Table 2.
Table 2. Finding culprit algorithm
Input: a finite non-recursive logic program P,
an intended model IM, an unexpected proposition p
Find_culprit(p)begin
Find R as a supporting rule of p w.r.t. IM
if1 p ∈ IM and there is no such R return p;else if p ∈ IM
Find q  pos_body(R) s.t. q  IM 2 and q  min(P)if there is such q return Find_culprit(q)Find r  neg_body(R) s.t. r  IM 2 and r  min(P)if there is such r return Find_culprit(r)return3 p
if1 p ∉ IM and there is such R return p;else if p ∉ IM
Find R’ as a supporting rule of p w.r.t. min(P)Find q  pos_body(R’) s.t. q  IM and q  min(P)2
if there is such q return Find_culprit(q)Find r  neg_body(R’) s.t. r  IM and r  min(P)2
if there is such r return Find_culprit(r)return3 p
end

1
2

3

They follow directly by the definition of a culprit, Definition 8.
These conditions are actually determined when finding a supporting rule. They are
mentioned to emphasize that they are unexpected.
If we could not find another unexpected proposition, then p itself is a culprit according to
Theorem 2.

The algorithm is only used for finding one culprit. However, there are cases that alogic program has two culprits or more, or the resolution of a culprit will create
another culprit. In such cases, a user has to repeat the same procedure for the revised
rules. Actually, it is safe to check that the result minimum model from the revised
program is equal to the intended model because it is possible to have the chain reflect
from the resolution.
For example, from example 1, if an intended model was {q}, we can see that only
q would be unexpected hence it would be a culprit. If we resolved by just adding q asa fact, {p, q} would become a minimum model instead of {q} that we expected. In
another round, p would become unexpected w.r.t. {q} and hence p would be a
culprit. If we resolved by removing a rule p  q, not r from the program, {q} would
finally become the minimum model as we expected.

3Legal Debugging in PROLEG

PROLEG is different from Prolog in manipulation of negative conditions but the
representation power of PROLEG is same as Prolog [4]. In this section, we provide
definitions for PROLEG and extend the legal debugging process into the context of
PROLEG program. First, these are basic definitions of PROLEG program.
Definition 9. [PROLEG] A PROLEG program P is a pair ⟨H, E⟩ where H is a set of rules R of the from h b1,…,bn. where h and bi (1 i  n) arepropositions (note that there are no negations in the rule). We denote h as head(R)and {b1,…,bn} 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 10. [Applicable rule] Let M be a set of propositions. We denote a set of
applicable rules w.r.t. M, HM = {R  H | ¬∃exception(head(R), e)  E s.t. e  M}
So if an exception of rule exists (e  M) then the rule is inapplicable.
Definition 11. [Extension] A set of propositions M is an extension of P if M is theminimum model of HM (M = min(HM)).
Example 3. P’ is a PROLEG program.
p q.
q f1.
r f2.
exception(p,r).

Let M = {r}, HM = { q f1, r f2 } (p q is inapplicable here because there is an
exception(p,r) and r  M). Since min(HM) = . M is not an extension of P’.
Let M = , HM = { p q, q f1, r f2 }. Since min(HM) = . M is an extensionof P’.
Actually, Example 3 is the PROLEG representation of the Example 1. We can seethat 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 thatcondition 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)

p q.
p r.
exception(p, e).

p q, not e.
p r, not e.

Because the representation power of PROLEG is same as the logic program withnegation as failure, we can use the same idea of supports, culprits, and finding culprit
theorem by using an extension of P instead of min(P). For example, these aredefinition of support (Definition 5), definition of intended model (Definition 6), anddefinition of unexpectation (Definition 7) in PROLEG.
Definition 12. [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 ruleof p w.r.t. S.
Definition 13. [Intended Model in PROLEG] A set of propositions IM can be an
intended model of a PROLEG program P if and only if a set of contingent facts in an
extension of P and a set of contingent facts in IM are equal.
Definition 14. [Unexpected in PROLEG] p is unexpected w.r.t. an intended model 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 stillbased 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
Input: a finite non-recursive PROLEG logic program P = ⟨H,E⟩,
an intended model IM, an unexpected proposition p
Find_culprit(p)begin
Find R as a supporting rule of p w.r.t. IM
if p ∈ IM and there is no such R return p;else if p ∈ IM
Find q  body(R) s.t. q is not in an extension of P
if there is such q return Find_culprit(q)Find e s.t. exception(p,e)  E and e is in an extension of P
if there is such e return Find_culprit(e)return p
if p ∉ IM and there is such R
return p;else if p ∉ IM
Find R’ as a supporting rule of p w.r.t. an extension of P
Find q  body(R’) s.t. q  IM
if there is such q return Find_culprit(q)Find e s.t. exception(p,e)  E and e  IM
if there is such e return Find_culprit(e)return p
end

4

Example of Legal Debugging in PROLEG

This section illustrates how to make legal reasoning and legal debugging in PROLEG
program from the case of Japanese Civil Code Article 612 as mentioned in the
introduction section. First, let us introduce the PROLEG representation of Japanese
Civil Code Article 612 in Table 5.
Table 5. PROLEG representation of Japanese Civil Code Article 612
cancellation_due_to_sublease <=effective_lease_contract,effective_sublease_contract,using_leased_thing,
manifestation_cancellation.
effective_lease_contract <=agreement_of_lease_contract,
handover_based_on_the_lease_contract.
effective_sublease_contract <=agreement_of_sublease_contract,
handover_based_on_the_sublease_contract.
exception(cancellation_due_to_sublease,approval_of_sublease).

approval_of_sublease <=approval_of_sublease_before_the_day.
// Facts that are contingently true
agreement_of_lease_contract.
handover_based_on_the_lease_contract.
agreement_of_sublease_contract.
handover_based_on_the_sublease_contract.
using_leased_thing.
manifestation_cancellation.
nonabuse_of_confidence.

Fig. 1. Legal debugging steps from the rule base

From the rule base, cancellation_due_to_sublease is fulfilled because all
positive conditions are met and no exception is executed. However, since we concernthat the result is too strict, we could initiate debugging by using cancellation_due_
to_sublease as an unexpected proposition as shown in Fig. 1.
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 model would support it. If bothof 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 theintended model would not support it. 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.
After a culprit was determined, the resolution of culprit could be introduced. For
example, to determine this case according to the Supreme Court decision, it is still
intended that effective_lease_contract and effective_sublease_contract to be
fulfilled and approval_of_sublease to be not fulfilled. Hence the cancellation_

due_to_sublease becomes aculprit. Then, the debugger could ask the user toresolve the culprit. Generally, it could be resolved by introducing some unconcernedfacts as an exception of the culprit. In this case, exception (cancellation_due_to_sublease, nonabuse_of_confidence) shall be introduced to solve the unexpected
result. This resolution also corresponds to the Supreme Court decision.

5

Discussion and Related works

The idea of legal debugging is closely related to the idea of debugging logic program
which has been widely concerned since the logic program was established [5] such as
the notable work of Ehud Shapiro’s algorithmic program debugging in 1982 [6]. The
idea has been developed in many logic programming perspectives, especially for
those in answer set programming. Perhaps the idea of debugging answer set
programming was introduced in [7] before many types of unexpected results has been
concerned such as inconsistency [8, 9] and absence of the answer sets [10, 11]. Manydifferent techniques have also been proposed to solve different applications such as
stepping framework [12] and meta-programming [13].
In this paper, the legal representation is aligned with answer set program withnegation as failure but different in some perspectives. First, the program is assumed to
be not recursive so we can eliminate the problem from loops such in [8–11]. Second,some propositions are contingent of evidences. Therefore, even the concept of support
is aligned with [7] but the logic program was restricted to not be able to touch truth
value of contingent facts. Finally, the user does not recognize all intended
propositions at the first time but rather recognize them when responding the debugger
steps by steps. Hence the algorithm was designed to be in steps with those three
specific assumptions.

6

Conclusion and Future Works

In this paper, we have proposed the idea of legal debugging especially in PROLEG
program. The idea has been presented in non-recursive program which we assume
that some propositions’ truth values shall not be changed (called contingent facts).
Then, we have proposed the idea of culprit, a rule condition that needs to be revisedwhen direct legal reasoning from legislation gives unexpected result. We begin the
debugging process from the unexpected result as 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 thecorrectness of algorithm under non-recursive logic programing with negation as
failure, and then we extend the algorithm to PROLEG program. In future, we will
extend the algorithm for first-order logic programs with arguments and develop aninteractive debugger in PROLEG program which asks user intention and steps intorule base to find culprits similarly to the debugging process in programming.

References
1. Satoh, K., Asai, K., Kogawa, T., Kubota, M., Nakamura, M., Nishigai, Y.,
Shirakawa, K., Takano, C.: PROLEG: An Implementation of the Presupposed
Ultimate Fact Theory of Japanese Civil Code by PROLOG Technology. In: New
Frontiers in Artificial Intelligence. pp. 153–164. Springer, Berlin, Heidelberg(2010).
2. Minshu Vol. 50, No. 9 at 2431: 1994 (O) 693. (1996).
3. Ullman, J.: Principles of database and knowledge-base systems. Computer Science
Press (1988).
4. Satoh, K., Kogawa, T., Okada, N., Omori, K., Omura, S., Tsuchiya, K.: On
Generality of PROLEG Knowledge Representation. In: Proceedings of the 6thInternational Workshop on Juris-informatics (JURISIN 2012), Miyazaki, Japan.
pp. 115–128 (2012).
5. Caballero, R., Riesco, A., Silva, J.: A Survey of Algorithmic Debugging. ACM
Comput. Surv. 50, 60:1–60:35 (2017).
6. Shapiro, E.Y.: Algorithmic Program Debugging. MIT Press, Cambridge, MA,
USA (1983).
7. Brain, M., De Vos, M.: Debugging Logic Programs under the Answer Set
Semantics. In: Answer Set Programming (2005).
8. Syrjänen, T.: Debugging inconsistent answer set programs. In: Proc. NMR. pp.
77–83 (2006).
9. Schulz, C., Satoh, K., Toni, F.: Characterising and Explaining Inconsistency in
Logic Programs. In: Calimeri, F., Ianni, G., and Truszczynski, M. (eds.) Logic
Programming and Nonmonotonic Reasoning. pp. 467–479. Springer International
Publishing (2015).
10. Caminada, M., Sakama, C.: On the existence of answer sets in normal extended
logic programs. ECAI 2006 Proc. 141, 743–744 (2006).
11. Oetsch, J., Pührer, J., Tompits, H.: Catching the ouroboros: On debugging
non-ground answer-set programs. Theory Pract. Log. Program. 10, 513–529(2010).
12. Oetsch, J., Pührer, J., Tompits, H.: Stepping through an answer-set program. In:
International Conference on Logic Programming and Nonmonotonic Reasoning.
pp. 134–147. Springer (2011).
13. Gebser, M., Pührer, J., Schaub, T., Tompits, H.: A meta-programming techniquefor debugging answer-set programs. In: AAAI. pp. 448–453 (2008).