uInfinite-Past and Infinite-Future are time
points
(and (Time-Point Infinite-Past)
(=>
(Time-Point ?p) (not (Before ?p Infinite-Past))))
uThe time line is considered to be dense
(=> (and (Time-Point ?i) (Time-Point ?j) (Before ?i
?j))
(exists ?k (and (Before ?i
?k) (Before ?k ?j))))