intervals have no internal gaps [ekm-1] - double negation issue?

[wceusters]

The original reads:
(cl:comment "intervals have no internal gaps [ekm-1]" (forall (i start end) (if (and (instance-of i temporal-interval i) (has-first-instant i start) (has-last-instant i end)) (not (exists (gap gap-start gap-end) (and (has-first-instant gap gap-start) (has-last-instant gap gap-end) (precedes gap-end end) (precedes start gap-start) (not (temporal-part-of gap i))))))))

I think the last clause should not be negated as it falls under the first 'not', thus:

(cl:comment "intervals have no internal gaps [ekm-1]" (forall (i start end) (if (and (instance-of i temporal-interval i) (has-first-instant i start) (has-last-instant i end)) (not (exists (gap gap-start gap-end) (and (has-first-instant gap gap-start) (has-last-instant gap gap-end) (precedes gap-end end) (precedes start gap-start) (temporal-part-of gap i)))))))

[alanruttenberg]

I think it's correct. Ignore the leading not

(exists (gap gap-start gap-end)
  (and
     (has-first-instant gap gap-start)
     (has-last-instant gap gap-end)
     (precedes gap-end end)
     (precedes start gap-start)
     (not (temporal-part-of gap i))))

First note that i is a temporal interval, so gap would have to be a temporal region, since it is a temporal part of a temporal region.

Now the quoted axiom says:

There is a temporal region whose bounds are within the bounds of the temporal interval (the interval start is before the gap start and gap end is before the interval end) and that temporal region is not part of the interval.

That would mean the interval had a gap. But the axiom as a whole wants to say there are no gaps, hence the surrounding not.

Please double check.

[alanruttenberg]

BTW, you can surround a pasted bit of code with 3 backquotes ``` and it will display as monospace with the spaces preserved.