Recap, Examples, and Guidelines after Skype meeting 10.06.2021

[Robaldo Livio. <livio.robaldo@swansea.ac.uk>]

Dear LegalRuleMLs,

 

This email is to recap and move a step forward the construction of a small corpus of idiomatic LegalRuleML, to be uploaded in the LegalRuleML GitHub. What follows is MY personal recap, but if I misunderstood or forgot anything, please comment.

 

We are now formalizing some provisions from the "Smoking Prohibition (Children in Motor Vehicles) (Scotland) Act 2016", available at https://www.legislation.gov.uk/asp/2016/3, and in Akoma Ntoso at https://www.legislation.gov.uk/asp/2016/3/data.akn.

 

This act is part of the âSmoking  Corpusâ on which Adam worked in the past (with some contacts he has in Paris, as far as I remember). The selected provisions are those listed in the tags â<lrml:LegalSources>...</lrml:LegalSources>â and â<lrml:Associations>...</lrml:Associations>â in the XML file attached.

 

We are formalizing these provisions in âIdiomatic LegalRuleMLâ. This is a semi-formal language, like UML. Idiomatic LegalRuleML does not refer to any specific semantics or axiomatization, it is conceived as an interchange language.

 

However, the LegalRuleML language may be also used to represent a particular logic (SDL, DDL, I/O logic, etc.) by defining a âsemantic profileâ, i.e., a formal 1:1 association between LegalRuleML tags and the constructs of the logic. Then, translation algorithms from/to Idiomatic LegalRuleML and a particular logic or between logics themselves may be defined as well, but these translations cannot of course be completely isomorphic, in that logics have different expressivities.

 

Our current goal is to provide guidelines for the end-users to support the usage of LegalRuleML. Guidelines can help to build tools for LegalRuleML. The main objective of the guidelines is to attract more people to use the standard. Therefore, they should be simple and intuitive. Anyway, guidelines are just rules of thumb, i.e., they cannot be applied algorithmically (there can be exceptions).

 

Current guidelines are the following:

 

Guideline #1: Generally, in most cases, there is an atom/predicate in the consequent for each violation.

 

Guideline #2.1: the formalization is isomorphic at the level of the paragraphs.

Guideline #2.2: the formalization is isomorphic at the level of the points within the paragraphs.

 

Guideline #3: all variables are (implicitly) universally quantified all over the LegalRuleML file. Variables are introduced with "key" at the first

time only and referred with "keyRef" in all other occurrences.

 

Note that:

 

1. These guidelines need to be motivated in the paper we are going to write. I have then created a new separate file âGuidelines.txtâ in which I listed and commented the guidelines. The file will be updated from time to time with new guidelines or comments.

 

2. These guidelines need to be tested on the examples; this is want we are going to do now, PLEASE FIND MY COMMENTS DIRECTLY IN THE XML FILE ATTACHED. Note that #2.1 and #2.2 are mutually exclusive. At the Skype meeting there was a preference towards #2.1, but the file attached I formalized both and I added comments, so we can compare & choose. See also my comments about #2.1 vs #2.2 in the file Guidelines.txt attached.

 

Last but not leastâ the XML file attached does not validate with respect to lrml-compact.xsd 😃 As you can see yourself, it protests about the values of the keyref attributes in the <ruleml:Var>, e.g:

 

col:39 - riga:69 - Errore:cvc-pattern-valid: Value '#vehicle' is not facet-valid with respect to pattern ':[\i-[:]][\c-[:]]*' for type 'keyref.value'.

 

I think I misunderstood how to use the CURIE conventionâ I understood we have to use the simbol ":" to introduce an ID and the symbol "#" to refer to it, but it seems the XSD does not like the second part. Please help.

 

Livio

 

 

 

 

 

 

Attachment: examplesFromSmokingAct2016.xml
Description: examplesFromSmokingAct2016.xml

Guideline #1: Generally, in most cases, there is an atom/predicate in the consequent for each violation.

MOTIVATION/EXPLANATION:

The guideline stems from our discussions on how to formalize the example: "if someone send the request for an hearing, the authority is obliged 
to hold an hearing". If we represent it like this:

adult(x) ^ send(x,r) ^ request(r) => O(hold(a,h) ^ isAbout(h,r) ^ authority(a) ^ hearing(h))

Then, since in SDL we have O(A^B)=>O(A)^O(B), in the formula above we derive:

adult(x) ^ send(x,r) ^ request(r) => O(hold(a,h)) ^ O(isAbout(h,r)) ^ O(authority(a)) ^ O(hearing(h))

meaning that it is obligatory for the hearing to be about the request, it is obligatory for "a" to be an authority, etc. These statements appear
to be counter-intuitive. 

It is true that we shouldn't use SDL, since idiomatic LegalRuleML is logic-neutral, but still many users will "implicitly" do it, thus generating
confusion. Various solutions are possible, but none of them is fully satisfactory. At the end, we decided for the guidelines above, stating that:

(1) First we identify all violations that can arise from the norm. 
(2) Each violation will correspond to an obligation; these obligations are conjoined in the consequent, i.e.:
	<ruleml:And><lrml:Obligation>...</lrml:Obligation> <lrml:Obligation>...</lrml:Obligation> Etc.</ruleml:And>
(3) If these obligations have "extra-predicates", these are moved in the antecedent. 

Therefore, with respect to the example above, since there is a single violation, we get:

adult(x) ^ send(x,r) ^ request(r) ^ isAbout(h,r) ^ authority(a) ^ hearing(h) => O(hold(a,h))


===================================================================================================================================================
Guideline #2.1: the formalization is isomorphic at the level of the paragraphs.
Guideline #2.2: the formalization is isomorphic at the level of the points within the paragraphs.

MOTIVATION/EXPLANATION:

These guidelines provide a rule of thumb to decide how to formalize paragraphs such as:

--------------------------------------------------------------------------------------------------------
Where a person has requested a hearing in accordance with this paragraph â??
	(a) the local authority must hold the hearing,
	(b) the person authorised for the purpose by the local authority of the area in which the offence
	    was committed must notify the procurator fiscal of the request, and
	(c) the period for payment of the fixed penalty must be calculated so that the period beginning
	    with the giving of the notice under this paragraph and ending with the receipt by the person
		who gave that notice of the decision reached at the hearing is left out of account.
--------------------------------------------------------------------------------------------------------

#2.1 states that the paragraph corresponds to a single rule with three conjoined obligations in the consequent while #2.2 states that the 
paragraph correspond to three rules with the same (or similar) antecedent and single obligation in the consequent each.

Livio prefers #2.2 as he thinks it will enhance modularity and so ease of formalization: the LegalRuleML editor can focus on a single point per time 
while ignoring the other points.

Guido and Adrian prefer #2.1 for economy reasons: since the antecedent is the same, it is not a good practice to have three copies.

However, I was thinking now... maybe the antecedent is not always the same, due to Guideline #1 above! That guideline says that all "extra-predicates"
of the obligation should be moved in the antecedent. Since there are three obligations, each of which can have some (different) extra-predicate, we
will have three different antecedents. Merging all of them together in the same consequent looks even more confusing to me. So maybe for the sake
of simplicity it is better to impose a guideline for idiomatic LegalRuleML imposing each rule to *ALWAYS* have a single obligation (or prohibition, 
or permission) in the consequent.

===================================================================================================================================================
MAYBE A NEW GUIDELINE?

Related to the previous guideline, maybe we should introduce also another guideline concerning the choice of the predicates, which should be isomorphic 
to the verb, nouns, etc. in the sentence. However, such a guideline indeed concerns formalizing in RuleML or even in Predicate Logic more generally. 

On the other hand, we should state somewhere all predicates used in LegalRuleML, e.g. <ruleml:Rel>Vehicle</ruleml:Rel>, should be connected with 
an external ontology/taxonomy/vocabulary. For instance, the ones in the DAPRECO knowledge base are connected with the PrOnto ontology. 

In the idiomatic LegalRuleML corpus we are building now, since we deem the meaning of the predicates enough self-intuitive, we do not provide 
this ontology. Rather, we only "assume" that it exists.

Besides the predicates, the LegalRuleML statements may refer to other concepts, likewise included in the ontology. For instance, the selected 
examples use the concept of defeasibility from the LegalRuleML meta-model:

<lrml:appliesStrength iri="lmrlmm:defeasible"/>

Where "lmrlmm" is the prefix of the LegalRuleML meta-model: "http://docs.oasis-open.org/legalruleml/ns/mm/v1.0/";

Users may of course define and use their own concept of defeasibility, from their own ontologies. To do so, they have just to replace 
"lmrlmm:defeasible" with their own concept.

The discussion about the reference ontology should be included in the paper, in my view.

===================================================================================================================================================
Guideline #3: all variables are (implicitly) universally quantified all over the LegalRuleML file. Variables are introduced with "key" at the first 
time only and referred with "keyRef" in all other occurrences.

MOTIVATION/EXPLANATION:

LegalRuleML is built on RuleML, which includes universal and existential quantification, so the XML format indeed allows to assert them 
(in fact, the DAPRECO KB makes use of quantifications). However, we decided in idiomatic LegalRuleML to implicitly consider all variables 
as universally quantified over the knowledge base. In other words, a LegalRuleML KB is equivalent to a formula in which we conjoin all 
assertions in the KB and we enclosed the formula within universal quantifiers binding all free variables occurring within the assertions.

This is of course done for simplicity and economy reasons.

Therefore, two predicates occurring in different rules can share some variables via the attributes "key" and "keyRef" of the tag <ruleml:Var>. 
For instance:

	<ruleml:Atom>
		<ruleml:Rel>Adult</ruleml:Rel>
		<ruleml:Var key=":adult">adult</ruleml:Var>
	</ruleml:Atom>

	<ruleml:Atom>
		<ruleml:Rel>Pay</ruleml:Rel>
		<ruleml:Var keyRef="#adult"/>
		<ruleml:Var>offence</ruleml:Var>
	</ruleml:Atom>

This means that the free variable "adult" in the first <ruleml:Atom> is the same of the second one, i.e., that they are bound by the same (implicit) 
universal quantifier. On the other hand, if we have:

	<ruleml:Atom>
		<ruleml:Rel>Adult</ruleml:Rel>
		<ruleml:Var>adult</ruleml:Var>
	</ruleml:Atom>

	<ruleml:Atom>
		<ruleml:Rel>Pay</ruleml:Rel>
		<ruleml:Var>adult</ruleml:Var>
		<ruleml:Var>offence</ruleml:Var>
	</ruleml:Atom>

And these two <ruleml:Atom> occur in two *different* rules, then the two occurrences of <ruleml:Var>adult</ruleml:Var> refer to two *different*
variables, bound by two *different* (implicit) universal quantifiers, although they have the same name ("adult").

On the other hand, if these two <ruleml:Atom> occur within the same rule, they refer to the same variable.

A final remark: the values of key and keyRef follow the CURIE naming convention: we use the simbol ":" to introduce an ID and the symbol "#" to 
refer to it. However, I think I misunderstood. If I try to validate, it raises a million of errors about this convention, e.g.:

col:39 - riga:69 - Errore:cvc-pattern-valid: Value '#vehicle' is not facet-valid with respect to pattern ':[\i-[:]][\c-[:]]*' for type 'keyref.value'.