Classical Description Logic has been widely used as a basis for ontology creation and reasoning in many knowledge specific domains. These specific domains naturally include Legal AI. As in any other domain, consistency is an important issue for legal ontologies. However, due to its inherently normative feature, coherence (consistency) in legal ontologies is more subtle than in most other domains. Negation and subsumption play a central role in ontology coherence. An adequate intuitionistic semantics for negation in a legal domain comes to the fore when we take legally valid individual statements as the inhabitants of our legal ontology. This allows us to elegantly deal with particular situations of legal coherence, such as conflict of laws, as those solved by Private International Law analysis. This paper: (1) Briefly presents our version of Intuitionistic Description Logic, called IALC for Intuitionistic ALC (ALC being the canonical classical description logic system)(2) Discuss the jurisprudence foundation of our system, and (3) Shows how we can perform a coherence analysis of “Conflict of Laws in Space” by means of IALC. This paper reports work-in-progress on using this alternative definition of logical negation for building and testing legal ontologies and reasoning in AI.
Classical Description Logic has been widely used as a basis for ontology creation and reasoning in many knowledge specific domains. These specific domains naturally include Legal AI. As in any other domain, consistency is an important issue for legal ontologies. However, due to its inherently normative feature, coherence (consistency) in legal ontologies is more subtle than in most other domains. Negation and subsumption play a central role in ontology coherence. An adequate intuitionistic semantics for negation in a legal domain comes to the fore when we take legally valid individual statements as the inhabitants of our legal ontology. This allows us to elegantly deal with particular situations of legal coherence, such as conflict of laws, as those solved by Private International Law analysis. This paper: (1) Briefly presents our version of Intuitionistic Description Logic, called IALC for Intuitionistic ALC (ALC being the canonical classical description logic system)(2) Discuss the jurisprudence foundation of our system, and (3) Shows how we can perform a coherence analysis of “Conflict of Laws in Space” by means of IALC. This paper reports work-in-progress on using this alternative definition of logical negation for building and testing legal ontologies and reasoning in AI.
One of the main problems from jurisprudence (legal theory) is to make
precise the use of the term “law”. In fact, the problem of individuation, namely,
what counts as the unit of law, seems to be one of the fundamental open
question in jurisprudence.Any approach to law classification requires firstly
answering the question “What is to count as one complete law?”
One is to take the all (existing) legally valid statements as a whole. This
totality is called “the law”. This approach is predominant in legal philosophy
and jurisprudence debiting his significance to the Legal Positivism tradition
initiated by Hans Kelsen (for a contemporary reference see
The other approach to law definition is to take into account all legally
valid statements as being individual laws. This view, in essence, is harder
to be shared with jurisprudence principles, since they firstly are concerned
to justify law. This latter approach seems to be more suitable to Legal AI.
It is also considered by Legal theoreticians, at least partially, whenever they
start considering ontological commitments, such as, taking some legal
relations as primitive ones
From the semantic point of view, iALC seems to be well suited to model the Legal theoretic approach pursued by KE as cited above. Let us consider an iALC model having as individuals each of the valid and possible legal statements. The relation is the natural hierarchy existing between these individual legal statements, as well from any precedence relation related to them. For example, sometimes conflicts between legal statements are solved by inspecting the age of the laws (how old is the date of its first edition in the legal system), the wideness enforcement scope of each law, and etc. Any of these considered relations are order reactions. For example, “Theodor is vicariously liable by John” is legally dominated (precedes) by “John is a worker of Theodor”, or “John and Theodor have an ’ employment contract’. Any legal statement involving the civil liability of someone must precedes any legal statement asserting that he/she is of legal age. If C is a concept symbol in a description logic language, its semantics is the subset of legal statements representing a kind of legal situation.
The main role of the Intuitionism in our setting is the meaning it provides to the negation of concepts, as well as to subsumption.
Let us analyze briefly the case of negation of concepts regarding the classical ALC logic and a more traditional approach, based on classic ALC, to the ontological formalization of ”the law” that includes the development of one or more domain ontologies to be used in validating the legal statements.
Consider a person, P eter, that is under the legal age in his living country. Let us consider, as it is usual, that people under the legal age are not able to sign contracts. Consider a part of an (hypothetical) ontology of Private Ownership Law with concepts RentingContract, for the set of valid renting contracts, ∃hasT enant.RentingContract, for the set of legal tenants, and, ∃hasLandlord.RentingContract for the set of legal landlords. Of course, our P eter is not in ∃hasT enant.RentingContract nor in ∃hasLandlord.RentingContract either. Thus, in classical ALC, P eter is in the complement of each respective concept, namely ¬∃hasLandlord.RentingContract and ∃hasLandlord.RentingContract. In other words, “ P eter has no contract signed” has to be taken as a legal statement in our ontology. But, P eter is under legal age, and hence, there must be no legal statement about him as an individual agent.
As seen in the previous paragraph, Classical negation forces the negation of a proposition to be part of a concept, but in the context of “the law” the negation of a valid law does not have to be valid either. Besides the ontological complexity of dealing with legal statements together with non-legal ones by defining concepts that are outside jurisprudence, Classical negation can lead to unnecessary incoherent situations in a legal ontology. The following paragraph illustrates this.
Suppose that P eter, from the above discussion, is under legal age in the place he lives, but he is citizen from another country where he is of legal age. If the country he lives has Private International Law then he has to be considered of legal age in the country he lives. Classical negation cannot be applied to this situation without leading to an incoherence: “Peter is and not is of legal age”. The usual way to circumvent this kind of situation is to consider an auxiliary ontology on objects and agents outside “the law” but related to it, and, by means of these auxiliary terminological entities overcome the incoherency. A partial description of the world is then used to separate concerns in a way that the propositions cannot be seen as contradictory. For example, one may consider the auxiliary concept of F oreigners with P eter belonging to it because he is of legal age in his country. Of course, this solves the problem with P eter, but does not solve the problem with his children that are not of legal age in his country either.
From what we have discussed, we can conclude that in order to define a legal ontology, one has either to deal with parcels of the world that have to do more with application of the law than “the law” itself or to consider a different negation and propositions denoting valid aspects of “the law”. The iALC approach depicted in this paper basically consists of a model which includes all the possible valid legal statements and the relations among them and the use of intuitionistic negation and subsumption instead of their classical counterparts.
Description logics are quite popular right now. However, They are classically
biased, in the sense that the negation (¬) of a concept is simply its
settheoretical complement, regarded to the universe of individuals. Subsumption
of concepts is set-theoretical inclusion. This seems to be enough to most of
the known applications. However, as discussed in (
iALC is a basic description language. Its concept formers are described by the following grammar:
C, D ::= A | ⊥ | > | ¬C | C u D | C t D | C v D | ∃R.C | ∀R.C where A stands for an atomic concept and R for an atomic role. This syntax is more general than standard ALC in that it includes subsumption v as a concept-forming operator. Negation can be represented via subsumption, ¬C = C v ⊥, but we find it convenient to keep it in the language. The constant > can also be omitted since it can be represented by ¬⊥.
Following Mendler and Scheele we say a constructive interpretation of iALC is a structure I = (ΔI , I , ·I ) consisting of a non-empty set ΔI of entities in which each entity represents a partially defined individual; a refinement preordering I on ΔI , i.e., a reflexive and transitive relation; and an interpretation function ·I mapping each role name R to a binary relation RI ⊆ ΔI × ΔI and each atomic concept A to a set AI ⊆ ΔI which is closed under refinement, i.e., x ∈ AI and x I y implies y ∈ AI . The interpretation I is lifted from atomic ⊥, A to arbitrary concepts via: (C t D)I =df CI ∪ DI
y ⇒ y 6∈ CI } (C v D)I =df {x|∀y ∈ ΔI .(x
y and y ∈ CI ) ⇒ y ∈ DI } (∃R.C)I =df {x|∀y ∈ ΔI .x (∀R.C)I =df {x|∀y ∈ ΔI .x y ⇒ ∃z ∈ ΔI .(y, z) ∈ RI and z ∈ CI } y ⇒ ∀z ∈ ΔI .(y, z) ∈ RI ⇒ z ∈ CI }
Clearly our setting is a simplification of Mendler and Scheele’s where we dispense with infallible entities, since our system iALC satisfies (like classical ALC) ∃R.⊥ = ⊥. But ∃R.(C t D) = ∃R.C t ∃R.D, like in Mendler and Scheele’s work is not necessarily true. We will have no use for nested subsumptions, but they do make the system easier to define, so we keep the general rules.
In this section we show an application of iALC to a part of Legal Ontology
We remind the reader that a concept symbol C, in a description logic language, is associated to a subset of legal statements representing a kind of legal situation. Roles in the description logic language are associated to relations between these legal situations, imposed by the relationship between each pair of individual legal statements.
In the sequel we detail the legal situation known as “Conflict of Laws in Space” within Private International Law scope. If ALCis used instead of iALC, the formal treatment is rather cumbersome. This is briefly commented at the end of the section.
Consider the following situation:
Peter and Maria signed a renting contract. The subject of the contract is an apartment in Rio de Janeiro. The contract states that any dispute will go to court in Rio de Janeiro. Peter is 17 and Maria is 20. Peter lives in Edinburgh and Maria lives in Rio.
In order to exist in our model, the legal statement (1) Maria and Peter have contractual obligations and rights to each other regarding an apartment in Rio de Janeiro has to be valid. Only valid legal statements are individuals present in the model. There is no invalid legal statement. This follows the foundations of jurisprudence discussed in this section. We will denote as contract the legal statement (1). Let us denote by BR the set of (valid) individual legal statements in Brazil, and, by SC the corresponding set regarding to Scotland. Since 18 is the legal age in Brazil, there is no individual legal statement about Peter in Brazil. On the other hand, the statement Maria is of legal age,M aria − l − age for short, is in BR, and P eter − l − age is in SC. There is a natural precedence relation between legal statements, only legally capable individuals have civil obligations. In other words, contract P eter−l−age and contract M aria − l − age. Let P ILBR be the set of legal statements in Brazil describing its Private International Law. Of course we have P ILBR v BR. By its very nature, P ILBR is a disjunction of sets of legal statements subsumed by ∃LexDomicilium.ABROAD. It is worth noting that Private International Law (PIL) relates legal statements in different contexts, locations, time, etc. Thus each member of PIL regards a specific context, here we deal with geographical living place. ABROAD is the union of the legal statements holding in each country, but Brazil. LexDomicilium is a legal connection, a relationship between laws in jurisprudence terminology. The pair of legal statements hP eter − l − age, P eter − l − agei is in LexDomicilium, since Peter lives in Scotland, abroad Brazil. Summing up, we have:
M aria − l − age ∈ BR P eter − l − age ∈ SC contract P eter − l − age contract M aria − l − age P ILBR v BR SC v ABROAD ∃LexDomicilium.SC v ∃LexDomicilium.ABROAD ∃LexDomicilium.ABROAD v P ILBR hP eter − l − age, P eter − l − agei ∈ LexDomicilium
Thus, from what was discussed above, we can conclude that contract ∈ BR, for each legal statement generalizing contract, with regard to , namely P eter − l − age and M aria − l − age, is in BR. For the interesting case we note that P eter − l − age ∈ ∃LexDomicilium.SC v P ILBR v BR, by the definition of ∃R.C concepts.
If one uses ALC instead of iALC in the above example formalization, she/he will need to consider a legal ontology involving non-valid Legal Statements, and hence an ad hoc ontology regarding jurisprudence main concepts. Dealing with non-valid legal statements will increase a lot the complexity of the ontology considered also. Of course we simplified our example, since it only considers P eter − l − age and M aria − l − age as succeeding contract. In a real ontology, many more statements would have to be considered, M aria − owns − the − apartment is among them. This simplification would turn much more complex the ALC case than the iALC.
Concerning the scalability of our approach, it can be argued that it scales as well as, or better than the traditional one, based on Classical ALC. Our approach does not have to deal with concepts outside jurisprudence, or more related to the application of laws. Dealing only with valid legal statements is a way to avoid describing the auxiliary terms and their ontologies. On the other hand, our approach forces us to relate these valid individual legal statements according their intrinsic juridical aspect. This can be done by considering subsumption between “sets” of individual laws. Stating A v B entails that each individual law a of kind A is preceded by every individual law b of kind b. By using our approach one has to consider only kinds of individual laws and their precedence relationship. Anyone building a legal ontology, using traditional way, has to perform this task also. Moreover, by using the traditional way of building legal ontologies, one has to deal with terms and concepts outside jurisprudence. This is, basically, the (potential) additional effort that traditional ontology practitioners have to deal with.
In this article, describing work-in-progress, we used iALC, a constructive description logic, to provide an alternative, and more adequate, definition for subsumption, that copes with the jurisprudence theory that views “The Law” as all (possible) legally valid individuals laws, instead of the totality of all (existing) valid laws.
An example of conflict of laws, namely geographic conflict of laws, was formalized by means of iALC in order to show its adequacy to perform coherence analysis in legal AI. We compared our approach with the more traditional approach, based on classic ALC, to the ontological formalization of ”the law” that includes the development of one or more domain ontologies to be used in validating the legal statements. A brief discussion on the scalability comparing both approaches was done.
Finally, we have to says some words about the state-of-the-art in performing reasoning in iALC . In (dePHR) it is presented a Sequent Calculus that provides a basis for the design of an automated reasoner for iALC . This Sequent Calculus is based on the labeled Sequent Calculus for ALC presented in (RHP2009). This is the basis for the development of a tools for performing reasoning on legal ontologies built under our approach.