Notation-3 and rule direction

[giacomociti]

Motivated by a blog post, I played with Notation-3 rules to derive OWL-Time relations (I see RIF and SWIRL are also mentioned in other issues of this repo).

The rules (available as gist), given time-test-individuals.ttl, generate all the xxx-true.ttl and xxx-false.ttl data in the test suite and helped spot the following missing triples:

# intervalIn-true.ttl
<http://www.w3.org/2021/time/test/individual/ent3-4>
  time:intervalIn <http://www.w3.org/2021/time/test/individual/ent0-4> ;
  time:intervalIn <http://www.w3.org/2021/time/test/individual/ent1-4> ;
  time:intervalIn <http://www.w3.org/2021/time/test/individual/ent2-4> ;
.

# after-true.ttl
<http://www.w3.org/2021/time/test/individual/ent2-4> 
    time:after <http://www.w3.org/2021/time/test/individual/ent1-1> 
.

Also I notice test files for before and after do not include triples with instants as subjects.
But this may be on purpose to keep them small.

The rules look like the following:

{
    ?T1 time:intervalStarts ?T2 .
}
<=
{
    ?T1 a time:ProperInterval ; time:hasBeginning ?B1 ; time:hasEnd ?E1 .
    ?T2 a time:ProperInterval ; time:hasBeginning ?B2 ; time:hasEnd ?E2 .
    ?B1 :equal ?B2 . 
    ?E1 :before ?E2 .
} .

where auxiliary predicates :equal and :before compare date positions of instants.

What looks strange to me is that the corresponding definition in the spec:

If a proper interval T1 is intervalStarts another proper interval T2, then the beginning of T1 is coincident with the beginning of T2, and the end of T1 is before the end of T2.

sounds more like the converse of what is implemented in the rule.

Is this meant to be a logical equivalence? Otherwise, I'm a bit confused.

[chris-little]

@dr-shorthair I understand in general what @giacomociti is trying to do, but the details are beyond me. Have you time to respond? I suspect it is just as he suggests, a balance between brevity and comprehensiveness. The corresponding definition in the spec: looks OK to me.

[dr-shorthair]

Thank you @giacomociti for your interest in OWL-Time. And thanks a lot for introducing us to Notation-3 rules. This looks like a perfect application.

Concerning your question: the textual expression of the key part of the rule says

the end of T1 is before the end of T2

Your Notation-3 implementation of that is

?E1 :before ?E2 .

These appear to be fully consistent to me. Am I misunderstanding your concern?

[giacomociti]

@dr-shorthair the N3 rule may be shortly paraphrased as:
"end of T1 before end of T2 (and same start) implies T1 starts T2"

while the spec says:
"T1 starts T2 implies end of T1 before the end of T2"

that's why it seems like one is the logical converse of the other instead of being equivalent

[dr-shorthair]

OK - I think I see the issue you are raising here now.
The two formulations are attempting to say the same thing, but the logical inference is inverted.

Since the logic is tied to the predicate (starts in this case) then I guess I prefer the second version "T1 starts T2 implies end of T1 before the end of T2". Is it possible to re-cast the N3 rule that way?

[giacomociti]

we may re-cast the N3 rule as:

{
    ?T1 a time:ProperInterval ; time:hasBeginning ?B1 ; time:hasEnd ?E1 .
    ?T2 a time:ProperInterval ; time:hasBeginning ?B2 ; time:hasEnd ?E2 .
    ?T1 time:intervalStarts ?T2 .
}
=>
{
    ?B1 time:equals ?B2 . 
    ?E1 time:before ?E2 .
} .

and maybe there are use cases in which such a rule would be useful.

Still, it would be interesting to know whether the other rule is correct wrt the semantics of OWL-Time. I guess it is since it derives all the axioms in the test suite, but I'm asking here just to be sure