gruninger/colore

Mistake in Allen relation axiom?

Closed this issue · 1 comments

alanruttenberg commented

x all y all z ((di(x,y) & d(y,z)) -> (o(x,z) | oi(x,z) | d(x,z) | di(x,z) | (x=z))).

I was having trouble proving this for Allen relations defined over my temporal theory. Consulting https://www.ics.uci.edu/~alspaugh/cls/shr/allen.html it looks like the rhs should be "concur" or oFDseSdfO

So missing disjuncts on the rhs: fi(x,z) | f(x,z) | si(x,z) | s(x,z)

A version with the missing disjuncts is able to be proved. That doesn't mean there aren't other errors. I did check the other two cases of "concur" and they are fine.

The formula occurs in 30 files:

cd <repo>
grep -r  '(di(x,y) & d(y,z))' .