The example we discussed last time

Dear LegalRuleMLs,

Last time we discussed about formula schedule_paragraph_6_1_Statements, which is included in the attached file allExamplesSoFar.xml and that I have also isolated in trickyExample.xml for your convenience.

Although at the end it was decided to tag the formula as it is now, I cannot say that we indeed reached an agreement about it. As for me, I still think the formula is not correct in its current version, but I won't make a crusade against that. Let's leave it as it is, for me it's fine. On the other hand, I think this example raised some general problems with idiomatic LegalRuleML, which would need to be addressed.

I recall the problem. I initially proposed a formalization for "If and adult received a notice “fp”, then the adult is permitted to send “hr”, where hr is another notice". The formalization that I proposed for this sentence is:

N(fp) ^ R(a,fp) -> P( S(a,hr) ^ N(hr) )

But this is not good because in SDL we have P(S(a,hr)^N(hr)) -> P(S(a,hr)) ^ P(N(hr)).

So we would infer that "hr is permitted to be a notice", which is not what we want.

Furthermore, in order to infer this, we would have to endorse the semantics and the axiom of SDL, which is incompatible with what we always said about idiomatic LegalRuleML, i.e., that is independent from a specific logic. But let's assume that SDL holds in idiomatic LegalRuleML, for the time being… this is a separate problem.

Guido then proposed to move "N(hr)" in the antecedent. This is the solution we have now:

N(fp) ^ R(a,fp) ^ N(hr) -> P( S(a,hr) )

And I disagree with it, because if in the states of affair N(fp) and R(a,fp) are true while N(hr) is either false or (most likely) unknown, the if-then rule does not trigger, while intuitively it should. Also, in the antecedent “hr” is unrelated from the adult “a”, which also appears counter-intuitive.

So, the alternative is to add a constitutive rule. Guido said that it is equivalent with the formalization above, but I don't agree with this. I think the formalization above is incorrect and the only way to represent this rule is by adding a constitutive rule. Under this assumption, the two rules, in my opinion, should be like this:

N(fp) ^ R(a,fp) -> P( SHR(a) )

S(a,hr) ^ N(hr) -> SHR(a)

Note that I changed the predicate within the operator "P". Now it is "SHR", which stands for "Send Hearing Request" and it has a single argument: the adult "a".

In fact, I believe we can use in the consequent only variables that are in the antecedent. Or, if we need other variables these should be existentially quantified. So we could alternatively have:

N(fp) ^ R(a,fp) -> P( Ex_hr[S(a,hr)] )

Anyway, this is just a caveat. Indeed, also this formalization capture the desired inferences, provided that all variables are universally quantified over the KB:

N(fp) ^ R(a,fp) -> P( S(a,hr) )

N(hr) -> S(a,hr)

“N(hr)” is a necessary condition for the truth of “S(a,hr)”, meaning that if the object hr is not a notice, the intended sending action is not the permitted one.

Another related problem is: how can we explain the current formalization in trickyExample.xml to future LegalRuleML users? As far as I've understood, this is the issue that Adam was raising by saying (taken from the chat):

--------------------

Adam, 20:12 It is one thing to have the results of the analysis. It is another thing to have examples with guidance on the constructions. After all, we will have to instruct others in how to make translations into LegalRuleML in some consistent and principled mannner. Right now it is ad hoc.

There is no documentation about the translation procedure.

Marcello, 20:17

I agree Adam, the protocol for the translation should be described

Monica, 20:18

Yes it is the famous idiomatic canonical format

--------------------

legalruleml message