(In-Package :hpkb)
(In-Language :hpkb-with-kif-3.0)

(Define-kb
    reusable-time (Hpkb-Upper-Level-Kernel-Latest Physical-Quantities Kif-Numbers))

(In-kb reusable-time)

;;; augmentation of Time-Interval from hpkb upper level

;;;
;;; Time-Point
;;;

(define-okbc-frame Time-Point
    :frame-type :class
    :template-facets 
    ((Location-Of (:maximum-cardinality 1))
     (Year-Of (:maximum-cardinality 1))
     (Month-Of (:maximum-cardinality 1))
     (Day-Of (:maximum-cardinality 1))
     (Week-Day-Of (:maximum-cardinality 1))
     (Hour-Of (:maximum-cardinality 1))
     (Minute-Of (:maximum-cardinality 1))
     (Second-Of (:maximum-cardinality 1))
     (Granularity-Of (:maximum-cardinality 1))))

(Define-Okbc-Frame Location-Of
    :Frame-Type :Slot 
    :Direct-Types (Binary-Relation Relation Slot) 
    :Own-Slots ((Range Time-Quantity)
		(Relation-Arity 2) 
		(Domain Time-Point)
                (Documentation "This time quantity locates this time point on the time line, 
                                and can be used to determine relations between two time points.  
                                Year-Of, Month-Of, Day-Of, Week-Day-Of, Hour-Of, Minute-Of and Second-Of 
                                are the seven slots defined for convenience.  
                                The seven slot values can be derived from the Location-Of slot value.
					  point zero is assumed to be midnight Jan 1, 1900.")))

(Define-Okbc-Frame Year-Of
    :Frame-Type :Slot 
    :Direct-Types (Binary-Relation Relation Slot) 
    :Own-Slots ((Range Integer)
		(Relation-Arity 2) 
		(Domain Time-Point)
                (Documentation "year expressed in A.D.")))

(Define-Okbc-Frame Month-Of
    :Frame-Type :Slot 
    :Direct-Types (Binary-Relation Relation Slot) 
    :Own-Slots ((Range Calendar-Month-Type)
		(Relation-Arity 2) 
		(Domain Time-Point)
                (Documentation "")))

(Define-Okbc-Frame Day-Of
    :Frame-Type :Slot 
    :Direct-Types (Binary-Relation Relation Slot) 
    :Own-Slots ((Range Calendar-Day-Type)
		(Relation-Arity 2) 
		(Domain Time-Point)
                (Documentation "")))

(Define-Okbc-Frame Week-Day-Of
    :Frame-Type :Slot 
    :Direct-Types (Binary-Relation Relation Slot) 
    :Own-Slots ((Range Calendar-Week-Day-Type)
		(Relation-Arity 2) 
		(Domain Time-Point)
                (Documentation ""))
    :Sentences (=> (and (Time-Point ?p)
                        (Week-Day-Of ?p ?w))
                   (= (Week-Day-Number-Of ?w) (+ 1 (Mod (LINLT (Magnitude (Location-Of ?p) Day-Unit)) 7)))))

(Define-Okbc-Frame Hour-Of
    :Frame-Type :Slot 
    :Direct-Types (Binary-Relation Relation Slot) 
    :Own-Slots ((Range Integer)
		(Relation-Arity 2) 
		(Domain Time-Point)
                (Documentation ""))
    :Sentences (=> (Time-Point ?p)
                   (= (Hour-Of ?p) (Mod (LINLT (Magnitude (Location-Of ?p) Hour-Unit)) 24))))
   

(Define-Okbc-Frame Minute-Of
    :Frame-Type :Slot 
    :Direct-Types (Binary-Relation Relation Slot) 
    :Own-Slots ((Range Integer)
		(Relation-Arity 2) 
		(Domain Time-Point)
                (Documentation ""))
    :Sentences (=> (Time-Point ?p)
                   (= (Minute-Of ?p) (Mod (LINLT (Magnitude (Location-Of ?p) Minute-Unit)) 60))))

(Define-Okbc-Frame Second-Of
    :Frame-Type :Slot 
    :Direct-Types (Binary-Relation Relation Slot) 
    :Own-Slots ((Range Integer)
		(Relation-Arity 2) 
		(Domain Time-Point)
                (Documentation ""))
    :Sentences (=> (Time-Point ?p)
                   (= (Second-Of ?p) (Mod (LINLT (Magnitude (Location-Of ?p) Second-Unit)) 60))))

(assertion ( => ( and (Time-Point ?p)
			    (Location-Of ?p ?l))
		    ( YMD (LINLT (Magnitude ?l Day-Unit)) (Year-Of ?p) (Month-Number-Of (Month-Of ?p)) (Day-Number-Of (Day-Of ?p)))))

(Define-Okbc-Frame YMD
    :Frame-Type :individual
    :Direct-Types (Relation) 
    :Own-Slots ((relation-arity 4))
    :Documentation "this relation maps the number of days from zero point to the Y, M, D of the particular day."
    :Sentences (=> (YMD ?n ?y ?m ?d)
    		    (and (Integer ?n)
		         (Integer ?y)
		         (Integer ?m)
		         (Integer ?d))))

(Define-Okbc-Frame Granularity-Of
    :Frame-Type :Slot 
    :Direct-Types (Binary-Relation Relation Slot) 
    :Own-Slots ((Range Time-Granularity)
		(Relation-Arity 2) 
		(Domain Time-Point)
                (Documentation "")))


;;;
;;; Granulairity
;;;

(define-okbc-frame Time-Granularity
    :frame-type :class
    :direct-superclasses (Thing)
    :template-facets 
    ((Time-Unit-Of (:maximum-cardinality 1))))

(Define-Okbc-Frame Time-Unit-Of
    :Frame-Type :Slot 
    :Direct-Types (Binary-Relation Relation Slot) 
    :Own-Slots ((Range Time-Unit)
		(Relation-Arity 2) 
		(Domain Time-Granularity)
                (Documentation "")))

(define-okbc-frame Time-Unit
    :frame-type :class
    :direct-superclasses (Unit-Of-Measure))

(assertion (and (instance-of Year-Unit Time-Unit)
		(instance-of Month-Unit Time-Unit)
		(instance-of Day-Unit Time-Unit)
		(instance-of Hour-Unit Time-Unit)
		(instance-of Minute-Unit Time-Unit)
		(instance-of Second-Unit Time-Unit)))

(assertion (and (instance-of Year-Granularity Time-Granularity)
          	(Time-Unit-Of Year-Granularity Year-Unit)))

(assertion (and (instance-of Month-Granularity Time-Granularity)
          	(Time-Unit-Of Month-Granularity Month-Unit)))

(assertion (and (instance-of Day-Granularity Time-Granularity)
          	(Time-Unit-Of Day-Granularity Day-Unit)))

(assertion (and (instance-of Hour-Granularity Time-Granularity)
          	(Time-Unit-Of Hour-Granularity Hour-Unit)))

(assertion (and (instance-of Minute-Granularity Time-Granularity)
          	(Time-Unit-Of Minute-Granularity Minute-Unit)))

(assertion (and (instance-of Second-Granularity Time-Granularity)
          	(Time-Unit-Of Second-Granularity Second-Unit)))

(assertion (instance-of Infinitely-Fine-Granularity Time-Granularity))

;;;
;;; Equal, Before and After for Time-Points
;;;

(Define-Okbc-Frame Before
    :Direct-Types (Binary-Relation) 
    :sentences (=>(and (Time-Point ?i) (Time-Point ?j))
   		  (<=> (Before ?i ?j)
       		       (or 
           		   (and (Granularity-Of ?i Infinitely-Fine-Granularity)
     				(Granularity-Of ?j Infinitely-Fine-Granularity) 
     				(<(Location-Of ?i) (Location-Of ?j)))
           		   (and (Granularity-Of ?i Infinitely-Fine-Granularity)
      				(Granularity-Of ?j ?gran-j) 
     				(<(Location-Of ?i) (The-Quantity (LINLT (Magnitude (Location-Of ?j)(Time-Unit-Of ?gran-j)))(Time-Unit-Of ?gran-j))))
           		   (and (Granularity-Of ?i gran-i)
     				(Granularity-Of ?j Infinitely-Fine-Granularity) 
                   		(<(The-Quantity (SILT (Magnitude 
        					(Location-Of ?i) (Time-Unit-Of ?gran-i))) (Time-Unit-Of ?gran-i)) (Location-Of ?j)))
            		   (and (Granularity-Of ?i ?gran-i)
	      			(Granularity-Of ?j ?gran-j)	
				(< (The-Quantity (SILT  (Magnitude (Location-Of ?i) (Time-Unit-Of ?gran-i))) (Time-Unit-Of ?gran-i))
           				(The-Quantity (LINLT (Magnitude (Location-Of ?j)(Time-Unit-Of ?gran-j)))(Time-Unit-Of ?gran-j)))))))
)
			          

(Define-Okbc-Frame After
    :Direct-Types (Binary-Relation) 
    :sentences ( =>(and (Time-Point ?i) (Time-Point ?j))
    		(<=> (After ?i ?j) (Before ?j ?i))))

(Define-Okbc-Frame Equal-Point
    :Direct-Types (Binary-Relation) 
    :sentences 
	(=>(and (Time-Point ?i) (Time-Point ?j))
   	   (<=> (Equal-Point ?i ?j)
       		(or 
	           (and (Granularity-Of ?i Infinitely-Fine-Granularity)
     			(Granularity-Of ?j Infinitely-Fine-Granularity) 
     			(=(Location-Of ?i) (Location-Of ?j)))
            	   (and (Granularity-Of ?i ?gran)
	      		(Granularity-Of ?j ?gran)	
                    	(= (LINLT (Magnitude (Location-Of ?i)
                           	             (Time-Unit-Of ?gran)))
           		   (LINLT (Magnitude (Location-Of ?j)
                                             (Time-Unit-Of ?gran)))))))))
	


;;;
;;; Time-Interval
;;;


(define-okbc-frame Time-Interval
    :frame-type :class
    :template-facets 
    ((Starting-Point (:maximum-cardinality 1))
     (Ending-Point (:maximum-cardinality 1))
     (Duration (:maximum-cardinality 1)))
    :documentation "Time-Interval can be discontinous, but must contain more
    than one time point"
    :sentences (=> (Time-Interval ?i)
    		   ( and (Before (Starting-Point ?i) (Ending-Point ?i))
		         (=> (Time-Point ?p)
			     (and (=> (Before ?p (Starting-Point ?i))
			              (not (Point-In-Interval ?p ?i)))
			          (=> (Before (Ending-Point ?i) ?p)
			              (not (Point-In-Interval ?p ?i))))))))

(Define-Okbc-Frame Starting-Point
    :Frame-Type :Slot 
    :Direct-Types (Binary-Relation Relation Slot) 
    :Own-Slots ((Range Time-Point)
		(Relation-Arity 2) 
		(Domain Time-Interval)
                (Documentation ""))
    :Sentences (=>(and (Time-Point ?s) (Time-Interval ?i))
       		  (<=> (Starting-Point ?i ?s)
                     (and (not (exists ?j 
                                (and (Time-Point ?j)
	                             (Before ?j ?s)
	    	                     (Point-In-Interval ?j ?i))))
                          (forall ?p 
 				(=> (not (exists ?k 
                			(and (Time-Point ?k)
                        	             (Before ?k ?p)
                                             (Point-In-Interval ?k  ?i))))
                                    (or (Equal-Point ?p ?s) 
                                        (Before ?p ?s))))))))

(Define-Okbc-Frame Ending-Point
    :Frame-Type :Slot 
    :Direct-Types (Binary-Relation Relation Slot) 
    :Own-Slots ((Range Time-Point)
		(Relation-Arity 2) 
		(Domain Time-Interval)
                (Documentation ""))
    :Sentences (=>(and (Time-Point ?s) (Time-Interval ?i))
       		  (<=> (Ending-Point ?i ?s)
                     (and (not (exists ?j 
                                (and (Time-Point ?j)
	                             (After ?j ?s)
	    	                     (Point-In-Interval ?j ?i))))
                          (forall ?p 
 				(=> (not (exists ?k 
                			(and (Time-Point ?k)
                        	             (After ?k ?p)
                                             (Point-In-Interval ?k  ?i))))
                                    (or (Equal-Point ?p ?s) 
                                        (After ?p ?s))))))))



(Define-Okbc-Frame Duration
    :Frame-Type :Slot 
    :Direct-Types (Binary-Relation Relation Slot) 
    :Own-Slots ((Range Time-Quantity)
		(Relation-Arity 2) 
		(Domain Time-Interval)
                (Documentation "")))

(Define-Okbc-Frame In-Year
    :Frame-Type :Slot 
    :Direct-Types (Binary-Relation Relation Slot) 
    :Own-Slots ((Range Integer)
		(Relation-Arity 2) 
		(Domain Time-Interval)
                (Documentation "(In-Year ?X 1999) means at least one point in
		interval ?X is in year 1999"))
    :sentences (<=> (In-Year ?i ?y)
    		   (exists ?p (and (Point-In-Interval ?p ?i)
		   		   (Year-Of ?p ?y)))))

(define-okbc-frame Convex-Time-Interval
    :frame-type :class
    :direct-superclasses (Time-Interval)
    :documentation "Convex-Time-Interval must be connected"
    :sentences (<=> (Convex-Time-Interval ?i)
    		    ( => ( and (Time-Point ?p)
    			 (Before (Starting-Point ?i) ?p)
			 (Before ?p (Ending-Point ?i)))
			 (Point-In-Interval ?p ?i))))

(define-okbc-frame Convex-Time-Interval-Type
    :frame-type :class
    :direct-superclasses (Thing)
    :documentation ""
    :sentences (<=> (Instance-Of ?i Convex-Time-Interval-Type)
    		    (Subclass-Of ?i Convex-Time-Interval)))

(define-okbc-frame Non-Convex-Time-Interval
    :frame-type :class
    :direct-superclasses (Time-Interval)
    :documentation "Non-Convex-Time-Interval must not be connected"
    :sentences (<=> (Non-Convex-Time-Interval ?i)
    		    ( exists ?p
                         ( and (Time-Point ?p)
    			       (Before (Starting-Point ?i) ?p)
			       (Before ?p (Ending-Point ?i))
			       (Point-In-Interval ?p ?i)))))

(assertion (Partition Time-Interval (setof Convex-Time-Interval Non-Convex-Time-Interval)))

(define-okbc-frame Characteristic-Time-Interval-Of
    :Frame-Type :Slot 
    :Direct-Types (Binary-Relation Relation Slot) 
    :Own-Slots ((Range Convex-Time-Interval-Type)
		(Relation-Arity 2) 
		(Domain Regular-Non-Convex-Time-Interval)
                (Documentation "")))

(define-okbc-frame Regular-Non-Convex-Time-Interval
    :frame-type :class
    :direct-superclasses (Non-Convex-Time-Interval)
    :documentation "Regular-Non-Convex-Time-Interval is every wednesday, every day at 10
    am, etc."
    :sentences ((=> (and (Regular-Non-Convex-Time-Interval ?r)
    		    (Characteristic-Time-Interval-Of ?r ?c))
		    (and (=> (and (holds ?c ?i)
		    	   (not (After (Starting-Point ?r) (Starting-Point ?i)))
		    	   (not (Before (Ending-Point ?r) (Ending-Point ?i))))
		   	 (Interval-In-Interval ?i ?r))))
		(=> (and (Regular-Non-Convex-Time-Interval ?r)
			 (Point-In-Interval ?p ?r))
		    (exists (?c ?i) 
		            (and (Characteristic-Time-Interval-Of ?r ?c)
			         (holds ?c ?i)
				 (Point-In-Interval ?p ?i))))) )
		   



;;;
;;; Thirteen Relations of Time-Intervals
;;;

(Define-Okbc-Frame Precedes
    :Frame-Type :Slot 
    :Direct-Types (Binary-Relation Relation Slot) 
    :Own-Slots ((Range Time-Interval)
		(Relation-Arity 2) 
		(Domain Time-Interval)
                (Documentation ""))
    :Sentences (<=> (Precedes ?i ?j)
    		    (and (Time-Interval ?i)
		         (Time-Interval ?j)
			 (Before (Ending-Point ?i) (Starting-Point ?j)))))

(Define-Okbc-Frame Precedes-Inverse
    :Frame-Type :Slot 
    :Direct-Types (Binary-Relation Relation Slot) 
    :Own-Slots ((Range Time-Interval)
		(Relation-Arity 2) 
		(Domain Time-Interval)
                (Documentation ""))
    :Sentences (<=> (Precedes-Inverse ?j ?i)
    		    (and (Time-Interval ?i)
		         (Time-Interval ?j)
			 (Before (Ending-Point ?i) (Starting-Point ?j)))))

(Define-Okbc-Frame Meets
    :Frame-Type :Slot 
    :Direct-Types (Binary-Relation Relation Slot) 
    :Own-Slots ((Range Time-Interval)
		(Relation-Arity 2) 
		(Domain Time-Interval)
                (Documentation ""))
    :Sentences (<=> (Meets ?i ?j)
    		    (and (Time-Interval ?i)
		         (Time-Interval ?j)
			 (Equal-Point (Ending-Point ?i) (Starting-Point ?j)))))

(Define-Okbc-Frame Meets-Inverse
    :Frame-Type :Slot 
    :Direct-Types (Binary-Relation Relation Slot) 
    :Own-Slots ((Range Time-Interval)
		(Relation-Arity 2) 
		(Domain Time-Interval)
                (Documentation ""))
    :Sentences (<=> (Meets-Inverse ?j ?i)
    		    (and (Time-Interval ?i)
		         (Time-Interval ?j)
			 (Equal-Point (Ending-Point ?i) (Starting-Point ?j)))))

(Define-Okbc-Frame Overlaps
    :Frame-Type :Slot 
    :Direct-Types (Binary-Relation Relation Slot) 
    :Own-Slots ((Range Time-Interval)
		(Relation-Arity 2) 
		(Domain Time-Interval)
                (Documentation ""))
    :Sentences (<=> (Overlaps ?i ?j)
    		    (and (Time-Interval ?i)
		         (Time-Interval ?j)
			 (Before (Starting-Point ?i) (Starting-Point ?j))
			 (Before (Starting-Point ?j) (Ending-Point ?i))
			 (Before (Ending-Point ?i) (Ending-Point ?j)))))

(Define-Okbc-Frame Overlaps-Inverse
    :Frame-Type :Slot 
    :Direct-Types (Binary-Relation Relation Slot) 
    :Own-Slots ((Range Time-Interval)
		(Relation-Arity 2) 
		(Domain Time-Interval)
                (Documentation ""))
    :Sentences (<=> (Overlaps-Inverse ?j ?i)
    		    (and (Time-Interval ?i)
		         (Time-Interval ?j)
			 (Before (Starting-Point ?i) (Starting-Point ?j))
			 (Before (Starting-Point ?j) (Ending-Point ?i))
			 (Before (Ending-Point ?i) (Ending-Point ?j)))))

(Define-Okbc-Frame Costarts
    :Frame-Type :Slot 
    :Direct-Types (Binary-Relation Relation Slot) 
    :Own-Slots ((Range Time-Interval)
		(Relation-Arity 2) 
		(Domain Time-Interval)
                (Documentation ""))
    :Sentences (<=> (Costarts ?i ?j)
    		    (and (Time-Interval ?i)
		         (Time-Interval ?j)
			 (Equal-Point (Starting-Point ?i) (Starting-Point ?j))
			 (Before (Ending-Point ?i) (Ending-Point ?j)))))

(Define-Okbc-Frame Costarts-Inverse
    :Frame-Type :Slot 
    :Direct-Types (Binary-Relation Relation Slot) 
    :Own-Slots ((Range Time-Interval)
		(Relation-Arity 2) 
		(Domain Time-Interval)
                (Documentation ""))
    :Sentences (<=> (Costarts-Inverse ?j ?i)
    		    (and (Time-Interval ?i)
		         (Time-Interval ?j)
			 (Equal-Point (Starting-Point ?i) (Starting-Point ?j))
			 (Before (Ending-Point ?i) (Ending-Point ?j)))))

(Define-Okbc-Frame During
    :Frame-Type :Slot 
    :Direct-Types (Binary-Relation Relation Slot) 
    :Own-Slots ((Range Time-Interval)
		(Relation-Arity 2) 
		(Domain Time-Interval)
                (Documentation ""))
    :Sentences (<=> (During ?i ?j)
    		    (and (Time-Interval ?i)
		         (Time-Interval ?j)
			 (After (Starting-Point ?i) (Starting-Point ?j))
			 (Before (Ending-Point ?i) (Ending-Point ?j)))))

(Define-Okbc-Frame During-Inverse
    :Frame-Type :Slot 
    :Direct-Types (Binary-Relation Relation Slot) 
    :Own-Slots ((Range Time-Interval)
		(Relation-Arity 2) 
		(Domain Time-Interval)
                (Documentation ""))
    :Sentences (<=> (During-Inverse ?j ?i)
    		    (and (Time-Interval ?i)
		         (Time-Interval ?j)
			 (After (Starting-Point ?i) (Starting-Point ?j))
			 (Before (Ending-Point ?i) (Ending-Point ?j)))))

(Define-Okbc-Frame Cofinishes
    :Frame-Type :Slot 
    :Direct-Types (Binary-Relation Relation Slot) 
    :Own-Slots ((Range Time-Interval)
		(Relation-Arity 2) 
		(Domain Time-Interval)
                (Documentation ""))
    :Sentences (<=> (Cofinishes ?i ?j)
    		    (and (Time-Interval ?i)
		         (Time-Interval ?j)
			 (After (Starting-Point ?i) (Starting-Point ?j))
			 (Equal-Point (Ending-Point ?i) (Ending-Point ?j)))))

(Define-Okbc-Frame Cofinishes-Inverse
    :Frame-Type :Slot 
    :Direct-Types (Binary-Relation Relation Slot) 
    :Own-Slots ((Range Time-Interval)
		(Relation-Arity 2) 
		(Domain Time-Interval)
                (Documentation ""))
    :Sentences (<=> (Cofinishes-Inverse ?j ?i)
    		    (and (Time-Interval ?i)
		         (Time-Interval ?j)
			 (After (Starting-Point ?i) (Starting-Point ?j))
			 (Equal-Point (Ending-Point ?i) (Ending-Point ?j)))))

;;; this is an augmentation of the relation in upper level

(Define-Okbc-Frame temporal-bounds-identical
    :Frame-Type :Slot 
    :Direct-Types (Binary-Relation Relation Slot) 
    :Own-Slots ((Range Time-Interval)
		(Relation-Arity 2) 
		(Domain Time-Interval)
                (Documentation ""))
    :Sentences (<=> (temporal-bounds-identical ?i ?j)
    		    (and (Time-Interval ?i)
		         (Time-Interval ?j)
			 (Equal-Point (Starting-Point ?i) (Starting-Point ?j))
			 (Equal-Point (Ending-Point ?i) (Ending-Point ?j)))))


;;;
;;; Definition of the relations in upper level
;;;

(Define-Okbc-Frame Starts-After-Ending-Of
    :Frame-Type :Slot 
    :Sentences (<=> (Starts-After-Ending-Of ?j ?i)
    		    (and (Time-Interval ?i)
		         (Time-Interval ?j)
			 (Before (Ending-Point ?i) (Starting-Point ?j))))
    :Documentation " (<=> (Precedes-Inverse ?i ?j)
    			(Starts-After-Ending-Of ?i ?j))")

(Define-Okbc-Frame Starts-After-Starting-Of
    :Frame-Type :Slot 
    :Sentences (<=> (Starts-After-Starting-Of ?j ?i)
    		    (and (Time-Interval ?i)
		         (Time-Interval ?j)
			 (Before (Starting-Point ?i) (Starting-Point ?j))))
    :Documentation "(<=> (or (Precedes-Inverse ?i ?j)
		    	(Meets-Inverse ?i ?j)
		    	(Overlap-Inverse ?i ?j)
		    	(During ?i ?j)
		    	(Cofinishes ?i ?j))
		    (Starts-After-Starting-Of ?i ?j))")

(Define-Okbc-Frame Starts-During
    :Frame-Type :Slot 
    :Sentences (<=> (Starts-During ?j ?i)
    		    (and (Time-Interval ?i)
		         (Time-Interval ?j)
			 (Before (Starting-Point ?i) (Starting-Point ?j))
			 (Before (Starting-Point ?j) (Ending-Point ?i))))
    :Documentation "(<=> (or (Overlap-Inverse ?i ?j)
		    	(During ?i ?j)
		    	(Cofinishes ?i ?j))
		(Starts-During ?i ?j))")

(Define-Okbc-Frame Ends-After-Starting-Of
    :Frame-Type :Slot 
    :Sentences (<=> (Ends-After-Starting-Of ?j ?i)
    		    (and (Time-Interval ?i)
		         (Time-Interval ?j)
			 (Before (Starting-Point ?i) (Ending-Point ?j))))
    :Documentation "(<=> (or (Precedes-Inverse ?i ?j)
		    (Meets-Inverse ?i ?j)
		    (Overlap ?i ?j)
		    (Overlap-Inverse ?i ?j)
		    (During ?i ?j)
		    (During-Inverse ?i ?j)
		    (Costarts ?i ?j)
		    (Costarts-Inverse ?i ?j)
		    (temporal-bounds-identical ?i ?j)
		    (Cofinishes ?i ?j)
		    (Cofinishes-Inverse ?i ?j))
		(Ends-After-Starting-Of ?i ?j))")

(Define-Okbc-Frame Ends-After-Ending-Of
    :Frame-Type :Slot 
    :Sentences (<=> (Ends-After-Ending-Of ?j ?i)
    		    (and (Time-Interval ?i)
		         (Time-Interval ?j)
			 (Before (Ending-Point ?i) (Ending-Point ?j))))
    :Documentation "(<=> (or (Precedes-Inverse ?i ?j)
		    (Meets-Inverse ?i ?j)
		    (Overlap-Inverse ?i ?j)
		    (During-Inverse ?i ?j)
		    (Costarts-Inverse ?i ?j))
		(Ends-After-Ending-Of ?i ?j))")

(Define-Okbc-Frame Ends-During
    :Frame-Type :Slot 
    :Sentences (<=> (Ends-During ?j ?i)
    		    (and (Time-Interval ?i)
		         (Time-Interval ?j)
			 (Before (Starting-Point ?i) (Ending-Point ?j))
			 (Before (Ending-Point ?j) (Ending-Point ?i))))
    :Documentation "(<=> (or (Overlap ?i ?j)
		    (During ?i ?j)
		    (Costarts ?i ?j))
		(Ends-During ?i ?j))")

(Define-Okbc-Frame Overlaps-Start
    :Frame-Type :Slot 
    :Sentences (<=> (Overlaps-Start ?i ?j)
    		    (and (Time-Interval ?i)
		         (Time-Interval ?j)
			 (Before (Starting-Point ?i) (Starting-Point ?j))
			 (Before (Starting-Point ?j) (Ending-Point ?i))
			 (Before (Ending-Point ?i) (Ending-Point ?j)))))
    :Documentation "(<=> (Overlaps ?i ?j)
		(Overlaps-Start ?i ?j))")

(Define-Okbc-Frame simultaneous-with
    :Frame-Type :Slot 
    :sentences ( =>(and (Time-Point ?i) (Time-Point ?j))
    		(<=> (simultaneous-with ?i ?j)
		     (Equal-Point ?i ?j)))
    :Documentation "(<=> (Equal-Point ?i ?j)
		(simultaneous-with ?i ?j))")

;;; temporally-xxxx deals with discontinuous time intervals and
;;; has domain and range of temporal thing.

;;; temporally-disjoint,

(Define-Okbc-Frame temporally-disjoint
    :Frame-Type :Slot 
    :Sentences (<=> (temporally-disjoint ?j ?i)
    		    (and (Time-Interval ?i)
		         (Time-Interval ?j)
			 (=> (Point-In-Interval ?p ?i)
			     (not (Point-In-Interval ?p ?j)))
			 (=> (Point-In-Interval ?p ?j)
			     (not (Point-In-Interval ?p ?i))))))

(assertion ( => (or (Precedes ?i ?j)
		    (Precedes-Inverse ?i ?j)
		    (Meets-OpenClosed ?i ?j)
		    (Meets-2Open ?i ?j)
		    (Meets-OpenClosed ?j ?i)
		    (Meets-2Open ?j ?i))
		(temporally-disjoint ?i ?j)))

;;; temporally-intersects,

(Define-Okbc-Frame temporally-intersects
    :Frame-Type :Slot 
    :Sentences (<=> (temporally-intersects ?j ?i)
    		    (and (Time-Interval ?i)
		         (Time-Interval ?j)
			 (exists ?p (and (Point-In-Interval ?p ?i)
			     		(Point-In-Interval ?p ?j))))))

(assertion ( <= (and (not (Precedes ?i ?j))
		     (not (Precedes-Inverse ?i ?j)))
		(temporally-intersects ?i ?j)))

;;; temporally-cooriginating is similar to costarts, but can be discontinuous

(Define-Okbc-Frame temportally-cooriginating
    :Frame-Type :Slot 
    :Sentences (<=> (temporally-cooriginating ?j ?i)
    		    (and (Time-Interval ?i)
		         (Time-Interval ?j)
			(Equal-Point (Starting-Point ?i) (Starting-Point ?j)))))

(assertion ( => (Costarts ?i ?j)
		(temportally-cooriginating ?i ?j)))

;;; temporally-coterminal,
;;;(Temporally-Coterminal ?X ?Y) means the Ending-Point of ?X is the
;;; same as the Ending-Point of ?Y. This implies that ?X and ?Y overlap, in
;;; at least one point

(Define-Okbc-Frame temportally-coterminal
    :Frame-Type :Slot 
    :Sentences (<=> (temporally-coterminal ?j ?i)
    		    (and (Time-Interval ?i)
		         (Time-Interval ?j)
			(Equal-Point (Ending-Point ?i) (Ending-Point ?j)))))

(assertion ( => (Cofinishes ?i ?j)
		(temportally-coterminal ?i ?j)))

;;; temporally-subsumes 

(Define-Okbc-Frame temporally-subsumes
    :Frame-Type :Slot 
    :Sentences (<=> (temporally-subsumes ?j ?i)
    		    (and (Time-Interval ?i)
		         (Time-Interval ?j)
			 (=> (Point-In-Interval ?p ?i)
			     (Point-In-Interval ?p ?j)))))

(assertion ( <= (or (temporal-bounds-identical ?i ?j)
		    (Costarts-Inverse ?i ?j)
		    (Cofinishes-Inverse ?i ?j)
		    (During-Inverse ?i ?j))
		(temporally-subsumes ?i ?j)))

;;; 
;;; temporal-bounds-contain require non zero length period between two
;;; starting points and ending points, but still discontinuous.

(Define-Okbc-Frame temporal-bounds-contain
    :Frame-Type :Slot 
    :Sentences (<=> (temporal-bounds-contain ?j ?i)
    		    (and (Time-Interval ?i)
		         (Time-Interval ?j)
			 (After (Starting-Point ?i) (Starting-Point ?j))
			 (Before (Ending-Point ?i) (Ending-Point ?j)))))

(assertion ( <=> (During-Inverse ?i ?j)
		 (temporal-bounds-contain ?i ?j)))

;;; temporal-bounds-intersect,
;;; (Temporal-Bounds-Intersect ?X ?Y) means that the closed solid time interval ;;; between from the start of ?X to the end of ?X,
;;; inclusive, intersects the solid time interval from the start of ?Y and the 
;;; end of ?Y, inclusive.

(Define-Okbc-Frame temporal-bounds-intersect
    :Frame-Type :Slot 
    :Sentences (<=> (temporal-bounds-intersect ?j ?i)
    		    (and (Time-Interval ?i)
		         (Time-Interval ?j)
			 (not (Before (Ending-Point ?i) (Starting-Point ?j)))
			 (not (Before (Ending-Point ?j) (Starting-Point ?i)))))
    :Documentation "(<=> (and (not (Precedes ?i ?j))
		     		(not (Precedes-Inverse ?i ?j)))
			(temporally-intersects ?i ?j))")

;;; temporal-bounds-cooriginating,
;;; temporal-bounds-coterminal
;;; in James' file, not found in ontolingua

;;;
;;; Relation between Time-Point and Time-Interval
;;;

;;; the sentences would not be true with discontinuous time intervals!!!

(Define-Okbc-Frame Point-In-Interval
    :Frame-Type :Slot 
    :Direct-Types (Binary-Relation Relation Slot) 
    :Own-Slots ((Range Time-Interval)
		(Relation-Arity 2) 
		(Domain Time-Point)
                (Documentation ""))
    :sentences ((=> (and (Time-Point ?p)
		    (Solid-Time-Interval ?i)
		    (Before (Starting-Point ?i) ?p)
		    (Before ?p (Ending-Point ?i)))
		(Point-In-Interval ?p ?i))
               (=>  (Point-In-Interval ?p ?i)
		(and (or (Before (Starting-Point ?i) ?p)
			 (Equal-Point (Starting-Point ?i) ?p))
		     (or (Before ?p (Ending-Point ?i))
			 (Equal-Point (Ending-Point ?i) ?p))))))

(Define-Okbc-Frame Interval-In-Interval
    :Frame-Type :Slot 
    :Direct-Types (Binary-Relation Relation Slot) 
    :Own-Slots ((Range Time-Interval)
		(Relation-Arity 2) 
		(Domain Time-Interval)
                (Documentation ""))
    :sentences (=> (and (Time-Interval ?i)
    			(Time-Interval ?j)
			(Interval-In-Interval ?i ?j))
		   (=> (Point-In-Interval ?p ?i)
		       (Point-In-Interval ?p ?j))))
;;;
;;; Subclasses of Time-Interval
;;;

(define-okbc-frame Time-Interval-Left-Open
    :frame-type :class
    :direct-superclasses (Time-Interval)
    :sentences (<=> (Time-Interval-Left-Open ?i)
    		(not (Point-In-Interval (Starting-Point ?i) ?i))))

(define-okbc-frame Time-Interval-Left-Closed
    :frame-type :class
    :direct-superclasses (Time-Interval)
    :sentences (<=> (Time-Interval-Left-Closed ?i)
    		(Point-In-Interval (Starting-Point ?i) ?i)))

(define-okbc-frame Time-Interval-Right-Open
    :frame-type :class
    :direct-superclasses (Time-Interval)
    :sentences (<=> (Time-Interval-Right-Open ?i)
    		(not (Point-In-Interval (Ending-Point ?i) ?i))))

(define-okbc-frame Time-Interval-Right-Closed
    :frame-type :class
    :direct-superclasses (Time-Interval)
    :sentences (<=> (Time-Interval-Right-Closed ?i)
    		(Point-In-Interval (Ending-Point ?i) ?i)))

(define-okbc-frame Time-Interval-Closed
    :frame-type :class
    :direct-superclasses (Time-Interval-Left-Closed Time-Interval-Right-Closed)
    :sentences (<=> (Time-Interval-Closed ?i)
		    (and (Point-In-Interval (Ending-Point ?i) ?i)
			 (Point-In-Interval (Starting-Point ?i) ?i))))

(define-okbc-frame Time-Interval-Open
    :frame-type :class
    :direct-superclasses (Time-Interval-Left-Open Time-Interval-Right-Open)
    :sentences (<=> (Time-Interval-Open ?i)
		    (and (not (Point-In-Interval (Ending-Point ?i) ?i))
			 (not (Point-In-Interval (Starting-Point ?i) ?i)))))


(assertion (Partition Time-Interval (setof Time-Interval-Left-Open Time-Interval-Left-Closed)))

(assertion (Partition Time-Interval (setof Time-Interval-Right-Open Time-Interval-Right-Closed)))

;;;
;;; Calendar day, month
;;;


(define-okbc-frame Calendar-Day
    :frame-type :class
    :direct-superclasses (Time-Interval)
    :template-facets 
    ((Month-Of-Interval (:maximum-cardinality 1))
     (Day-Of-Interval (:maximum-cardinality 1)))
    :sentences (=> (Calendar-Day ?c)
    		(and (Starting-Point ?c ?s)
		     (Ending-Point ?c ?e)
		     (Year-Of ?s ?y)
		     (Year-Of ?e ?y)
		     (Month-Of ?s ?m)
		     (Month-Of ?e ?m)
		     (Day-Of ?s ?d)
		     (Day-Of ?e ?d)
                     (Magnitude (Duration ?c) Hour-Unit 24))))

(define-okbc-frame Calendar-Day-1
    :frame-type :class
    :direct-superclasses (Calendar-Day))

(define-okbc-frame Calendar-Day-2
    :frame-type :class
    :direct-superclasses (Calendar-Day))

(define-okbc-frame Calendar-Day-3
    :frame-type :class
    :direct-superclasses (Calendar-Day))

(define-okbc-frame Calendar-Day-4
    :frame-type :class
    :direct-superclasses (Calendar-Day))

(define-okbc-frame Calendar-Day-5
    :frame-type :class
    :direct-superclasses (Calendar-Day))

(define-okbc-frame Calendar-Day-6
    :frame-type :class
    :direct-superclasses (Calendar-Day))

(define-okbc-frame Calendar-Day-7
    :frame-type :class
    :direct-superclasses (Calendar-Day))

(define-okbc-frame Calendar-Day-8
    :frame-type :class
    :direct-superclasses (Calendar-Day))

(define-okbc-frame Calendar-Day-9
    :frame-type :class
    :direct-superclasses (Calendar-Day))

(define-okbc-frame Calendar-Day-10
    :frame-type :class
    :direct-superclasses (Calendar-Day))

(define-okbc-frame Calendar-Day-11
    :frame-type :class
    :direct-superclasses (Calendar-Day))

(define-okbc-frame Calendar-Day-12
    :frame-type :class
    :direct-superclasses (Calendar-Day))

(define-okbc-frame Calendar-Day-13
    :frame-type :class
    :direct-superclasses (Calendar-Day))

(define-okbc-frame Calendar-Day-14
    :frame-type :class
    :direct-superclasses (Calendar-Day))

(define-okbc-frame Calendar-Day-15
    :frame-type :class
    :direct-superclasses (Calendar-Day))

(define-okbc-frame Calendar-Day-16
    :frame-type :class
    :direct-superclasses (Calendar-Day))

(define-okbc-frame Calendar-Day-17
    :frame-type :class
    :direct-superclasses (Calendar-Day))

(define-okbc-frame Calendar-Day-18
    :frame-type :class
    :direct-superclasses (Calendar-Day))

(define-okbc-frame Calendar-Day-19
    :frame-type :class
    :direct-superclasses (Calendar-Day))

(define-okbc-frame Calendar-Day-20
    :frame-type :class
    :direct-superclasses (Calendar-Day))

(define-okbc-frame Calendar-Day-21
    :frame-type :class
    :direct-superclasses (Calendar-Day))

(define-okbc-frame Calendar-Day-22
    :frame-type :class
    :direct-superclasses (Calendar-Day))

(define-okbc-frame Calendar-Day-23
    :frame-type :class
    :direct-superclasses (Calendar-Day))

(define-okbc-frame Calendar-Day-24
    :frame-type :class
    :direct-superclasses (Calendar-Day))

(define-okbc-frame Calendar-Day-25
    :frame-type :class
    :direct-superclasses (Calendar-Day))

(define-okbc-frame Calendar-Day-26
    :frame-type :class
    :direct-superclasses (Calendar-Day))

(define-okbc-frame Calendar-Day-27
    :frame-type :class
    :direct-superclasses (Calendar-Day))

(define-okbc-frame Calendar-Day-28
    :frame-type :class
    :direct-superclasses (Calendar-Day))

(define-okbc-frame Calendar-Day-29
    :frame-type :class
    :direct-superclasses (Calendar-Day))

(define-okbc-frame Calendar-Day-30
    :frame-type :class
    :direct-superclasses (Calendar-Day))

(define-okbc-frame Calendar-Day-31
    :frame-type :class
    :direct-superclasses (Calendar-Day))

(define-okbc-frame Calendar-Sunday
    :frame-type :class
    :direct-superclasses (Calendar-Day))

(define-okbc-frame Calendar-Monday
    :frame-type :class
    :direct-superclasses (Calendar-Day))

(define-okbc-frame Calendar-Tuesday
    :frame-type :class
    :direct-superclasses (Calendar-Day))

(define-okbc-frame Calendar-Wednesday
    :frame-type :class
    :direct-superclasses (Calendar-Day))

(define-okbc-frame Calendar-Thursday
    :frame-type :class
    :direct-superclasses (Calendar-Day))

(define-okbc-frame Calendar-Friday
    :frame-type :class
    :direct-superclasses (Calendar-Day))

(define-okbc-frame Calendar-Saturday
    :frame-type :class
    :direct-superclasses (Calendar-Day))

(define-okbc-frame Calendar-Day-Type
    :frame-type :class)

(assertion (and (instance-of Calendar-Day-1 Calendar-Day-Type)
                (instance-of Calendar-Day-2 Calendar-Day-Type)
                (instance-of Calendar-Day-3 Calendar-Day-Type)
                (instance-of Calendar-Day-4 Calendar-Day-Type)
                (instance-of Calendar-Day-5 Calendar-Day-Type)
                (instance-of Calendar-Day-6 Calendar-Day-Type)
                (instance-of Calendar-Day-7 Calendar-Day-Type)
                (instance-of Calendar-Day-8 Calendar-Day-Type)
                (instance-of Calendar-Day-9 Calendar-Day-Type)
                (instance-of Calendar-Day-10 Calendar-Day-Type)
                (instance-of Calendar-Day-11 Calendar-Day-Type)
                (instance-of Calendar-Day-12 Calendar-Day-Type)
                (instance-of Calendar-Day-13 Calendar-Day-Type)
                (instance-of Calendar-Day-14 Calendar-Day-Type)
                (instance-of Calendar-Day-15 Calendar-Day-Type)
                (instance-of Calendar-Day-16 Calendar-Day-Type)
                (instance-of Calendar-Day-17 Calendar-Day-Type)
                (instance-of Calendar-Day-18 Calendar-Day-Type)
                (instance-of Calendar-Day-19 Calendar-Day-Type)
                (instance-of Calendar-Day-20 Calendar-Day-Type)
                (instance-of Calendar-Day-21 Calendar-Day-Type)
                (instance-of Calendar-Day-22 Calendar-Day-Type)
                (instance-of Calendar-Day-23 Calendar-Day-Type)
                (instance-of Calendar-Day-24 Calendar-Day-Type)
                (instance-of Calendar-Day-25 Calendar-Day-Type)
                (instance-of Calendar-Day-26 Calendar-Day-Type)
                (instance-of Calendar-Day-27 Calendar-Day-Type)
                (instance-of Calendar-Day-28 Calendar-Day-Type)
                (instance-of Calendar-Day-29 Calendar-Day-Type)
                (instance-of Calendar-Day-30 Calendar-Day-Type)
                (instance-of Calendar-Day-31 Calendar-Day-Type)))

(assertion (and (Day-Number-of Calendar-Day-1 1)
                (Day-Number-of Calendar-Day-2 2)
                (Day-Number-of Calendar-Day-3 3)
                (Day-Number-of Calendar-Day-4 4)
                (Day-Number-of Calendar-Day-5 5)
                (Day-Number-of Calendar-Day-6 6)
                (Day-Number-of Calendar-Day-7 7)
                (Day-Number-of Calendar-Day-8 8)
                (Day-Number-of Calendar-Day-9 9)
                (Day-Number-of Calendar-Day-10 10)
                (Day-Number-of Calendar-Day-11 11)
                (Day-Number-of Calendar-Day-12 12)
                (Day-Number-of Calendar-Day-13 13)
                (Day-Number-of Calendar-Day-14 14)
                (Day-Number-of Calendar-Day-15 15)
                (Day-Number-of Calendar-Day-16 16)
                (Day-Number-of Calendar-Day-17 17)
                (Day-Number-of Calendar-Day-18 18)
                (Day-Number-of Calendar-Day-19 19)
                (Day-Number-of Calendar-Day-20 20)
                (Day-Number-of Calendar-Day-21 21)
                (Day-Number-of Calendar-Day-22 22)
                (Day-Number-of Calendar-Day-23 23)
                (Day-Number-of Calendar-Day-24 24)
                (Day-Number-of Calendar-Day-25 25)
                (Day-Number-of Calendar-Day-26 26)
                (Day-Number-of Calendar-Day-27 27)
                (Day-Number-of Calendar-Day-28 28)
                (Day-Number-of Calendar-Day-29 29)
                (Day-Number-of Calendar-Day-30 30)
                (Day-Number-of Calendar-Day-31 31)))

(define-okbc-frame Calendar-Week-Day-Type
    :frame-type :class)

(assertion (and (instance-of Calendar-Sunday Calendar-Week-Day-Type)
                (instance-of Calendar-Monday Calendar-Week-Day-Type)
                (instance-of Calendar-Tuesday Calendar-Week-Day-Type)
                (instance-of Calendar-Wednesday Calendar-Week-Day-Type)
                (instance-of Calendar-Thursday Calendar-Week-Day-Type)
                (instance-of Calendar-Friday Calendar-Week-Day-Type)
                (instance-of Calendar-Saturday Calendar-Week-Day-Type)))

(assertion (and (Week-Day-Number-of Calendar-Sunday 1)
                (Week-Day-Number-of Calendar-Monday 2)
                (Week-Day-Number-of Calendar-Tuesday 3)
                (Week-Day-Number-of Calendar-Wednesday 4)
                (Week-Day-Number-of Calendar-Thursday 5)
                (Week-Day-Number-of Calendar-Friday 6)
                (Week-Day-Number-of Calendar-Saturday 7)))

(define-okbc-frame Calendar-Month
    :frame-type :class
    :direct-superclasses (Convex-Time-Interval)
    :sentences (=> (Calendar-Month ?c)
    		(and (Starting-Point ?c ?s)
		     (Ending-Point ?c ?e)
		     (Year-Of ?s ?y)
		     (Year-Of ?e ?y)
		     (Month-Of ?s ?m)
		     (Month-Of ?e ?m)
                     (Magnitude (Duration ?c) Day-Unit (Month-Length ?m)) )))

(define-okbc-frame Calendar-Month-Type
    :frame-type :class
    :sentences (=> (subclass-of ?m Calendar-Month)
                   (instance-of ?m Calendar-Month-Type)))

(define-okbc-frame Calendar-January
    :frame-type :class
    :direct-superclasses (Calendar-Month))

(define-okbc-frame Calendar-February 
    :frame-type :class
    :direct-superclasses (Calendar-Month))

(define-okbc-frame Calendar-March 
    :frame-type :class
    :direct-superclasses (Calendar-Month))

(define-okbc-frame Calendar-April 
    :frame-type :class
    :direct-superclasses (Calendar-Month))

(define-okbc-frame Calendar-May 
    :frame-type :class
    :direct-superclasses (Calendar-Month))

(define-okbc-frame Calendar-June 
    :frame-type :class
    :direct-superclasses (Calendar-Month))

(define-okbc-frame Calendar-July 
    :frame-type :class
    :direct-superclasses (Calendar-Month))

(define-okbc-frame Calendar-August 
    :frame-type :class
    :direct-superclasses (Calendar-Month))

(define-okbc-frame Calendar-September 
    :frame-type :class
    :direct-superclasses (Calendar-Month))

(define-okbc-frame Calendar-October 
    :frame-type :class
    :direct-superclasses (Calendar-Month))

(define-okbc-frame Calendar-November 
    :frame-type :class
    :direct-superclasses (Calendar-Month))

(define-okbc-frame Calendar-December 
    :frame-type :class
    :direct-superclasses (Calendar-Month))

(assertion ( and (Month-Length Calendar-January 31)
		(Month-Length Calendar-February 29)
		(Month-Length Calendar-March 31)
		(Month-Length Calendar-April 30)
		(Month-Length Calendar-May 31)
		(Month-Length Calendar-June 30)
		(Month-Length Calendar-July 31)
		(Month-Length Calendar-August 31)
		(Month-Length Calendar-September 30)
		(Month-Length Calendar-October 31)
		(Month-Length Calendar-November 30)
		(Month-Length Calendar-December 31)))

(assertion ( and (Month-Number-Of Calendar-January 1)
		(Month-Number-Of Calendar-February 2)
		(Month-Number-Of Calendar-March 3)
		(Month-Number-Of Calendar-April 4)
		(Month-Number-Of Calendar-May 5)
		(Month-Number-Of Calendar-June 6)
		(Month-Number-Of Calendar-July 7)
		(Month-Number-Of Calendar-August 8)
		(Month-Number-Of Calendar-September 9)
		(Month-Number-Of Calendar-October 10)
		(Month-Number-Of Calendar-November 11)
		(Month-Number-Of Calendar-December 12)))



;;;
;;; Three cases of Meets
;;;

(Define-Okbc-Frame Meets-2Closed
    :Frame-Type :Slot 
    :Direct-Types (Binary-Relation Relation Slot) 
    :Own-Slots ((Range Time-Interval)
		(Relation-Arity 2) 
		(Domain Time-Interval)
                (Documentation ""))
    :Sentences (<=> (Meets-2Closed ?i ?j)
    		    (and (Time-Interval-Right-Closed ?i)
		         (Time-Interval-Left-Closed ?j)
			 (Meets ?i ?j))))

(Define-Okbc-Frame Meets-2Open
    :Frame-Type :Slot 
    :Direct-Types (Binary-Relation Relation Slot) 
    :Own-Slots ((Range Time-Interval)
		(Relation-Arity 2) 
		(Domain Time-Interval)
                (Documentation ""))
    :Sentences (<=> (Meets-2Open ?i ?j)
    		    (and (Time-Interval-Right-Open ?i)
		         (Time-Interval-Left-Open ?j)
			 (Meets ?i ?j))))

(Define-Okbc-Frame Meets-OpenClosed
    :Frame-Type :Slot 
    :Direct-Types (Binary-Relation Relation Slot) 
    :Own-Slots ((Range Time-Interval)
		(Relation-Arity 2) 
		(Domain Time-Interval)
                (Documentation ""))
    :Sentences (<=> (Meets-OpenClosed ?i ?j)
    		    (and (or (and (Time-Interval-Right-Open ?i)
		         	  (Time-Interval-Left-Open ?j))
    		    	     (and (Time-Interval-Right-Open ?i)
		                  (Time-Interval-Left-Open ?j)))
			 (Meets ?i ?j))))


;;;
;;; plus
;;;


(Define-Okbc-Frame Plus
    :Frame-Type :individual
    :Direct-Types (Relation) 
    :Own-Slots ((relation-arity 3))
    :Sentences (<=> (Plus ?i ?j ?k)
    		    (and (Time-Interval ?i)
		         (Time-Interval ?j)
			 (Time-Interval ?k)
			 (Time-Point ?p)
			 (<=>(or (Point-In-Interval ?p ?i)
			        (Point-In-Interval ?p ?j))
			    (Point-In-Interval ?p ?k)))))


;;;
;;; infinity
;;;

(assertion (and (Time-Point Infinite-Past)	 
                (=> (Time-Point ?p) (not (Before ?p Infinite-Past)))))

(assertion (and (Time-Point Infinite-Future)	 
                (=> (Time-Point ?p) (not (After ?p Infinite-Future)))))

;;;
;;; density
;;;

(assertion  (=> (and (Time-Point ?i)
                     (Time-Point ?j)
                     (Before ?i ?j))
                (exists ?k (and (Before ?i ?k) (Before ?k ?j)))))